feat(library/init/meta): rename dsimp => rsimp, and add primitive tactic that takes an arbitrary simp_lemmas

library/init/meta/converter.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 Converter monad for building simplifiers.
 -/
 prelude
-import init.meta.tactic init.meta.simp_tactic init.meta.defeq_simp_tactic
+import init.meta.tactic init.meta.simp_tactic
 import init.meta.congr_lemma init.meta.match_tactic
 open tactic
 
@@ -85,8 +85,8 @@ meta def whnf_core (m : transparency) : conv unit :=
 meta def whnf : conv unit :=
 conv.whnf_core reducible
 
-meta def dsimp : conv unit :=
-λ r e, do n ← defeq_simp e, return ⟨(), n, none⟩
+meta def rsimp : conv unit :=
+λ r e, do s ← simp_lemmas.mk_default, n ← s^.rsimplify e, return ⟨(), n, none⟩
 
 meta def try (c : conv unit) : conv unit :=
 c <|> return ()

library/init/meta/default.lean

@@ -11,5 +11,5 @@ import init.meta.injection_tactic init.meta.relation_tactics init.meta.fun_info
 import init.meta.congr_lemma init.meta.match_tactic init.meta.ac_tactics
 import init.meta.backward init.meta.rewrite_tactic init.meta.unfold_tactic
 import init.meta.mk_dec_eq_instance init.meta.mk_inhabited_instance
-import init.meta.simp_tactic init.meta.defeq_simp_tactic init.meta.set_get_option_tactics
+import init.meta.simp_tactic init.meta.set_get_option_tactics
 import init.meta.interactive init.meta.converter

library/init/meta/defeq_simp_tactic.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.meta.tactic
-
-namespace tactic
-/- Simplify the given expression using [defeq] lemmas.
-   The resulting expression is definitionally equal to the input. -/
-meta constant defeq_simp_core : transparency → expr → tactic expr
-
-meta def defeq_simp : expr → tactic expr :=
-defeq_simp_core reducible
-
-meta def dsimp : tactic unit :=
-target >>= defeq_simp >>= change
-
-meta def dsimp_at (H : expr) : tactic unit :=
-do num_reverted : ℕ ← revert H,
-   (expr.pi n bi d b : expr) ← target | failed,
-   H_simp : expr ← defeq_simp d,
-   change $ expr.pi n bi H_simp b,
-   intron num_reverted
-
-end tactic

library/init/meta/interactive.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.meta.tactic init.meta.rewrite_tactic init.meta.simp_tactic
-import init.meta.defeq_simp_tactic
 
 namespace tactic
 namespace interactive
@@ -296,13 +295,13 @@ do s ← mk_simp_set attr_names hs ids,
    end,
    try tactic.triv, try tactic.reflexivity
 
-private meta def dsimp_hyps : location → tactic unit
+private meta def rsimp_hyps : location → tactic unit
 | []      := skip
-| (h::hs) := get_local h >>= dsimp_at
+| (h::hs) := get_local h >>= rsimp_at
 
-meta def dsimp : location → tactic unit
-| [] := tactic.dsimp
-| hs := dsimp_hyps hs
+meta def rsimp : location → tactic unit
+| [] := tactic.rsimp
+| hs := rsimp_hyps hs
 
 meta def reflexivity : tactic unit :=
 tactic.reflexivity

library/init/meta/simp_tactic.lean

@@ -59,6 +59,13 @@ simp_lemmas.rewrite_core reducible
    Fails if no simplifications can be performed. -/
 meta constant simp_lemmas.simplify_core : simp_lemmas → tactic unit → name → expr → tactic (expr × expr)
 
+/- Simplify the given expression using *only* reflexivity equality lemmas from the given set of lemmas.
+   The resulting expression is definitionally equal to the input. -/
+meta constant simp_lemmas.rsimplify_core : transparency → simp_lemmas → expr → tactic expr
+
+meta def simp_lemmas.rsimplify : simp_lemmas → expr → tactic expr :=
+simp_lemmas.rsimplify_core reducible
+
 namespace tactic
 
 meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
@@ -79,6 +86,18 @@ simplify_goal failed [] >> try triv >> try reflexivity
 meta def simp_using (Hs : list expr) : tactic unit :=
 simplify_goal failed Hs >> try triv
 
+meta def rsimp : tactic unit :=
+do S ← simp_lemmas.mk_default,
+   target >>= S^.rsimplify >>= change
+
+meta def rsimp_at (H : expr) : tactic unit :=
+do num_reverted : ℕ ← revert H,
+   (expr.pi n bi d b : expr) ← target | failed,
+   S      ← simp_lemmas.mk_default,
+   H_simp ← S^.rsimplify d,
+   change $ expr.pi n bi H_simp b,
+   intron num_reverted
+
 private meta def is_equation : expr → bool
 | (expr.pi n bi d b) := is_equation b
 | e                  := match (expr.is_eq e) with (some a) := tt | none := ff end

src/library/tactic/defeq_simplifier.cpp

@@ -16,6 +16,7 @@ Author: Daniel Selsam
 #include "library/defeq_canonizer.h"
 #include "library/vm/vm_expr.h"
 #include "library/tactic/tactic_state.h"
+#include "library/tactic/simp_lemmas_tactics.h"
 #include "library/tactic/defeq_simplifier.h"
 
 #ifndef LEAN_DEFAULT_DEFEQ_SIMPLIFY_MAX_SIMP_ROUNDS
@@ -302,11 +303,11 @@ expr defeq_simplify(type_context & ctx, simp_lemmas const & simp_lemmas, expr co
     return defeq_simplify_fn(ctx, simp_lemmas)(e);
 }
 
-vm_obj tactic_defeq_simp(vm_obj const & m, vm_obj const & e, vm_obj const & s0) {
+vm_obj simp_lemmas_rsimplify_core(vm_obj const & m, vm_obj const & _lemmas, vm_obj const & e, vm_obj const & s0) {
     type_context ctx = mk_type_context_for(s0, m);
     tactic_state const & s    = to_tactic_state(s0);
     LEAN_TACTIC_TRY;
-    simp_lemmas lemmas = get_default_simp_lemmas(s.env(), transparency_mode::Reducible);
+    simp_lemmas lemmas = to_simp_lemmas(_lemmas);
     expr new_e         = defeq_simplify(ctx, lemmas, to_expr(e));
     return mk_tactic_success(to_obj(new_e), s);
     LEAN_TACTIC_CATCH(s);
@@ -319,7 +320,7 @@ expr defeq_simplify(type_context & ctx, expr const & e) {
 
 /* Setup and teardown */
 void initialize_defeq_simplifier() {
-    DECLARE_VM_BUILTIN(name({"tactic", "defeq_simp_core"}), tactic_defeq_simp);
+    DECLARE_VM_BUILTIN(name({"simp_lemmas", "rsimplify_core"}), simp_lemmas_rsimplify_core);
 
     register_trace_class("defeq_simplifier");
     register_trace_class(name({"defeq_simplifier", "canonize"}));

tests/lean/change1.lean

@@ -8,7 +8,8 @@ example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
 by do intro `Heq,
       t  ← target,
       trace_state,
-      t' ← defeq_simp t,
+      s ← simp_lemmas.mk_default,
+      t' ← s^.rsimplify t,
       change t',
       trace "---- after change ----",
       trace_state,

tests/lean/change2.lean

@@ -8,7 +8,7 @@ example (a b : nat) : a = b → succ (succ a) = succ (b + 1) :=
 by do intro `Heq,
       get_local `a >>= subst,
       trace_state,
-      dsimp,
+      rsimp,
       trace "---- after dsimp ----",
       trace_state,
       t ← target,

tests/lean/defeq1.lean

@@ -8,6 +8,7 @@ rfl
 example (n m : nat) (H : succ (succ n) = succ m) : true :=
 by do H  ← get_local `H,
       t  ← infer_type H,
-      t' ← defeq_simp t,
+      s  ← simp_lemmas.mk_default,
+      t' ← s^.rsimplify t,
       trace t',
       exact (expr.const `trivial [])

tests/lean/defeq_simp1.lean

@@ -8,13 +8,15 @@ open tactic
 
 example (a b : nat) (H : @add nat (id (id nat.has_add)) a b = @add nat nat_has_add2 a b) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor
 
 
 example (a b : nat) (H : (λ x : nat, @add nat (id (id nat.has_add)) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor
 
 attribute [reducible]

tests/lean/defeq_simp2.lean

@@ -9,7 +9,8 @@ axiom foo3 (n : nat) : n ≥ 0
   -- by default we dont canonize proofs
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor
 
 set_option defeq_simplify.canonize_proofs true
@@ -18,18 +19,21 @@ constant x1 : nat -- update the environment to force defeq_canonize cache to be
 
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor
 
 constant x2 : nat -- update the environment to force defeq_canonize cache to be reset
 
 example (a b : nat) (H : f a (id (id (id (foo1 a)))) = f a (foo2 a)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor
 
 -- Example that does not work
 example (a b : nat) (H : (λ x, f x (id (id (id (foo1 x))))) = (λ x, f x (foo2 x))) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor

tests/lean/defeq_simp3.lean

@@ -11,5 +11,6 @@ set_option pp.all true
 
 example (a b : nat) (H : (λ x : nat, @add nat nat_has_add2 a x) = (λ x : nat, @add nat (nat_has_add3 x) a b)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor

tests/lean/defeq_simp4.lean

@@ -15,8 +15,9 @@ set_option pp.all true
 -- behavior.
 example (a b : nat) (H : (λ x : nat, @add nat (nat_has_add3 x) a b) = (λ x : nat, @add nat nat_has_add2 a x)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   trace "---------",
   -- The following should work
-  get_local `H >>= infer_type >>= defeq_simp >>= defeq_simp >>= trace,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= s^.rsimplify >>= trace,
   constructor

tests/lean/defeq_simp5.lean

@@ -16,5 +16,6 @@ example (a b : nat)
         (H : (λ x y : nat, @add nat (nat_has_add3 x) a b) =
              (λ x y : nat, @add nat (nat_has_add3 y) a x)) : true :=
 by do
-  get_local `H >>= infer_type >>= defeq_simp >>= trace,
+  s ← simp_lemmas.mk_default,
+  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
   constructor

tests/lean/run/cases_tac1.lean

@@ -25,7 +25,7 @@ by do
   w ← get_local `w,
   cases_using w [`n', `hw, `tw],
   trace_state,
-  dsimp,
+  rsimp,
   Heq1 ← intro1,
   Heq2 ← intro1,
   subst Heq1, subst Heq2,

tests/lean/run/converter.lean

@@ -17,7 +17,7 @@ by conversion $
   whnf >>
   trace_lhs >>
   apply_simp_set `bla >>
-  dsimp >>
+  rsimp >>
   trace "after defeq simplifier" >>
   trace_lhs >>
   change `(f a a) >>
@@ -34,7 +34,7 @@ by conversion $
   funext $ do
     trace_lhs,
     apply_simp_set `bla,
-    dsimp,
+    rsimp,
     apply_simp_set `foo
 
 constant h : nat → nat → nat
@@ -46,7 +46,7 @@ meta def conv.depth : conv unit → conv unit
 lemma ex (a : nat) : (λ a, h (f a (sizeof a)) (g a)) = (λ a, h 0 a) :=
 by conversion $
    depth_first $
-     (apply_simp_set `foo <|> apply_simp_set `bla <|> dsimp)
+     (apply_simp_set `foo <|> apply_simp_set `bla <|> rsimp)
 
 lemma ex2 {A : Type} [comm_group A] (a b : A) : b * 1 * a = a * b :=
 by conversion $

tests/lean/run/dsimp_at1.lean

@@ -8,6 +8,6 @@ noncomputable definition f (z : A) : A := z
 definition foo (z₁ z₂ : A) : f z₁ = f z₂ → z₁ = z₂ :=
 by do H ← intro `H,
       trace_state,
-      dsimp_at H,
+      rsimp_at H,
       trace_state,
       assumption

tests/lean/unfold_crash.lean

@@ -5,6 +5,6 @@ example (a b : nat) : a = succ b → a = b + 1 :=
 by do
   H ← intro `H,
   try (unfold_at [`nat.succ] H),
-  unfold [`add], dsimp, unfold [`nat.add],
+  unfold [`add], rsimp, unfold [`nat.add],
   trace_state,
   assumption