michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

doc(builtin): Diaconescu’s theorem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-18 09:11:54 -08:00
parent e9dada5e14
commit f781ad823c
1 changed files with 43 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/builtin/dia.lean Normal file
View file

@ -0,0 +1,43 @@
import macros
theorem bool_inhab : inhabited Bool
:= inhabited_intro true
-- Excluded middle from eps_ax, boolext, funext, and subst
theorem em_new (p : Bool) : p ∨ ¬ p
:= let u := @eps Bool bool_inhab (λ x, x = true ∨ p),
v := @eps Bool bool_inhab (λ x, x = false ∨ p) in
have Hu : u = true ∨ p,
from @eps_ax Bool bool_inhab (λ x, x = true ∨ p) true (or_introl (refl true) p),
have Hv : v = false ∨ p,
from @eps_ax Bool bool_inhab (λ x, x = false ∨ p) false (or_introl (refl false) p),
have H1 : u ≠ v ∨ p,
from or_elim Hu
(assume Hut : u = true,
or_elim Hv
(assume Hvf : v = false,
have Hne : u ≠ v,
from subst (subst true_ne_false (symm Hut)) (symm Hvf),
or_introl Hne p)
(assume Hp : p, or_intror (u ≠ v) Hp))
(assume Hp : p, or_intror (u ≠ v) Hp),
have H2 : p → u = v,
from assume Hp : p,
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p),
from funext (take x : Bool,
have Hl : (x = true ∨ p) → (x = false ∨ p),
from assume A, or_intror (x = false) Hp,
have Hr : (x = false ∨ p) → (x = true ∨ p),
from assume A, or_intror (x = true) Hp,
show (x = true ∨ p) = (x = false ∨ p),
from boolext Hl Hr),
show u = v,
from @subst (Bool → Bool) (λ x : Bool, (@eq Bool x true) ∨ p) (λ x : Bool, (@eq Bool x false) ∨ p)
(λ q : Bool → Bool, @eps Bool bool_inhab (λ x : Bool, (@eq Bool x true) ∨ p) = @eps Bool bool_inhab q)
(@refl Bool (@eps Bool bool_inhab (λ x : Bool, (@eq Bool x true) ∨ p)))
Hpred,
have H3 : u ≠ v → ¬ p,
from contrapos H2,
or_elim H1
(assume Hne : u ≠ v, or_intror p (H3 Hne))
(assume Hp : p, or_introl Hp (¬ p))