class Cslib.HasFresh (α : Type u) : Type u

A type α has a computable fresh function if it is always possible, for any finite set of α, to compute a fresh element not in the set.

• fresh : Finset α → α

  Given a finite set, returns an element not in the set.

• fresh_notMem (s : Finset α) : fresh s ∉ s

  Proof that fresh returns a fresh element for its input set.

theorem Cslib.HasFresh.fresh_exists {α : Type u} [HasFresh α] (s : Finset α) : ∃ (a : α), a ∉ s

An existential version of the HasFresh typeclass. This is useful for the sake of brevity in proofs.

structure Cslib.FreeUnionConfig : Type

Configuration for the free_union term elaborator.

• singleton : Bool

  For free_union Var, include all x : Var. Defaults to true.

• finset : Bool

  For free_union Var, include all xs : Finset Var. Defaults to true.

def Cslib.elabFreeUnionConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM FreeUnionConfig

Elaborate a FreeUnionConfig.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.freeUnion : Lean.ParserDescr

Given a DecidableEq Var instance, this elaborator automatically constructs the union of any variables, finite sets of variables, and optionally the results of provided functions mapping to variables. This is configurable with optional boolean boolean arguments singleton and finset.

As an example, consider the following:

variable (x : ℕ) (xs : Finset ℕ) (var : String)

def f (_ : String) : Finset ℕ := {1, 2, 3}
def g (_ : String) : Finset ℕ := {4, 5, 6}

-- info: ∅ ∪ {x} ∪ xs : Finset ℕ
#check free_union ℕ

-- info: ∅ ∪ {x} ∪ xs ∪ f var ∪ g var : Finset ℕ
#check free_union [f, g] ℕ

info: ∅ ∪ xs : Finset ℕ
#check free_union (singleton := false) ℕ

-- info: ∅ ∪ {x} : Finset ℕ
#check free_union (finset := false) ℕ

-- info: ∅ : Finset ℕ
#check free_union (singleton := false) (finset := false) ℕ

Equations

• One or more equations did not get rendered due to their size.

def Cslib.HasFresh.freeUnion : Lean.Elab.Term.TermElab

Elaborator for free_union.

Equations

• One or more equations did not get rendered due to their size.

instance Cslib.HasFresh.to_infinite (α : Type u) [HasFresh α] : Infinite α

HasFresh α implies a computably infinite type.

@[implicit_reducible]

noncomputable instance Cslib.HasFresh.of_infinite (α : Type u) [Infinite α] : HasFresh α

All infinite types have an associated (at least noncomputable) fresh function. This, in conjunction with HasFresh.to_infinite, characterizes HasFresh.

Equations

• Cslib.HasFresh.of_infinite α = { fresh := fun (s : Finset α) => ⋯.choose, fresh_notMem := ⋯ }

@[implicit_reducible]

def Cslib.HasFresh.ofNatEmbed {α : Type u} [DecidableEq α] (e : ℕ ↪ α) : HasFresh α

Construct a fresh element from an embedding of ℕ using Nat.find.

Equations

• Cslib.HasFresh.ofNatEmbed e = { fresh := fun (s : Finset α) => e (Nat.find ⋯), fresh_notMem := ⋯ }

@[implicit_reducible]

def Cslib.HasFresh.ofSucc {α : Type u} [Inhabited α] [SemilatticeSup α] (f : α → α) (hf : ∀ (x : α), x < f x) : HasFresh α

Construct a fresh element given a function f with x < f x.

Equations

• Cslib.HasFresh.ofSucc f hf = { fresh := fun (s : Finset α) => if hs : s.Nonempty then f (s.sup' hs id) else default, fresh_notMem := ⋯ }

@[implicit_reducible]

instance Cslib.instHasFreshNat : HasFresh ℕ

ℕ has a computable fresh function.

Equations

• Cslib.instHasFreshNat = Cslib.HasFresh.ofSucc (fun (x : ℕ) => x + 1) Nat.lt_add_one

@[implicit_reducible]

instance Cslib.instHasFreshInt : HasFresh ℤ

ℤ has a computable fresh function.

Equations

• Cslib.instHasFreshInt = Cslib.HasFresh.ofSucc (fun (x : ℤ) => x + 1) Int.lt_succ

@[implicit_reducible]

instance Cslib.instHasFreshRat : HasFresh ℚ

ℚ has a computable fresh function.

Equations

• Cslib.instHasFreshRat = Cslib.HasFresh.ofSucc (fun (x : ℚ) => x + 1) Cslib.instHasFreshRat._proof_1

@[implicit_reducible]

instance Cslib.instHasFreshFinsetOfDecidableEq {α : Type u} [DecidableEq α] [HasFresh α] : HasFresh (Finset α)

If α has a computable fresh function, then so does Finset α.

Equations

• Cslib.instHasFreshFinsetOfDecidableEq = Cslib.HasFresh.ofSucc (fun (s : Finset α) => insert (Cslib.fresh s) s) ⋯

@[implicit_reducible]

instance Cslib.instHasFreshMultisetOfDecidableEqOfInhabited {α : Type u} [DecidableEq α] [Inhabited α] : HasFresh (Multiset α)

If α is inhabited, then Multiset α has a computable fresh function.

Equations

• Cslib.instHasFreshMultisetOfDecidableEqOfInhabited = Cslib.HasFresh.ofSucc (fun (s : Multiset α) => default ::ₘ s) ⋯

@[implicit_reducible]

instance Cslib.instHasFreshForallNat : HasFresh (ℕ → ℕ)

ℕ → ℕ has a computable fresh function.

Equations

• Cslib.instHasFreshForallNat = Cslib.HasFresh.ofSucc (fun (f : ℕ → ℕ) (x : ℕ) => f x + 1) Cslib.instHasFreshForallNat._proof_1