feat(library/init/meta): rename rsimp* back to dsimp*

library/init/meta/converter.lean

@@ -85,8 +85,8 @@ meta def whnf_core (m : transparency) : conv unit :=
 meta def whnf : conv unit :=
 conv.whnf_core reducible
 
-meta def rsimp : conv unit :=
-λ r e, do s ← simp_lemmas.mk_default, n ← s^.rsimplify e, return ⟨(), n, none⟩
+meta def dsimp : conv unit :=
+λ r e, do s ← simp_lemmas.mk_default, n ← s^.dsimplify e, return ⟨(), n, none⟩
 
 meta def try (c : conv unit) : conv unit :=
 c <|> return ()

library/init/meta/interactive.lean

@@ -295,13 +295,13 @@ do s ← mk_simp_set attr_names hs ids,
    end,
    try tactic.triv, try tactic.reflexivity
 
-private meta def rsimp_hyps : location → tactic unit
+private meta def dsimp_hyps : location → tactic unit
 | []      := skip
-| (h::hs) := get_local h >>= rsimp_at
+| (h::hs) := get_local h >>= dsimp_at
 
-meta def rsimp : location → tactic unit
-| [] := tactic.rsimp
-| hs := rsimp_hyps hs
+meta def dsimp : location → tactic unit
+| [] := tactic.dsimp
+| hs := dsimp_hyps hs
 
 meta def reflexivity : tactic unit :=
 tactic.reflexivity

library/init/meta/simp_tactic.lean

@@ -59,14 +59,35 @@ 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.
+/- (Definitional) 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 constant simp_lemmas.dsimplify_core : transparency → simp_lemmas → expr → tactic expr
 
-meta def simp_lemmas.rsimplify : simp_lemmas → expr → tactic expr :=
-simp_lemmas.rsimplify_core reducible
+meta def simp_lemmas.dsimplify : simp_lemmas → expr → tactic expr :=
+simp_lemmas.dsimplify_core reducible
 
 namespace tactic
+meta constant dsimplify_core
+  (max_steps       : nat)
+  /- If visit_instances = ff, then instance implicit arguments are not visited, but
+     tactic will canonize them. -/
+  (visit_instances : bool)
+  /- (pre e) is invoked before visiting the children of subterm 'e',
+     if it succeeds the result is a new expression that must be definitionally equal to 'e',
+     and a flag indicating whether the new children should be visited or not. -/
+  (pre             : expr → tactic (expr × bool))
+  /- (post e) is invoked after visiting the children of subterm 'e',
+     if it succeeds the result is a new expression that must be definitionally equal to 'e',
+     and a flag indicating whether the new children should be revisited.
+     Remark: if (pre e) returns (some (new_e, ff)), then post is not invoked for new_e. -/
+  (post            : expr → tactic (expr × bool))
+  : expr → tactic expr
+
+meta def dsimplify
+  (pre             : expr → tactic (expr × bool))
+  (post            : expr → tactic (expr × bool))
+  : expr → tactic expr :=
+dsimplify_core 1000000 ff pre post
 
 meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
 do lemmas       ← simp_lemmas.mk_default,
@@ -86,15 +107,15 @@ 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 :=
+meta def dsimp : tactic unit :=
 do S ← simp_lemmas.mk_default,
-   target >>= S^.rsimplify >>= change
+   target >>= S^.dsimplify >>= change
 
-meta def rsimp_at (H : expr) : tactic unit :=
+meta def dsimp_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,
+   H_simp ← S^.dsimplify d,
    change $ expr.pi n bi H_simp b,
    intron num_reverted
 

src/library/tactic/defeq_simplifier.cpp

@@ -303,7 +303,7 @@ expr defeq_simplify(type_context & ctx, simp_lemmas const & simp_lemmas, expr co
     return defeq_simplify_fn(ctx, simp_lemmas)(e);
 }
 
-vm_obj simp_lemmas_rsimplify_core(vm_obj const & m, vm_obj const & _lemmas, vm_obj const & e, vm_obj const & s0) {
+vm_obj simp_lemmas_dsimplify_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;
@@ -320,7 +320,7 @@ expr defeq_simplify(type_context & ctx, expr const & e) {
 
 /* Setup and teardown */
 void initialize_defeq_simplifier() {
-    DECLARE_VM_BUILTIN(name({"simp_lemmas", "rsimplify_core"}), simp_lemmas_rsimplify_core);
+    DECLARE_VM_BUILTIN(name({"simp_lemmas", "dsimplify_core"}), simp_lemmas_dsimplify_core);
 
     register_trace_class("defeq_simplifier");
     register_trace_class(name({"defeq_simplifier", "canonize"}));

tests/lean/change1.lean

@@ -9,7 +9,7 @@ by do intro `Heq,
       t  ← target,
       trace_state,
       s ← simp_lemmas.mk_default,
-      t' ← s^.rsimplify t,
+      t' ← s^.dsimplify 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,
-      rsimp,
+      dsimp,
       trace "---- after dsimp ----",
       trace_state,
       t ← target,

tests/lean/defeq1.lean

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

tests/lean/defeq_simp1.lean

@@ -9,14 +9,14 @@ 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 attribute [reducible]

tests/lean/defeq_simp2.lean

@@ -10,7 +10,7 @@ axiom foo3 (n : nat) : n ≥ 0
 example (a b : nat) (H : f a (foo1 a) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 set_option defeq_simplify.canonize_proofs true
@@ -20,7 +20,7 @@ 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor
 
 constant x2 : nat -- update the environment to force defeq_canonize cache to be reset
@@ -28,12 +28,12 @@ constant x2 : nat -- update the environment to force defeq_canonize cache to be
 example (a b : nat) (H : f a (id (id (id (foo1 a)))) = f a (foo2 a)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor

tests/lean/defeq_simp3.lean

@@ -12,5 +12,5 @@ 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   constructor

tests/lean/defeq_simp4.lean

@@ -16,8 +16,8 @@ set_option pp.all true
 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
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= trace,
   trace "---------",
   -- The following should work
-  get_local `H >>= infer_type >>= s^.rsimplify >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= s^.dsimplify >>= trace,
   constructor

tests/lean/defeq_simp5.lean

@@ -17,5 +17,5 @@ example (a b : nat)
              (λ x y : nat, @add nat (nat_has_add3 y) a x)) : true :=
 by do
   s ← simp_lemmas.mk_default,
-  get_local `H >>= infer_type >>= s^.rsimplify >>= trace,
+  get_local `H >>= infer_type >>= s^.dsimplify >>= 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,
-  rsimp,
+  dsimp,
   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 >>
-  rsimp >>
+  dsimp >>
   trace "after defeq simplifier" >>
   trace_lhs >>
   change `(f a a) >>
@@ -34,7 +34,7 @@ by conversion $
   funext $ do
     trace_lhs,
     apply_simp_set `bla,
-    rsimp,
+    dsimp,
     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 <|> rsimp)
+     (apply_simp_set `foo <|> apply_simp_set `bla <|> dsimp)
 
 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,
-      rsimp_at H,
+      dsimp_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], rsimp, unfold [`nat.add],
+  unfold [`add], dsimp, unfold [`nat.add],
   trace_state,
   assumption