class 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 WithBot.lt_succ {α : Type u} [Preorder α] [OrderBot α] [SuccOrder α] [NoMaxOrder α] (x : WithBot α) : x < ↑x.succ

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

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

Equations

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

def 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

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

instance instHasFreshNat : HasFresh ℕ

ℕ has a computable fresh function.

Equations

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

instance instHasFreshInt : HasFresh ℤ

ℤ has a computable fresh function.

Equations

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

instance instHasFreshRat : HasFresh ℚ

ℚ has a computable fresh function.

Equations

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

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

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

Equations

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

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

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

Equations

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

instance instHasFreshForallNat : HasFresh (ℕ → ℕ)

ℕ → ℕ has a computable fresh function.

Equations

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