fix(library/tactic/dsimplify): make sure dsimp only unfold reducible constants when matching

fixes #1327

src/library/tactic/dsimplify.cpp

@@ -311,7 +311,7 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
                              vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     try {
-        type_context ctx = mk_type_context_for(s);
+        type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs = s.dcs();
         tactic_dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
                               to_bool(visit_instances), a, pre, post);
@@ -327,7 +327,7 @@ vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit
                                   vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     try {
-        type_context ctx    = mk_type_context_for(s);
+        type_context ctx    = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs = s.dcs();
         simp_lemmas_for dlemmas;
         if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))

tests/lean/1327.lean

@@ -0,0 +1,4 @@
+example (n) : nat.pred n = n :=
+begin
+  dsimp
+end

tests/lean/1327.lean.expected.out

@@ -0,0 +1,4 @@
+1327.lean:4:0: error: tactic failed, there are unsolved goals
+state:
+n : ℕ
+⊢ nat.pred n = n

tests/lean/defeq_simp1.lean

@@ -1,6 +1,6 @@
-attribute [reducible]
-definition nat_has_add2 : has_add nat :=
-has_add.mk (λ x y : nat, x + y)
+@[reducible]
+def nat_has_add2 : has_add nat :=
+⟨λ x y : nat, nat.add x y⟩
 
 set_option pp.all true
 

tests/lean/run/destruct.lean

@@ -25,6 +25,6 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
 begin
   intro n,
   destruct n,
-   dsimp, intros, note h := lt_irrefl 0, cc,
-   dsimp, intros, subst n
+   {dsimp, intros, note h := lt_irrefl 0, cc},
+   {intros, subst n, dsimp, reflexivity}
 end