From 7accd0f1e6bd56dc6b5211a5850fc27e024196dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Mar 2015 18:07:55 -0700
Subject: [PATCH] feat(library/tactic/rewrite_tactic): allow rewrite with terms
 that contains binders

see discussion at #470
---
 hott/types/fiber.hlean                | 6 ++----
 src/library/tactic/rewrite_tactic.cpp | 5 ++++-
 tests/lean/hott/rw_binders.hlean      | 9 +++++++++
 3 files changed, 15 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/hott/rw_binders.hlean

diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean
index 8a88671fb0..0658f0ae52 100644
--- a/hott/types/fiber.hlean
+++ b/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
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index a688a4d3b1..8f543de018 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/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);
diff --git a/tests/lean/hott/rw_binders.hlean b/tests/lean/hott/rw_binders.hlean
new file mode 100644
index 0000000000..48052ee2a6
--- /dev/null
+++ b/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