fix(library/tactic/rewrite_tactic): do not allow projections to be unfolded

fixes #1032

This is just a workaround. A better fix has been implemented in the
lean3 branch.

hott/types/arrow_2.hlean

@@ -68,7 +68,6 @@ namespace arrow
           ⬝ is_retraction.right_inverse_cod r (g a)))
       (fiber.mk a (refl (g a)))
       (is_retraction.right_inverse_dom r a), -- everything but this field should be inferred
-    unfold fiber.point_eq,
     rewrite [is_retraction.cohere r a],
     apply inv_con_cancel_right
   end

library/data/hf.lean

@@ -69,7 +69,7 @@ notation [priority finset.prio] a ∉ b := ¬ mem a b
 
 lemma insert_lt_of_not_mem {a s : hf} : a ∉ s → s < insert a s :=
 begin
-  unfold [insert, of_finset, equiv.to_fun, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
+  unfold [insert, of_finset, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
   intro h,
   rewrite [finset.to_nat_insert h],
   rewrite [to_nat_of_nat, -zero_add s at {1}],
@@ -80,7 +80,7 @@ end
 lemma insert_lt_insert_of_not_mem_of_not_mem_of_lt {a s₁ s₂ : hf}
       : a ∉ s₁ → a ∉ s₂ → s₁ < s₂ → insert a s₁ < insert a s₂ :=
 begin
-  unfold [insert, of_finset, equiv.to_fun, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
+  unfold [insert, of_finset, finset_nat_equiv_nat, mem, to_finset, equiv.inv],
   intro h₁ h₂ h₃,
   rewrite [finset.to_nat_insert h₁],
   rewrite [finset.to_nat_insert h₂, *to_nat_of_nat],

library/data/rat/basic.lean

@@ -97,7 +97,7 @@ definition smul (a : ℤ) (b : prerat) (H : a > 0) : prerat :=
 prerat.mk (a * num b) (a * denom b) (mul_pos H (denom_pos b))
 
 theorem of_int_add (a b : ℤ) : of_int (a + b) ≡ add (of_int a) (of_int b) :=
-by esimp [equiv, num, denom, one, add, of_int]; rewrite [*int.mul_one]
+by esimp [equiv, one, add, of_int]; rewrite [*int.mul_one]
 
 theorem of_int_mul (a b : ℤ) : of_int (a * b) ≡ mul (of_int a) (of_int b) :=
 !equiv.refl
@@ -114,7 +114,7 @@ definition inv : prerat → prerat
 | inv (prerat.mk -[1+n] d dp)       := prerat.mk (-d) (nat.succ n) !of_nat_succ_pos
 
 theorem equiv_zero_of_num_eq_zero {a : prerat} (H : num a = 0) : a ≡ zero :=
-by rewrite [↑equiv, H, ↑zero, ↑num, ↑of_int, *zero_mul]
+by rewrite [↑equiv, H, ↑zero, ↑of_int, *zero_mul]
 
 theorem num_eq_zero_of_equiv_zero {a : prerat} : a ≡ zero → num a = 0 :=
 by rewrite [↑equiv, ↑zero, ↑of_int, mul_one, zero_mul]; intro H; exact H
@@ -256,7 +256,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on
       calc
         mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_neg an_neg adp)
                   ... ≡ one      : begin
-                                     esimp [equiv, num, denom, one, mul, of_int],
+                                     esimp [equiv, one, mul, of_int],
                                      rewrite [*int.mul_one, *int.one_mul, mul.comm,
                                               neg_mul_comm]
                                    end)
@@ -266,7 +266,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on
       calc
         mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_pos an_pos adp)
                   ... ≡ one      : begin
-                                     esimp [equiv, num, denom, one, mul, of_int],
+                                     esimp [equiv, one, mul, of_int],
                                      rewrite [*int.mul_one, *int.one_mul, mul.comm]
                                    end)
 

src/library/tactic/rewrite_tactic.cpp

@@ -644,6 +644,10 @@ class rewrite_fn {
         // TODO(Leo): should we add add an option that will not try to fold recursive applications
         if (to_unfold) {
             lean_assert(occs);
+            for (name const & n : to_unfold) {
+                if (is_projection(m_env, n))
+                    throw_rewrite_exception(sstream() << "invalid 'unfold', '" << n << "' is a projection");
+            }
             auto new_e = unfold_rec(m_env, force_unfold, e, to_unfold, *occs);
             if (!new_e)
                 return none_expr();