fix(library/tactic/rewrite_tactic): type check rewriting steps

closes #550

hott/cubical/square.hlean

@@ -103,15 +103,20 @@ namespace cubical
     from eq.rec_on p (by cases r; cases t; exact H),
   left_inv (to_fun !square_equiv_eq) s ▹ !con_inv_cancel_right ▹ H2
 
-  definition rec_on_t {a₁₀ : A}
-    {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type}
+  definition rec_on_t.{l} {A : Type.{l}} {a₁₀ : A}
+    {P : Π {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}, square idp b l r → Type.{l}}
     {a₀₂ a₂₂ : A} {b : a₀₂ = a₂₂} {l : a₁₀ = a₀₂} {r : a₁₀ = a₂₂}
       (s : square idp b l r) (H : P ids) : P s :=
   let p : l ⬝ b = r := (eq_of_square s)⁻¹ ⬝ !idp_con in
   assert H2 : P (square_of_eq ((p ⬝ !idp_con⁻¹)⁻¹)),
     from eq.rec_on p (by cases b; cases l; exact H),
-  by rewrite [con_inv_cancel_right at H2, inv_inv at H2];
-     exact (left_inv (to_fun !square_equiv_eq) s ▹ H2)
+  assert H3 : P (square_of_eq ((eq_of_square s)⁻¹⁻¹)),
+    from eq.rec_on !con_inv_cancel_right H2,
+  assert H4 : P (square_of_eq (eq_of_square s)),
+    from eq.rec_on !inv_inv H3,
+  proof
+    left_inv (to_fun !square_equiv_eq) s ▹ H4
+  qed
 
   definition rec_on_tb {a : A}
     {P : Π{b : A} {l : a = b} {r : a = b}, square idp idp l r → Type}

src/library/tactic/rewrite_tactic.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
+#include "kernel/kernel_exception.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/default_converter.h"
 #include "kernel/inductive/inductive.h"
@@ -1169,6 +1170,10 @@ class rewrite_fn {
         }
     }
 
+    void check_term(expr const & H) {
+        type_checker(m_env).check_ignore_undefined_universes(H);
+    }
+
     bool process_rewrite_hypothesis(expr const & hyp, expr const & orig_elem, expr const & pattern, occurrence const & occ) {
         add_target(hyp, true);
         expr Pa = mlocal_type(hyp);
@@ -1214,7 +1219,9 @@ class rewrite_fn {
             expr new_mvar = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
             expr new_meta = mk_app(new_mvar, new_hyps);
             goal new_g(new_meta, new_type);
-            assign(m_subst, m_g, mk_app(new_mvar, args));
+            expr V = mk_app(new_mvar, args);
+            check_term(V);
+            assign(m_subst, m_g, V);
             update_goal(new_g);
             return true;
         }
@@ -1247,7 +1254,7 @@ class rewrite_fn {
             } else {
                 H          = mk_app({mk_constant(get_eq_rec_name(), {l1, l2}), A, b, mk_lambda("x", A, Px), M, a, Heq});
             }
-
+            check_term(H);
             goal new_g(M, Pb);
             assign(m_subst, m_g, H);
             update_goal(new_g);
@@ -1404,6 +1411,33 @@ class rewrite_fn {
         }
     }
 
+    void process_failure(expr const & elem, bool type_error) {
+        if (m_ps.report_failure()) {
+            proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen);
+            if (!m_use_trace || !m_trace_initialized) {
+                throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
+                                       [=](formatter const &) {
+                                           if (type_error)
+                                               return format("invalid 'rewrite' tactic, rewrite step produced type incorrect term");
+                                           else
+                                               return format("invalid 'rewrite' tactic, rewrite step failed");
+                                       });
+            } else {
+                trace saved_trace = m_trace;
+                throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
+                                       [=](formatter const & fmt) {
+                                           format r;
+                                           if (type_error)
+                                               r += format("invalid 'rewrite' tactic, step produced type incorrect term, details: ");
+                                           else
+                                               r += format("invalid 'rewrite' tactic, ");
+                                           r += saved_trace.pp(fmt);
+                                           return r;
+                                       });
+            }
+        }
+    }
+
 public:
     rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps):
         m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()),
@@ -1423,22 +1457,13 @@ public:
     proof_state_seq operator()(buffer<expr> const & elems) {
         for (expr const & elem : elems) {
             flet<expr> set1(m_expr_loc, elem);
-            if (!process_step(elem)) {
-                if (m_ps.report_failure()) {
-                    proof_state curr_ps(m_ps, cons(m_g, tail(m_ps.get_goals())), m_subst, m_ngen);
-                    if (!m_use_trace || !m_trace_initialized) {
-                        throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
-                                               [](formatter const &) { return format("invalid 'rewrite' tactic, rewrite step failed"); });
-                    } else {
-                        trace saved_trace = m_trace;
-                        throw tactic_exception("rewrite step failed", some_expr(elem), curr_ps,
-                                               [=](formatter const & fmt) {
-                                                   format r = format("invalid 'rewrite' tactic, ");
-                                                   r       += saved_trace.pp(fmt);
-                                                   return r;
-                                               });
-                    }
+            try {
+                if (!process_step(elem)) {
+                    process_failure(elem, false);
+                    return proof_state_seq();
                 }
+            } catch (kernel_exception &) {
+                process_failure(elem, true);
                 return proof_state_seq();
             }
         }

tests/lean/550.lean

@@ -0,0 +1,45 @@
+import algebra.function
+import logic.funext
+
+open function
+
+structure bijection (A : Type) :=
+(func finv : A → A)
+(linv : finv ∘ func = id)
+(rinv : func ∘ finv = id)
+
+attribute bijection.func [coercion]
+
+namespace bijection
+  variable {A : Type}
+
+  definition compose (f g : bijection A) : bijection A :=
+  bijection.mk
+    (f ∘ g)
+    (finv g ∘ finv f)
+    (by rewrite [compose.assoc, -{finv f ∘ _}compose.assoc, linv f, compose.left_id, linv g])
+    (by rewrite [-compose.assoc, {_ ∘ finv g}compose.assoc, rinv g, compose.right_id, rinv f])
+
+  infixr `∘b`:100 := compose
+
+  lemma compose.assoc (f g h : bijection A) : (f ∘b g) ∘b h = f ∘b (g ∘b h) := rfl
+
+  definition id : bijection A :=
+  bijection.mk id id (compose.left_id id) (compose.left_id id)
+
+  lemma id.left_id (f : bijection A) : id ∘b f = f :=
+  bijection.rec_on f (λx x x x, rfl)
+
+  lemma id.right_id (f : bijection A) : f ∘b id = f :=
+  bijection.rec_on f (λx x x x, rfl)
+
+  definition inv (f : bijection A) : bijection A :=
+  bijection.mk
+    (finv f)
+    (func f)
+    (rinv f)
+    (linv f)
+
+  lemma inv.linv (f : bijection A) : inv f ∘b f = id :=
+  bijection.rec_on f (λfunc finv linv rinv, by rewrite [↑inv, ↑compose, linv])
+end bijection

tests/lean/550.lean.expected.out

@@ -0,0 +1,32 @@
+550.lean:44:72: error:invalid 'rewrite' tactic, step produced type incorrect term, details: rewrite step failed using pattern
+  finv ∘ func
+proof state:
+A : Type,
+f : bijection A,
+func finv : A → A,
+linv : finv ∘ func = function.id,
+rinv : func ∘ finv = function.id
+⊢ mk (finv ∘ func) (finv ∘ func)
+    (eq.rec
+       (eq.rec
+          (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.left_id func)))
+             (eq.symm rinv))
+          (function.compose.assoc func finv func))
+       (eq.symm (function.compose.assoc finv func (finv ∘ func))))
+    (eq.rec
+       (eq.rec
+          (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.right_id finv)))
+             (eq.symm rinv))
+          (eq.symm (function.compose.assoc finv func finv)))
+       (function.compose.assoc (finv ∘ func) finv func)) = id
+550.lean:44:47: error: don't know how to synthesize placeholder
+A : Type,
+f : bijection A,
+func finv : A → A,
+linv : finv ∘ func = function.id,
+rinv : func ∘ finv = function.id
+⊢ inv (mk func finv linv rinv) ∘b mk func finv linv rinv = id
+550.lean:44:2: error: failed to add declaration 'bijection.inv.linv' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (A : Type) (f : …),
+    bijection.rec_on f (λ (func finv : …) (linv : …) (rinv : …), ?M_1)