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.

In the source code of this file, you can find an example implementation of this typeclass for the natural numbers.

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, ⋯⟩