GetFreshInhabitant

This file defines a type class GetFreshInhabitant that provides a single function GetFreshInhabitant.fresh. This function takes as input a list l over a type t and then returns an element of type t that does itself not occur in l. This captures the intuition that certain types always allow picking "fresh" representants. For example, one would assume that it is always possibly to pick a fresh natural numbers if only finitely many numbers have been used so far.

To give an example, we also implement this typeclass for the natural numbers at the end of the file.

class GetFreshInhabitant (t : Type u) : Type u

A type class that allows to get a fresh element of the desired type. That is, an element that does not occur in a given list.

• fresh (l : List t) : { e : t // ¬e ∈ l }

def GetFreshInhabitant.fresh_n {t : Type u} [GetFreshInhabitant t] (l : List t) (n : Nat) : { l' : List t // l'.length = n ∧ l'.Nodup ∧ ∀ (e : t), e ∈ l' → ¬e ∈ l }

If we are able to pick individual fresh elements, we can also pick a list of n fresh elements at once using this function. Of course this list shall not contain any duplicates.

Equations

• GetFreshInhabitant.fresh_n l Nat.zero = ⟨[], ⋯⟩
• GetFreshInhabitant.fresh_n l n_2.succ = ⟨(GetFreshInhabitant.fresh ((GetFreshInhabitant.fresh_n l n_2).val ++ l)).val :: (GetFreshInhabitant.fresh_n l n_2).val, ⋯⟩

We give an example implementation for the natural numbers.

def Nat.fresh (l : List Nat) : { n : Nat // ¬n ∈ l }

For a list of natural numbers, we can pick a fresh element by taking the successor of the maximal number from the list.

Equations

• Nat.fresh l = ⟨(l.max?.getD 0).succ, ⋯⟩

instance Nat.instGetFreshInhabitant : GetFreshInhabitant Nat

Equations

• Nat.instGetFreshInhabitant = { fresh := Nat.fresh }