feat(library/tactic/rewrite_tactic): allow rewrite with terms that contains binders

see discussion at #470

hott/types/fiber.hlean

@@ -28,8 +28,6 @@ namespace fiber
     {intro x, cases x, apply idp},
     {intro x, cases x, apply idp},
   end
-  --set_option pp.notation false
-
 
   definition equiv_fiber_eq (x y : fiber f b)
     : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
@@ -41,13 +39,13 @@ namespace fiber
     apply sigma_equiv_sigma_id,
     intro p,
     apply equiv_of_equiv_of_eq,
-      {apply (ap (λx, x = _)), apply transport_eq_Fl},
+    rotate 1,
     apply inv_con_eq_equiv_eq_con,
+    {apply (ap (λx, x = _)), rewrite transport_eq_Fl}
   end
 
   definition eq_mk {x y : fiber f b} (p : point x = point y) (q : point_eq x = ap f p ⬝ point_eq y)
     : x = y :=
   to_inv !equiv_fiber_eq ⟨p, q⟩
 
-
 end fiber

src/library/tactic/rewrite_tactic.cpp

@@ -759,7 +759,10 @@ class rewrite_fn {
                 if (!has_metavar(e)) {
                     return some_expr(e); // done
                 } else if (is_binding(e)) {
-                    throw_rewrite_exception("invalid rewrite tactic, pattern contains binders");
+                    unsigned next_idx = m_esubst.size();
+                    expr r = mk_idx_meta(next_idx, m_tc->infer(e).first);
+                    m_esubst.push_back(none_expr());
+                    return some_expr(r);
                 } else if (is_meta(e)) {
                     if (auto it = emap.find(e)) {
                         return some_expr(*it);

tests/lean/hott/rw_binders.hlean

@@ -0,0 +1,9 @@
+import types.eq
+open eq
+
+variables {A : Type} {a1 a2 a3 : A}
+definition my_transport_eq_l (p : a1 = a2) (q : a1 = a3)
+    : transport (λx, x = a3) p q = p⁻¹ ⬝ q :=
+begin
+  rewrite transport_eq_l,
+end