From f64db5375158ff10fb77b5ab62175bae10cb76ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Jun 2016 17:51:22 +0100
Subject: [PATCH] refactor(library/init/meta/tactic): simplify 'simp' tactic

---
 library/init/meta/tactic.lean | 39 +++++++++++++----------------------
 1 file changed, 14 insertions(+), 25 deletions(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 4a23fdff46..49e40023c7 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.trace init.function
+import init.trace init.function init.option
 import init.meta.base_tactic init.meta.environment init.meta.qexpr
 
 meta_constant tactic_state : Type₁
@@ -272,26 +272,23 @@ defeq_simp_core reducible
 meta_definition dsimp : tactic unit :=
 target >>= defeq_simp >>= change
 
--- TODO(Leo): remove unifier.conservative after we finish new elaborator
-set_option unifier.conservative true
-meta_definition simp : tactic unit :=
+/- Swap first two goals, do nothing if tactic state does not have at least two goals. -/
+meta_definition swap : tactic unit :=
 do gs ← get_goals,
    match gs with
-   | (g :: rest) := do
-     (new_tgt, pf) ← target >>= simplify,
-     pf_type ← infer_type pf,
-     new_g ← mk_meta_var new_tgt,
-     ns ← return $ match expr.is_eq pf_type with
-                   | some _ := "eq"
-                   | none   := "iff"
-                   end,
-     g_pf ← mk_app (ns <.> "mpr") [pf, new_g],
-     g_pf_type ← infer_type g_pf,
-     unify g g_pf,
-     set_goals (new_g :: rest)
-   | _              := fail "simp called but no goals"
+   | g₁ :: g₂ :: rs := set_goals (g₂ :: g₁ :: rs)
+   | _              := skip
    end
 
+set_option unifier.conservative true
+
+meta_definition simp : tactic unit :=
+do (new_target, Heq) ← target >>= simplify,
+   assert "Htarget" new_target, swap,
+   ns       ← return $ (if expr.is_eq Heq ≠ none then "eq" else "iff"),
+   Ht       ← get_local "Htarget",
+   mk_app (ns <.> "mpr") [Heq, Ht] >>= exact
+
 /- Return the number of goals that need to be solved -/
 meta_definition num_goals     : tactic nat :=
 do gs ← get_goals,
@@ -352,14 +349,6 @@ meta_definition now : tactic unit :=
 do n ← num_goals,
    when (n ≠ 0) (fail "now tactic failed, there are unsolved goals")
 
-/- Swap first two goals, do nothing if tactic state does not have at least two goals. -/
-meta_definition swap : tactic unit :=
-do gs ← get_goals,
-   match gs with
-   | g₁ :: g₂ :: rs := set_goals (g₂ :: g₁ :: rs)
-   | _              := skip
-   end
-
 meta_definition apply : expr → tactic unit :=
 apply_core semireducible ff tt