Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-!
## 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.
-/
namespace EnumDecide
/-- It is possible to check whether a given decidable predicate holds for all natural numbers below a given bound. -/
def decideBelow ( p : Nat → Prop )[ DecidablePred : {α : Sort ?u.6} → (α → Prop Sort (max1?u.6) p ]( bound : Nat ): Decidable (∀ n : Nat , n < bound → p n ) :=
match bound with
| 0 => by
apply Decidable.isTrue
intro n bd
contradiction
| k + 1 =>
let prev := decideBelow p k
match prev with
| Decidable.isTrue hyp : ∀ (n : Nat ), n < k p n hyp =>
if c : p k then
by
apply Decidable.isTrue h ∀ (n : Nat ), n < k + 1 p n
intro n bd
cases Nat.eq_or_lt_of_le : ∀ {n m : Nat }, n ≤ m n = m ∨ n < m bd with
| inl : ∀ {a b : Prop }, a → a ∨ b eql =>
have eql' : n = k := by
injection eql
simp [ eql' ]
assumption
| inr : ∀ {a b : Prop }, b → a ∨ b lt =>
have lt' : n < k := by
apply Nat.le_of_succ_le_succ
assumption
exact hyp : ∀ (n : Nat ), n < k p n hyp n lt'
else
by
apply Decidable.isFalse
intro contra : ∀ (n : Nat ), n < k + 1 p n contra
have lem : p k := by
apply contra : ∀ (n : Nat ), n < k + 1 p n contra k
apply Nat.le_refl : ∀ (n : Nat ), n ≤ n
contradiction
| Decidable.isFalse hyp : ¬ ∀ (n : Nat ), n < k p n hyp => by
apply Decidable.isFalse
intro contra : ∀ (n : Nat ), n < k + 1 p n contra
have lem : ∀ (n : Nat ), n < k p n lem : ∀ ( n : Nat ), n < k → p n := by
intro n bd
have bd' : n < k + 1 := by
apply Nat.le_step
exact bd
exact contra : ∀ (n : Nat ), n < k + 1 p n contra n bd'
contradiction
def decideBelowFin { m : Nat }( p : Fin m → Prop )[ DecidablePred : {α : Sort ?u.1263} → (α → Prop Sort (max1?u.1263) p ]( bound : Nat ): Decidable (∀ n : Fin m , n < bound → p n ) :=
match bound with
| 0 => by
apply Decidable.isTrue h ∀ (n : Fin m n .val< 0 p n
intro n bd
contradiction
| k + 1 =>
let prev := decideBelowFin p k
match prev with
| Decidable.isTrue hyp : ∀ (n : Fin m n .val< k p n hyp =>
if ineq : k < m then
if c : p ⟨ k , ineq ⟩ then
by
apply Decidable.isTrue h ∀ (n : Fin m n .val< k + 1 p n
intro n bd
cases Nat.eq_or_lt_of_le : ∀ {n m : Nat }, n ≤ m n = m ∨ n < m bd with
| inl : ∀ {a b : Prop }, a → a ∨ b eql =>
have eql' : n = ⟨ k , ineq ⟩ := by
n = { val := k , isLt := ineq } apply Fin.eq_of_val_eq : ∀ {n : Nat } {i j : Fin n i .val= j .vali = j a n .val= { val := k , isLt := ineq } .val
n = { val := k , isLt := ineq } injection eql
simp [ eql' ] h.inl p { val := k , isLt := ineq }
assumption
| inr : ∀ {a b : Prop }, b → a ∨ b lt =>
have lt' : n < k := by
apply Nat.le_of_succ_le_succ
assumption
exact hyp : ∀ (n : Fin m n .val< k p n hyp n lt'
else
by
apply Decidable.isFalse h ¬ ∀ (n : Fin m n .val< k + 1 p n
intro contra : ∀ (n : Fin m n .val< k + 1 p n contra
have lem : p { val := k , isLt := ineq }
lem : p ⟨ k , ineq ⟩ := by
p { val := k , isLt := ineq }
apply contra : ∀ (n : Fin m n .val< k + 1 p n contra ⟨ k , ineq ⟩ { val := k , isLt := ineq } .val< k + 1
p { val := k , isLt := ineq }
apply Nat.le_refl : ∀ (n : Nat ), n ≤ n
contradiction
else
by
apply Decidable.isTrue h ∀ (n : Fin m n .val< k + 1 p n
intro ⟨ n , nbd ⟩ _ : { val := n , isLt := nbd } .val< k + 1 h p { val := n , isLt := nbd }
have ineq' : m ≤ k := h p { val := n , isLt := nbd }
by
apply Nat.le_of_succ_le_succ
apply Nat.gt_of_not_le : ∀ {n m : Nat }, ¬ n ≤ m n > m ineq
have ineq'' := Nat.le_trans : ∀ {n m k : Nat }, n ≤ m m ≤ k n ≤ k nbd ineq' h p { val := n , isLt := nbd }
exact hyp : ∀ (n : Fin m n .val< k p n hyp ⟨ n , nbd ⟩ ineq''
| Decidable.isFalse hyp : ¬ ∀ (n : Fin m n .val< k p n hyp => by
apply Decidable.isFalse h ¬ ∀ (n : Fin m n .val< k + 1 p n
intro contra : ∀ (n : Fin m n .val< k + 1 p n contra
have lem : ∀ (n : Fin m n .val< k p n lem : ∀ ( n : Fin m ), n < k → p n := by
∀ (n : Fin m n .val< k p n intro n bd
∀ (n : Fin m n .val< k p n have bd' : n < k + 1 := by
apply Nat.le_step
exact bd
∀ (n : Fin m n .val< k p n exact contra : ∀ (n : Fin m n .val< k + 1 p n contra n bd'
contradiction
/-- It is possible to decide whether a predicate holds for all elements of `Fin n`. -/
def decideFin { m : Nat }( p : Fin m → Prop )[ DecidablePred : {α : Sort ?u.4157} → (α → Prop Sort (max1?u.4157) p ]: Decidable (∀ n : Fin m , p n ) :=
match decideBelowFin p m with
| Decidable.isTrue hyp : ∀ (n : Fin m n .val< m p n hyp =>
by
apply Decidable.isTrue
intro ⟨ n , ineq ⟩ h p { val := n , isLt := ineq }
exact hyp : ∀ (n : Fin m n .val< m p n hyp ⟨ n , ineq ⟩ ineq
| Decidable.isFalse hyp : ¬ ∀ (n : Fin m n .val< m p n hyp => by
apply Decidable.isFalse
intro contra : ∀ (n : Fin m p n contra
apply hyp : ¬ ∀ (n : Fin m n .val< m p n hyp h ∀ (n : Fin m n .val< m p n
intro ⟨ n , ineq ⟩ _ : { val := n , isLt := ineq } .val< m h p { val := n , isLt := ineq }
exact contra : ∀ (n : Fin m p n contra ⟨ n , ineq ⟩
/-- 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. -/
class DecideForall ( α : Type _ ) where
decideForall ( p : α → Prop ) [ DecidablePred : {α : Sort ?u.4647} → (α → Prop Sort (max1?u.4647) p ]:
Decidable (∀ x : α , p x )
instance { k : Nat } : DecideForall : Type ?u.4669 → Type ?u.4669 ( Fin k ) :=
⟨ by apply decideFin ⟩
instance { α : Type _ }[ dfa : DecideForall : Type ?u.4748 → Type ?u.4748 α ]{ p : α → Prop }[ DecidablePred : {α : Sort ?u.4755} → (α → Prop Sort (max1?u.4755) p ]: Decidable (∀ x : α , p x ) := dfa . decideForall p
section Examples
example : ∀ (x : Fin 3 x + 0 = x example : ∀ x : Fin 3 , x + 0 = x := by decide
example : ∀ (x y : Fin 3 x + y = y + x example : ∀ x y : Fin 3 , x + y = y + x := by
∀ (x y : Fin 3 x + y = y + x decide
theorem Zmod3.assoc : ∀ (x y z : Fin 3 x + y + z = x + (y + z Zmod3.assoc :
∀ x y z : Fin 3 , ( x + y ) + z = x + ( y + z ) := by
∀ (x y z : Fin 3 x + y + z = x + (y + z decide
end Examples
section CompositeEnumeration
@[ instance ]
def decideProd { α β : Type _ }[ dfa : DecideForall : Type ?u.6335 → Type ?u.6335 α ][ dfb : DecideForall : Type ?u.6338 → Type ?u.6338 β ] ( p : α × β → Prop )[ DecidablePred : {α : Sort ?u.6347} → (α → Prop Sort (max1?u.6347) p ] : Decidable (∀ xy : α × β , p xy ) :=
if c : (∀ x : α , ∀ y : β , p ( x , y ))
then
by
apply Decidable.isTrue
intro ( x , y )
exact c : ∀ (x : α ) (y : β ), p (x , y )
c x y
else
by
apply Decidable.isFalse
intro contra : ∀ (xy : α × β p xy contra
apply c : ¬ ∀ (x : α ) (y : β ), p (x , y ) c h ∀ (x : α ) (y : β ), p (x , y )
intro x y
exact contra : ∀ (xy : α × β p xy contra ( x , y )
instance { α β : Type _ }[ dfa : DecideForall : Type ?u.6844 → Type ?u.6844 α ][ dfb : DecideForall : Type ?u.6847 → Type ?u.6847 β ] :
DecideForall : Type ?u.6850 → Type ?u.6850 ( α × β ) :=
⟨ by apply decideProd ⟩
@[ instance ]
def decideUnit ( p : Unit → Prop )[ DecidablePred : {α : Sort ?u.6941} → (α → Prop Sort (max1?u.6941) p ] : Decidable (∀ x : Unit , p x ) :=
if c : p ( () ) then by
apply Decidable.isTrue
intro x
have l : x = () := by rfl
rw [ l ]
exact c
else by
apply Decidable.isFalse
intro contra : ∀ (x : Unit ), p x contra
apply c
exact contra : ∀ (x : Unit ), p x contra ()
instance : DecideForall : Type ?u.7086 → Type ?u.7086 Unit :=
⟨ by apply decideUnit ⟩
@[ instance ]
def decideSum { α β : Type _ }[ dfa : DecideForall : Type ?u.7127 → Type ?u.7127 α ][ dfb : DecideForall : Type ?u.7130 → Type ?u.7130 β ]( p : α ⊕ β → Prop )[ DecidablePred : {α : Sort ?u.7139} → (α → Prop Sort (max1?u.7139) p ] : Decidable (∀ x : α ⊕ β , p x ) :=
if c : ∀ x : α , p ( Sum.inl : {α : Type ?u.7170} → {β : Type ?u.7169} → α → α ⊕ β x ) then
if c' : ∀ y : β , p ( Sum.inr : {α : Type ?u.7230} → {β : Type ?u.7229} → β → α ⊕ β y ) then
by
apply Decidable.isTrue
intro x
cases x with
| inl a => exact c a
| inr a => exact c' a
else by
apply Decidable.isFalse
intro contra : ∀ (x : α ⊕ β p x contra
apply c'
intro x
exact contra : ∀ (x : α ⊕ β p x contra ( Sum.inr : {α : Type ?u.7398} → {β : Type ?u.7397} → β → α ⊕ β x )
else by
apply Decidable.isFalse
intro contra : ∀ (x : α ⊕ β p x contra
apply c
intro x
exact contra : ∀ (x : α ⊕ β p x contra ( Sum.inl : {α : Type ?u.7416} → {β : Type ?u.7415} → α → α ⊕ β x )
instance { α β : Type _ }[ dfa : DecideForall : Type ?u.7612 → Type ?u.7612 α ][ dfb : DecideForall : Type ?u.7615 → Type ?u.7615 β ] :
DecideForall : Type ?u.7618 → Type ?u.7618 ( α ⊕ β ) :=
⟨ by apply decideSum ⟩
instance funEnum { α β : Type _ }[ dfa : DecideForall : Type ?u.7711 → Type ?u.7711 α ][ dfb : DecidableEq : Sort ?u.7714 → Sort (max1?u.7714) β ] : DecidableEq : Sort ?u.7723 → Sort (max1?u.7723) ( α → β ) := fun f g =>
if c :∀ x : α , f x = g x then
by
apply Decidable.isTrue
apply funext : ∀ {α : Sort ?u.7846} {β : α → Sort ?u.7845f g : (x : α ) → β x }, (∀ (x : α ), f x = g x ) → f = g
intro x
exact c x
else
by
apply Decidable.isFalse
intro contra
apply c
intro x
exact congrFun : ∀ {α : Sort ?u.7881} {β : α → Sort ?u.7880f g : (x : α ) → β x }, f = g ∀ (a : α ), f a = g a contra x
example : ∀ (xy : Fin 3 × Fin 2 xy .fst+ xy .snd= xy .snd+ xy .fst example : ∀ xy : ( Fin 3 ) × ( Fin 2 ),
xy . 1 : {α : Type ?u.8079} → {β : Type ?u.8078} → α × β α . val + xy . 2 : {α : Type ?u.8087} → {β : Type ?u.8086} → α × β β . val = xy . 2 : {α : Type ?u.8095} → {β : Type ?u.8094} → α × β β . val + xy . 1 : {α : Type ?u.8100} → {β : Type ?u.8099} → α × β α . val := by
∀ (xy : Fin 3 × Fin 2 xy .fst+ xy .snd= xy .snd+ xy .fst decide
end CompositeEnumeration