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 types.
• EnumDecide.funEnum - the type of functions from an exhaustively checkable type to a type with decidable equality is exhaustively checkable.

def LeanPool.Polylean.EnumDecide.decideBelow (p : Nat → Prop) [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

• LeanPool.Polylean.EnumDecide.decideBelow p 0 = isTrue ⋯
• LeanPool.Polylean.EnumDecide.decideBelow p k.succ = match LeanPool.Polylean.EnumDecide.decideBelow p k with | isTrue hyp => if c : p k then isTrue ⋯ else isFalse ⋯ | isFalse hyp => isFalse ⋯

def LeanPool.Polylean.EnumDecide.decideBelowFin {m : Nat} (p : Fin m → Prop) [DecidablePred p] (bound : Nat) : Decidable (∀ (n : Fin m), ↑n < bound → p n)

It is possible to check whether a decidable predicate on Fin m holds below a given natural-number bound.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.EnumDecide.decideBelowFin p 0 = isTrue ⋯

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

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

Equations

• LeanPool.Polylean.EnumDecide.decideFin p = match LeanPool.Polylean.EnumDecide.decideBelowFin p m with | isTrue hyp => isTrue ⋯ | isFalse hyp => isFalse ⋯

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

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.

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

  Decide whether a decidable predicate holds for all elements.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LeanPool.Polylean.EnumDecide.instDecidableForallOfDecideForallOfDecidablePred {α : Type u_1} [dfa : DecideForall α] {p : α → Prop} [DecidablePred p] : Decidable (∀ (x : α), p x)

Equations

• LeanPool.Polylean.EnumDecide.instDecidableForallOfDecideForallOfDecidablePred = LeanPool.Polylean.EnumDecide.DecideForall.decideForall p

@[reducible]

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

Equations

• LeanPool.Polylean.EnumDecide.decideProd p = if c : ∀ (x : α) (y : β), p (x, y) then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

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

Equations

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

@[reducible]

instance LeanPool.Polylean.EnumDecide.decideUnit (p : Unit → Prop) [DecidablePred p] : Decidable (∀ (x : Unit), p x)

Equations

• LeanPool.Polylean.EnumDecide.decideUnit p = if c : p () then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance LeanPool.Polylean.EnumDecide.instDecideForallUnit : DecideForall Unit

Equations

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

@[reducible]

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

Equations

• LeanPool.Polylean.EnumDecide.decideSum p = if c : ∀ (x : α), p (Sum.inl x) then if c' : ∀ (y : β), p (Sum.inr y) then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• LeanPool.Polylean.EnumDecide.funEnum f g = if c : ∀ (x : α), f x = g x then isTrue ⋯ else isFalse ⋯