From b52e8d67bea5a9c400415bc82e7f40fe147d85fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Feb 2017 13:02:08 -0800
Subject: [PATCH] feat(library/init/meta): simp&intro tactics

---
 library/init/data/nat/lemmas.lean  |  2 +-
 library/init/meta/interactive.lean | 19 ++++++++++++++
 library/init/meta/simp_tactic.lean | 42 ++++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+), 1 deletion(-)

diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index b221dc77a4..e51f66505b 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -64,7 +64,7 @@ protected lemma zero_ne_one : 0 ≠ (1 : ℕ) :=
 assume h, nat.no_confusion h
 
 lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
-| 0     m := by simp [nat.zero_add] {contextual := tt}
+| 0     m := by simp [nat.zero_add]
 | (n+1) m := λ h,
   begin
     exfalso,
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index fad6306570..1862d8b692 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -497,6 +497,25 @@ meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
                (cfg : simplify_config := {}) : tactic unit :=
 simp_using_hs hs attr_names ids cfg
 
+meta def simp_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
+                     (wo_ids : parse without_ident_list) (cfg : simplify_config := {}) : tactic unit :=
+do s ← mk_simp_set attr_names hs wo_ids,
+   match ids with
+   | [] := simp_intros_using s cfg
+   | ns := simp_intro_lst_using ns s cfg
+   end,
+   try triv >> try (reflexivity reducible)
+
+meta def simph_intros (ids : parse ident*) (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list)
+                     (wo_ids : parse without_ident_list) (cfg : simplify_config := {}) : tactic unit :=
+do s ← mk_simp_set attr_names hs wo_ids,
+   match ids with
+   | [] := simph_intros_using s cfg
+   | ns := simph_intro_lst_using ns s cfg
+   end,
+   try triv >> try (reflexivity reducible)
+
+
 private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit
 | []      := skip
 | (h::hs) := get_local h >>= dsimp_at_core s
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 6d33e1ee35..1475ce7895 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -294,6 +294,48 @@ do es ← collect_ctx_simps, simp_using es cfg
 meta def simph (cfg : simplify_config := {}) :=
 simp_using_hs cfg
 
+meta def intro1_aux : bool → list name → tactic expr
+| ff _       := intro1
+| tt (n::ns) := intro n
+| _  _       := failed
+
+meta def simp_intro_aux (cfg : simplify_config) (updt : bool) : simp_lemmas → bool → list name → tactic unit
+| S tt     [] := return ()
+| S use_ns ns := do
+  t ← target,
+  if t^.is_napp_of `not 1 then
+    intro1_aux use_ns ns >> simp_intro_aux S use_ns ns^.tail
+  else if t^.is_arrow then do
+    d ← return t^.binding_domain,
+    (new_d, h_d_eq_new_d) ← simplify S d cfg,
+    h_d ← intro1_aux use_ns ns,
+    h_new_d ← mk_eq_mp h_d_eq_new_d h_d,
+    assertv_core h_d^.local_pp_name new_d h_new_d,
+    h_new   ← intro1,
+    new_S ← if updt && is_equation new_d then S^.add h_new else return S,
+    clear h_d,
+    simp_intro_aux new_S use_ns ns
+  else if t^.is_pi || t^.is_let then
+    intro1_aux use_ns ns >> simp_intro_aux S use_ns ns^.tail
+  else do
+    new_t ← whnf t reducible,
+    if new_t^.is_pi then change new_t >> simp_intro_aux S use_ns ns
+    else return ()
+
+meta def simp_intros_using (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit :=
+simp_intro_aux cfg ff s ff []
+
+meta def simph_intros_using (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit :=
+do s ← collect_ctx_simps >>= s^.append,
+   simp_intro_aux cfg tt s ff []
+
+meta def simp_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit :=
+simp_intro_aux cfg ff s tt ns
+
+meta def simph_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simplify_config := {}) : tactic unit :=
+do s ← collect_ctx_simps >>= s^.append,
+   simp_intro_aux cfg tt s tt ns
+
 meta def simp_at (h : expr) (extra_lemmas : list expr := []) (cfg : simplify_config := {}) : tactic unit :=
 do when (expr.is_local_constant h = ff) (fail "tactic simp_at failed, the given expression is not a hypothesis"),
    htype ← infer_type h,