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

Make example 1 less symmetric

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-03 18:12:46 -07:00
parent 8e7c657cf7
commit c6db95802c
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
examples/ex1.lean
View file

@ -13,14 +13,14 @@ Variable d : N
Variable e : N Variable e : N
(* Add axioms stating facts about these variables *) (* Add axioms stating facts about these variables *)
Axiom H1 : (a = b ∧ b = c) ∨ (a = d ∧ d = c) Axiom H1 : (a = b ∧ b = c) ∨ (d = c ∧ a = d)
Axiom H2 : b = e Axiom H2 : b = e
(* Proof that (h a b) = (h c e) *) (* Proof that (h a b) = (h c e) *)
Theorem T1 : (h a b) = (h c e) := Theorem T1 : (h a b) = (h c e) :=
DisjCases H1 DisjCases H1
(λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2) (λ C1, CongrH (Trans (Conjunct1 C1) (Conjunct2 C1)) H2)
(λ C2, CongrH (Trans (Conjunct1 C2) (Conjunct2 C2)) H2) (λ C2, CongrH (Trans (Conjunct2 C2) (Conjunct1 C2)) H2)
(* We can use theorem T1 to prove other theorems *) (* We can use theorem T1 to prove other theorems *)
Theorem T2 : (h a (h a b)) = (h a (h c e)) := Theorem T2 : (h a (h a b)) = (h a (h c e)) :=