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

chore(examples/lean): use macros in examples

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-01 14:01:12 -08:00
parent 7726ccad28
commit a299778c88
2 changed files with 25 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
examples/lean/ex2.lean
View file

@ -1,17 +1,19 @@
Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
Discharge (λ H_pq_qr, Discharge (λ H_p,
Import macros.
Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r
:= assume H_pq_qr H_p,
let P_pq := Conjunct1 H_pq_qr,
P_qr := Conjunct2 H_pq_qr,
P_q := MP P_pq H_p
in MP P_qr P_q))
in MP P_qr P_q.
SetOption pp::implicit true
Show Environment 1
SetOption pp::implicit true.
Show Environment 1.
Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c :=
Discharge (λ H_abc, Discharge (λ H_ab, Discharge (λ H_a,
Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c
:= assume H_abc H_ab H_a,
let P_b := (MP H_ab H_a),
P_bc := (MP H_abc H_a)
in MP P_bc P_b)))
in MP P_bc P_b.
Show Environment 1
Show Environment 1.

25
examples/lean/ex3.lean
View file

@ -1,10 +1,13 @@
Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) :=
Discharge (λ H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab))
Import macros.
Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) :=
Discharge (λ H_ab, DisjCases H_ab
(λ H_a, Disj2 b H_a)
(λ H_b, Disj1 H_b a))
Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a)
:= assume H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab).
Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a)
:= assume H_ab,
DisjCases H_ab
(λ H_a, Disj2 b H_a)
(λ H_b, Disj1 H_b a).
(* ---------------------------------
(EM a) is the excluded middle a ∨ ¬a
@ -19,9 +22,9 @@ NotImp1 applied to
produces
a
----------------------------------- *)
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
Discharge (λ H, DisjCases (EM a)
(λ H_a, H_a)
(λ H_na, NotImp1 (MT H H_na)))
Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a
:= assume H, DisjCases (EM a)
(λ H_a, H_a)
(λ H_na, NotImp1 (MT H H_na)).
Show Environment 3
Show Environment 3.