Decision by enumeration

For a type X that is finite (or more generally, compact), it is possible to automatically decide any statement of the form ∀ x : X, P x by enumeration when P is a decidable predicate on X (i.e., a predicate for the individual propositions P x are decidable for any given x : X).

Overview

The EnumDecide.decideForall typeclass defines the property of a type being exhaustively checkable.

Results in this file include

• EnumDecide.decideFin - the type Fin n (the canonical finite set with n elements) is checkable for any n : ℕ.
• EnumDecide.decideUnit - the single-element type is exhaustively checkable.
• EnumDecide.decideProd, EnumDecide.decideSum - the product and direct sum of two exhaustively checkable.
• EnumDecide.funEnum - the type of functions from an exhaustively checkable type to a type with decidable equality is exhaustively checkable.

ink

def EnumDecide.decideBelow (p : Nat → Prop) [inst : DecidablePred p] (bound : Nat) : Decidable ((n : Nat) → n < bound → p n)

It is possible to check whether a given decidable predicate holds for all natural numbers below a given bound.

Equations

• One or more equations did not get rendered due to their size.
• EnumDecide.decideBelow p 0 = isTrue fun n bd => False.elim (_ : False)

ink

def EnumDecide.decideBelowFin {m : Nat} (p : Fin m → Prop) [inst : DecidablePred p] (bound : Nat) : Decidable ((n : Fin m) → n.val < bound → p n)

Equations

• One or more equations did not get rendered due to their size.
• EnumDecide.decideBelowFin p 0 = isTrue fun n bd => False.elim (_ : False)

ink

def EnumDecide.decideFin {m : Nat} (p : Fin m → Prop) [inst : DecidablePred p] : Decidable ((n : Fin m) → p n)

It is possible to decide whether a predicate holds for all elements of Fin n.

Equations

• EnumDecide.decideFin p = match EnumDecide.decideBelowFin p m with | isTrue hyp => isTrue (EnumDecide.decideFin.proof_1 p hyp) | isFalse hyp => isFalse (_ : ((n : Fin m) → p n) → False)

ink

class EnumDecide.DecideForall (α : Type u_1) : Type u_1

• decideForall : (p : α → Prop) → [inst : DecidablePred p] → Decidable (∀ (x : α), p x)

A typeclass for "exhaustively verifiable types", i.e., types for which it is possible to decide whether a given (decidable) predicate holds for all its elements.

ink

instance EnumDecide.instDecideForallFin {k : Nat} : EnumDecide.DecideForall (Fin k)

Equations

• EnumDecide.instDecideForallFin = { decideForall := EnumDecide.decideFin }

ink

instance EnumDecide.instDecidableForAll {α : Type u_1} [dfa : EnumDecide.DecideForall α] {p : α → Prop} [inst : DecidablePred p] : Decidable ((x : α) → p x)

Equations

• EnumDecide.instDecidableForAll = EnumDecide.DecideForall.decideForall p

ink

theorem EnumDecide.Zmod3.assoc (x : Fin 3) (y : Fin 3) (z : Fin 3) : x + y + z = x + (y + z)

ink

instance EnumDecide.decideProd {α : Type u_1} {β : Type u_2} [dfa : EnumDecide.DecideForall α] [dfb : EnumDecide.DecideForall β] (p : α × β → Prop) [inst : DecidablePred p] : Decidable ((xy : α × β) → p xy)

Equations

• EnumDecide.decideProd p = if c : (x : α) → (y : β) → p (x, y) then isTrue (EnumDecide.decideProd.proof_1 p c) else isFalse (_ : ((xy : α × β) → p xy) → False)

ink

instance EnumDecide.instDecideForallProd {α : Type u_1} {β : Type u_2} [dfa : EnumDecide.DecideForall α] [dfb : EnumDecide.DecideForall β] : EnumDecide.DecideForall (α × β)

Equations

• EnumDecide.instDecideForallProd = { decideForall := EnumDecide.decideProd }

ink

instance EnumDecide.decideUnit (p : Unit → Prop) [inst : DecidablePred p] : Decidable ((x : Unit) → p x)

Equations

• EnumDecide.decideUnit p = if c : p () then isTrue (EnumDecide.decideUnit.proof_1 p c) else isFalse (_ : ((x : Unit) → p x) → False)

ink

instance EnumDecide.instDecideForallUnit : EnumDecide.DecideForall Unit

Equations

• EnumDecide.instDecideForallUnit = { decideForall := EnumDecide.decideUnit }

ink

instance EnumDecide.decideSum {α : Type u_1} {β : Type u_2} [dfa : EnumDecide.DecideForall α] [dfb : EnumDecide.DecideForall β] (p : α ⊕ β → Prop) [inst : DecidablePred p] : Decidable ((x : α ⊕ β) → p x)

Equations

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

ink

instance EnumDecide.instDecideForallSum {α : Type u_1} {β : Type u_2} [dfa : EnumDecide.DecideForall α] [dfb : EnumDecide.DecideForall β] : EnumDecide.DecideForall (α ⊕ β)

Equations

• EnumDecide.instDecideForallSum = { decideForall := EnumDecide.decideSum }

ink

instance EnumDecide.funEnum {α : Type u_1} {β : Type u_2} [dfa : EnumDecide.DecideForall α] [dfb : DecidableEq β] : DecidableEq (α → β)

Equations

• EnumDecide.funEnum f g = if c : ∀ (x : α), f x = g x then isTrue (_ : f = g) else isFalse (_ : f = g → False)