feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution

library/data/fintype.lean

@@ -78,7 +78,7 @@ definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : d
   match h₁ with
   | fintype.mk e u c :=
     match find_discr f g e with
-    | some a := λ h : find_discr f g e = some a, inr (λ f_eq_g : f = g, absurd (by rewrite f_eq_g) (ne_of_find_discr_eq_some h))
+    | some a := λ h : find_discr f g e = some a, inr (λ f_eq_g : f = g, absurd (by rewrite f_eq_g; reflexivity) (ne_of_find_discr_eq_some h))
     | none   := λ h : find_discr f g e = none, inl (show f = g, from funext (λ a : A, all_eq_of_find_discr_eq_none h a (c a)))
     end rfl
   end

library/data/list/perm.lean

@@ -104,7 +104,7 @@ theorem perm_cons_app (a : A) : ∀ (l : list A), (a::l) ~ (l ++ [a])
 
 theorem perm_app_comm {l₁ l₂ : list A} : (l₁++l₂) ~ (l₂++l₁) :=
 list.induction_on l₁
-  (by rewrite [append_nil_right, append_nil_left]; apply refl)
+  (by rewrite [append_nil_right, append_nil_left])
   (λ a t r, calc
     a::(t++l₂) ~ a::(l₂++t)   : skip a r
           ...  ~ l₂++t++[a]   : perm_cons_app
@@ -166,7 +166,7 @@ theorem perm_erase [H : decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l →
 | []     h := absurd h !not_mem_nil
 | (x::t) h :=
   by_cases
-    (assume aeqx  : a = x, by rewrite [aeqx, erase_cons_head]; exact !perm.refl)
+    (assume aeqx  : a = x, by rewrite [aeqx, erase_cons_head])
     (assume naeqx : a ≠ x,
       have aint : a ∈ t,             from mem_of_ne_of_mem naeqx h,
       have aux : t ~ a :: erase a t, from perm_erase aint,
@@ -185,11 +185,11 @@ assume p, perm.induction_on p
     by_cases
       (assume aeqx : a = x,
         by_cases
-          (assume aeqy  : a = y, by rewrite [-aeqx, -aeqy]; exact !perm.refl)
+          (assume aeqy  : a = y, by rewrite [-aeqx, -aeqy])
-          (assume naeqy : a ≠ y, by rewrite [-aeqx, erase_cons_tail _ naeqy, *erase_cons_head]; exact !perm.refl))
+          (assume naeqy : a ≠ y, by rewrite [-aeqx, erase_cons_tail _ naeqy, *erase_cons_head]))
       (assume naeqx : a ≠ x,
         by_cases
-          (assume aeqy  : a = y, by rewrite [-aeqy, erase_cons_tail _ naeqx, *erase_cons_head]; exact !perm.refl)
+          (assume aeqy  : a = y, by rewrite [-aeqy, erase_cons_tail _ naeqx, *erase_cons_head])
           (assume naeqy : a ≠ y, by rewrite[erase_cons_tail _ naeqx, *erase_cons_tail _ naeqy, erase_cons_tail _ naeqx];
                                     exact !swap)))
   (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
@@ -595,19 +595,19 @@ include H
 
 theorem perm_union_left {l₁ l₂ : list A} (t₁ : list A) : l₁ ~ l₂ → (union l₁ t₁) ~ (union l₂ t₁) :=
 assume p, perm.induction_on p
-  (by rewrite [nil_union]; exact !refl)
+  (by rewrite [nil_union])
   (λ x l₁ l₂ p₁ r₁, by_cases
      (λ xint₁  : x ∈ t₁, by rewrite [*union_cons_of_mem _ xint₁]; exact r₁)
      (λ nxint₁ : x ∉ t₁, by rewrite [*union_cons_of_not_mem _ nxint₁]; exact (skip _ r₁)))
   (λ x y l, by_cases
     (λ yint  : y ∈ t₁, by_cases
       (λ xint  : x ∈ t₁,
-        by rewrite [*union_cons_of_mem _ xint, *union_cons_of_mem _ yint, *union_cons_of_mem _ xint]; exact !refl)
+        by rewrite [*union_cons_of_mem _ xint, *union_cons_of_mem _ yint, *union_cons_of_mem _ xint])
       (λ nxint : x ∉ t₁,
-        by rewrite [*union_cons_of_mem _ yint, *union_cons_of_not_mem _ nxint, union_cons_of_mem _ yint]; exact !refl))
+        by rewrite [*union_cons_of_mem _ yint, *union_cons_of_not_mem _ nxint, union_cons_of_mem _ yint]))
     (λ nyint : y ∉ t₁, by_cases
       (λ xint  : x ∈ t₁,
-        by rewrite [*union_cons_of_mem _ xint, *union_cons_of_not_mem _ nyint, union_cons_of_mem _ xint]; exact !refl)
+        by rewrite [*union_cons_of_mem _ xint, *union_cons_of_not_mem _ nyint, union_cons_of_mem _ xint])
       (λ nxint : x ∉ t₁,
         by rewrite [*union_cons_of_not_mem _ nxint, *union_cons_of_not_mem _ nyint, union_cons_of_not_mem _ nxint]; exact !swap)))
   (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
@@ -657,21 +657,18 @@ assume p, perm.induction_on p
         by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_mem _ yint, *inter_cons_of_mem _ xint];
            exact !swap)
       (λ nxint : x ∉ t₁,
-        by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint];
+        by rewrite [*inter_cons_of_mem _ yint, *inter_cons_of_not_mem _ nxint, inter_cons_of_mem _ yint]))
-           exact !refl))
     (λ nyint : y ∉ t₁, by_cases
       (λ xint  : x ∈ t₁,
-        by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint];
+        by rewrite [*inter_cons_of_mem _ xint, *inter_cons_of_not_mem _ nyint, inter_cons_of_mem _ xint])
-           exact !refl)
       (λ nxint : x ∉ t₁,
         by rewrite [*inter_cons_of_not_mem _ nxint, *inter_cons_of_not_mem _ nyint,
-                     inter_cons_of_not_mem _ nxint];
+                     inter_cons_of_not_mem _ nxint])))
-           exact !refl)))
   (λ l₁ l₂ l₃ p₁ p₂ r₁ r₂, trans r₁ r₂)
 
 theorem perm_inter_right (l : list A) {t₁ t₂ : list A} : t₁ ~ t₂ → (inter l t₁) ~ (inter l t₂) :=
 list.induction_on l
-  (λ p, by rewrite [*inter_nil]; exact !refl)
+  (λ p, by rewrite [*inter_nil])
   (λ x xs r p, by_cases
     (λ xint₁  : x ∈ t₁,
       assert xint₂ : x ∈ t₂, from mem_perm p xint₁,
@@ -748,7 +745,7 @@ assume p : l₁ ~ l₂, perm.induction_on p
 
 theorem perm_cross_product_right (l : list A) {t₁ t₂ : list B} : t₁ ~ t₂ → (cross_product l t₁) ~ (cross_product l t₂) :=
 list.induction_on l
-  (λ p, by rewrite [*nil_cross_product]; exact !perm.refl)
+  (λ p, by rewrite [*nil_cross_product])
   (λ a t r p,
     perm_app (perm_map _ p) (r p))
 

library/data/uprod.lean

@@ -20,13 +20,13 @@ take p, or.inl rfl
 
 private theorem eqv.symm [symm] {A : Type} : ∀ p₁ p₂ : A × A, p₁ ~ p₂ → p₂ ~ p₁ :=
 take p₁ p₂ h, or.elim h
-  (λ e, by rewrite e; reflexivity)
+  (λ e, by rewrite e)
   (λ e, begin esimp [eqv], rewrite [-e, swap_swap], right, reflexivity end)
 
 private theorem eqv.trans [trans] {A : Type} : ∀ p₁ p₂ p₃ : A × A, p₁ ~ p₂ → p₂ ~ p₃ → p₁ ~ p₃ :=
 take p₁ p₂ p₃ h₁ h₂, or.elim h₁
   (λ e₁₂,  or.elim h₂
-    (λ e₂₃,  by rewrite [e₁₂, e₂₃]; reflexivity)
+    (λ e₂₃,  by rewrite [e₁₂, e₂₃])
     (λ es₂₃, begin esimp [eqv], rewrite -es₂₃, right, congruence, assumption end))
   (λ es₁₂, or.elim h₂
     (λ e₂₃,  begin esimp [eqv], rewrite es₁₂, right, assumption end)

src/library/tactic/equivalence_tactics.cpp

@@ -11,13 +11,16 @@ Author: Leonardo de Moura
 #include "library/tactic/expr_to_tactic.h"
 
 namespace lean {
-static optional<name> get_goal_op(proof_state const & s) {
+// Remark: if no_meta == true, then return none if goal contains metavariables
+static optional<name> get_goal_op(proof_state const & s, bool no_meta = false) {
     goals const & gs = s.get_goals();
     if (empty(gs)) {
         throw_no_goal_if_enabled(s);
         return optional<name>();
     }
     goal const & g   = head(gs);
+    if (no_meta && has_metavar(g.get_type()))
+        return optional<name>();
     expr const & op  = get_app_fn(g.get_type());
     if (is_constant(op))
         return optional<name>(const_name(op));
@@ -25,9 +28,9 @@ static optional<name> get_goal_op(proof_state const & s) {
         return optional<name>();
 }
 
-tactic refl_tactic(elaborate_fn const & elab) {
+tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false) {
     auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
-        auto op = get_goal_op(s);
+        auto op = get_goal_op(s, no_meta);
         if (!op)
             return proof_state_seq();
         if (auto refl = get_refl_info(env, *op)) {

src/library/tactic/equivalence_tactics.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 namespace lean {
+tactic refl_tactic(elaborate_fn const & elab, bool no_meta = false);
 void initialize_equivalence_tactics();
 void finalize_equivalence_tactics();
 }

src/library/tactic/rewrite_tactic.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "library/tactic/rewrite_tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/class_instance_synth.h"
+#include "library/tactic/equivalence_tactics.h"
 
 // #define TRACE_MATCH_PLUGIN
 
@@ -1385,27 +1386,6 @@ class rewrite_fn {
         }
     }
 
-    bool check_trivial_goal() {
-        expr type = m_g.get_type();
-        if (is_eq(type) || (is_iff(type) && m_env.impredicative())) {
-            constraint_seq cs;
-            expr lhs = app_arg(app_fn(type));
-            expr rhs = app_arg(type);
-            if (m_unifier_tc->is_def_eq(lhs, rhs, justification(), cs) && !cs) {
-                expr H = is_eq(type) ? mk_refl(*m_tc, lhs) : mk_iff_refl(lhs);
-                assign(m_subst, m_g, H);
-                return true;
-            } else {
-                return false;
-            }
-        } else if (type == mk_true()) {
-            assign(m_subst, m_g, mk_constant(get_eq_intro_name()));
-            return true;
-        } else {
-            return false;
-        }
-    }
-
     class match_converter : public unfold_reducible_converter {
     public:
         match_converter(environment const & env, bool relax_main_opaque):
@@ -1501,11 +1481,7 @@ public:
             }
         }
 
-        goals new_gs;
+        goals new_gs = cons(m_g, tail(m_ps.get_goals()));
-        if (check_trivial_goal())
-            new_gs = tail(m_ps.get_goals());
-        else
-            new_gs = cons(m_g, tail(m_ps.get_goals()));
         proof_state new_ps(m_ps, new_gs, m_subst, m_ngen);
         return proof_state_seq(new_ps);
     }
@@ -1663,13 +1639,14 @@ void initialize_rewrite_tactic() {
                              !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg))
                              throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
                      }
-                     return mk_rewrite_tactic(elab, args);
+                     bool fail_if_metavars = true;
+                     return then(mk_rewrite_tactic(elab, args), try_tactic(refl_tactic(elab, fail_if_metavars)));
                  });
     register_tac(name{"tactic", "subst"},
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
                      buffer<name> ns;
                      get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
-                     return mk_subst_tactic(to_list(ns));
+                     return then(mk_subst_tactic(to_list(ns)), try_tactic(refl_tactic(elab)));
                  });
 }
 

src/library/tactic/tactic.h

@@ -62,6 +62,7 @@ inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1,
 /** \brief Return a tactic that applies \c t1, and if \c t1 returns the empty sequence of states, then applies \c t2. */
 tactic orelse(tactic const & t1, tactic const & t2);
 inline tactic operator||(tactic const & t1, tactic const & t2) { return orelse(t1, t2); }
+inline tactic try_tactic(tactic const & t) { return orelse(t, id_tactic()); }
 /** \brief Return a tactic that appies \c t, but using the additional set of options \c opts. */
 tactic using_params(tactic const & t, options const & opts);
 /**

tests/lean/revert_fail.lean.expected.out

@@ -13,12 +13,8 @@ revert_fail.lean:6:0: error: failed to add declaration '14.0' to environment, va
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (A : Type) (n : nat) (v : …),
     ?M_1
-revert_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+revert_fail.lean:11:2: error: tactic failed
-proof state:
 no goals
-revert_fail.lean:12:0: error: don't know how to synthesize placeholder
-n : nat
-⊢ n = n
 revert_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (n : nat),

tests/lean/rewrite_fail.lean.expected.out

@@ -15,12 +15,8 @@ rewrite_fail.lean:6:0: error: failed to add declaration '14.0' to environment, v
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a b : ℕ) (Ha : …) (Hb : …),
     ?M_1
-rewrite_fail.lean:11:2: error:invalid tactic, there are no goals to be solved
+rewrite_fail.lean:11:2: error: tactic failed
-proof state:
 no goals
-rewrite_fail.lean:12:0: error: don't know how to synthesize placeholder
-a : ℕ
-⊢ a = a
 rewrite_fail.lean:12:0: error: failed to add declaration '14.1' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   λ (a : ℕ),