From 244e061f76320ea293cc774dca56edf66f72abae Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sun, 8 Jan 2017 10:45:48 +0100 Subject: [PATCH] refactor(tools/super/simp): do not enable simp by default simp interacts badly with super's term ordering. I believe a better approach is to pick the term ordering according to the available simp rules, as in "More SPASS with Isabelle". --- library/tools/super/simp.lean | 1 - tests/lean/run/super_examples.lean | 7 +++---- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/library/tools/super/simp.lean b/library/tools/super/simp.lean index 582c618ceb..ec296a7a18 100644 --- a/library/tools/super/simp.lean +++ b/library/tools/super/simp.lean @@ -35,7 +35,6 @@ on_right_at' c i $ λhyp, do prf ← mk_app ``eq.mpr [heqsymm, hyp], return [(add_hyps, prf)] -@[super.inf] meta def simp_inf : inf_decl := inf_decl.mk 40 $ take given, sequence' $ do r ← [try_simplify_right, try_simplify_left], i ← list.range given^.c^.num_lits, diff --git a/tests/lean/run/super_examples.lean b/tests/lean/run/super_examples.lean index 9e59b3b4d3..f438cb45f3 100644 --- a/tests/lean/run/super_examples.lean +++ b/tests/lean/run/super_examples.lean @@ -23,11 +23,10 @@ example (n : ℕ) : n > 0 ↔ is_positive n := by super example (m n : ℕ) : 0 + m = 0 + n → m = n := by super with nat.zero_add -local attribute [simp] nat.zero_add nat.succ_add -@[simp] lemma nat_add_succ (m n : ℕ) : m + nat.succ n = nat.succ (m + n) := rfl -@[simp] lemma nat_zero_has_zero : nat.zero = 0 := rfl example : ∀x y : ℕ, x + y = y + x := -begin intros, induction x, super, super end +begin intros, induction x, + super with nat.add_zero nat.zero_add, + super with nat.add_succ nat.succ_add end example (i) [inhabited i] : nonempty i := by super example (i) [nonempty i] : ¬(inhabited i → false) := by super