max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/run/cpdt): simplify

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-19 13:49:19 -08:00
parent 50f4a28fc3
commit ec6e1e389b
1 changed files with 2 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/run/cpdt.lean
View file

@ -20,9 +20,7 @@ def times (k : nat) : exp → exp
attribute [simp] exp_eval times mul_add
theorem eval_times (k e) : exp_eval (times k e) = k * exp_eval e :=
by induction e; simp_using_hs
/- CPDT: induction e; crush. -/
by induction e; simph
def reassoc : exp → exp
| (Const n) := (Const n)
@ -43,8 +41,5 @@ def reassoc : exp → exp
attribute [simp] reassoc
lemma rewr : ∀ a b c d : nat, b * c = d → a * b * c = a * d :=
by intros; simp_using_hs
theorem reassoc_correct (e) : exp_eval (reassoc e) = exp_eval e :=
by induction e; simp; try {cases (reassoc e2); dsimp at ih_2; dsimp; simp_using_hs}
by induction e; simph; try {cases (reassoc e2); rsimp}