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

fix(tests/lean): remove unnecessary theorems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-19 12:55:33 -08:00
parent cc11b9e125
commit 999984e701
2 changed files with 0 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/simp2.lean
View file

@ -16,15 +16,6 @@ theorem symm_trans {A : TypeU} {a b c : A} (Hab : a = b) (Hbc : b = c) :
symm (trans Hab Hbc) = trans (symm Hbc) (symm Hab)
:= proof_irrel (symm (trans Hab Hbc)) (trans (symm Hbc) (symm Hab))
theorem trans_valley1 {A : TypeU} {a b c d : A} (Hab : a = b) (Hbc : b = c) (Hcb : c = b) (Hbd : b = d) :
trans Hab (trans Hbc (trans Hcb Hbd)) = trans Hab Hbd
:= proof_irrel (trans Hab (trans Hbc (trans Hcb Hbd))) (trans Hab Hbd)
theorem trans_valley2 {A : TypeU} {a b c d e : A} (Hab : a = b) (Hbc : b = c) (Hcb : c = b) (Hbd : b = d) (Hde : d = e) :
trans Hab (trans Hbc (trans Hcb (trans Hbd Hde))) = trans Hab (trans Hbd Hde)
:= proof_irrel (trans Hab (trans Hbc (trans Hcb (trans Hbd Hde)))) (trans Hab (trans Hbd Hde))
-- Now, we define a new rewrite rule set for these theorems
rewrite_set proof_simp
add_rewrite trans_refl_right trans_refl_left trans_assoc symm_trans : proof_simp

2
tests/lean/simp2.lean.expected.out
View file

@ -4,8 +4,6 @@
Proved: trans_refl_left
Proved: trans_assoc
Proved: symm_trans
Proved: trans_valley1
Proved: trans_valley2
Assumed: a1
Assumed: a2
Assumed: a3