Documentation

PfsProgs25.Unit10.Listable

Listable typeclass #

This is a crude version of finite types. It is a typeclass that provides a list of all the elements of a type.

class Listable (α : Type u) :

elems : List α
elemsComplete (a : α) : a ∈ Listable.elems

Instances

instance instListableBool :

Equations

instListableBool = { elems := [false, true], elemsComplete := instListableBool.proof_1 }

def elemsList (α : Type u) [Listable α] :

Equations

elemsList α = Listable.elems

Instances For

theorem memElemList {α : Type u} [Listable α] (a : α) :

a ∈ elemsList α

instance prodListable {α β : Type u} [Listable α] [Listable β] :

Listable (α × β)

Equations

prodListable = { elems := let as := elemsList α; let bs := elemsList β; do let a ← as let b ← bs pure (a, b), elemsComplete := ⋯ }

Application of listable #

Suppose α is Listable and f, g: α → ℕ are functions. Then we can decide (algorithmically) if f = g . This is impossible for α = ℕ and f, g arbitrary.

Having decision procedures is captured by the Decidable typeclass. This gives a Boolean-valued function decide.

def NatFns.f (n : ℕ) :

Equations

NatFns.f n = n + 1

Instances For

def NatFns.g (n : ℕ) :

Equations

NatFns.g n = n + 2

Instances For

def FinFns.f (n : Fin 5) :

Equations

FinFns.f n = ↑n + 1

Instances For

def FinFns.g (n : Fin 5) :

Equations

FinFns.g n = ↑n + 2

Instances For

We will use Listable to make a similar decision procedure.

def List.decidableFunctionEqual {α β : Type} [DecidableEq β] (f g : α → β) (l : List α) :

Decidable (∀ x ∈ l, f x = g x)

Equations

List.decidableFunctionEqual f g l = List.rec (isTrue ⋯) (fun (h : α) (tail : List α) (ih : Decidable (∀ x ∈ tail, f x = g x)) => if p : f h = g h then ⋯.mpr ih else isFalse ⋯) l

Instances For

instance decidableEqFns_of_Listable {α β : Type} [Listable α] [DecidableEq β] (f g : α → β) :

Decidable (f = g)

Equations

decidableEqFns_of_Listable f g = if p : ∀ x ∈ elemsList α, f x = g x then isTrue ⋯ else isFalse ⋯

instance instListableShortAnswer :

Listable ShortAnswer

Equations

instListableShortAnswer = { elems := [ShortAnswer.yes, ShortAnswer.no, ShortAnswer.maybe], elemsComplete := instListableShortAnswer.proof_1 }