fix(library/tactic/subst_tactic): bug in 'subst' tactic

src/library/tactic/subst_tactic.cpp

@@ -52,6 +52,11 @@ optional<proof_state> subst(environment const & env, name const & h_name, bool s
         std::swap(lhs, rhs);
     if (!is_local(lhs))
         return none_proof_state();
+    if (depends_on(rhs, lhs)) {
+        throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, '" << lhs
+                                          << "' occurs in the other side of the equation");
+        return none_proof_state();
+    }
     buffer<expr> hyps, deps, non_deps;
     g.get_hyps(hyps);
     bool depends_on_h = depends_on(g.get_type(), h);
@@ -181,9 +186,9 @@ tactic mk_subst_tactic(list<name> const & ids) {
             for (expr const & H : hyps) {
                 expr lhs, rhs;
                 if (is_eq(mlocal_type(H), lhs, rhs)) {
-                    if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x)) {
+                    if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x) && !depends_on(rhs, lhs)) {
                         return apply_rewrite(H, false);
-                    } else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x)) {
+                    } else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x) && !depends_on(lhs, rhs)) {
                         return apply_rewrite(H, true);
                     }
                 }

tests/lean/subst_bug.lean

@@ -0,0 +1,14 @@
+example (f : nat → nat) (a b : nat) : f a = a → f (f a) = a :=
+begin
+  intro h₁,
+  subst h₁ -- ERROR
+end
+
+open nat
+
+example (f : nat → nat) (a b : nat) : f a = a → a = 0 → f (f a) = a :=
+begin
+  intro h₁ h₂,
+  subst a, -- should use h₂
+  rewrite +h₁
+end

tests/lean/subst_bug.lean.expected.out

@@ -0,0 +1,13 @@
+subst_bug.lean:4:2: error:invalid 'subst' tactic, 'a' occurs in the other side of the equation
+proof state:
+f : nat → nat,
+a b : nat,
+h₁ : f a = a
+⊢ f (f a) = a
+subst_bug.lean:5:0: error: don't know how to synthesize placeholder
+f : nat → nat,
+a b : nat
+⊢ f a = a → f (f a) = a
+subst_bug.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1