feat(frontends/lean/parse_rewrite_tactic): change the semantics of rewrite[↑f] when f is recursive

After this commit it behaves like 'unfold f'.
That is, it will unfold f even if it fails to fold recursive
applications. Now, only 'esimp[f]' will not unfold f-applications when
it cannot fold the recursive applications.

This commit also closes #692. It is part of a series of commits that
addresses this issue.

closes #692

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -75,7 +75,7 @@ static expr parse_rewrite_unfold(parser & p, bool force_unfold) {
 // If use_paren is true, then lemmas must be identifiers or be wrapped with parenthesis
 static expr parse_rewrite_element(parser & p, bool use_paren) {
     if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) {
-        bool force_unfold = false;
+        bool force_unfold = true;
         return parse_rewrite_unfold(p, force_unfold);
     }
     if (p.curr_is_token(get_down_tk())) {

tests/lean/hott/unfold_test.hlean

@@ -0,0 +1,37 @@
+import algebra.e_closure
+
+open eq
+
+namespace relation
+section
+  parameters {A : Type}
+             (R : A → A → Type)
+
+  local abbreviation T := e_closure R
+
+  variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
+  parameter {R}
+
+  theorem ap_ap_e_closure_elim_h₁ {B C D : Type} {f : A → B}
+    {g : B → C} (h : C → D)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
+    : square (ap (ap h) (ap_e_closure_elim_h e p t))
+             (ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) t)
+             (ap_compose h g (e_closure.elim e t))⁻¹
+             (ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) :=
+  begin
+    induction t,
+    apply sorry,
+    apply sorry,
+    {
+      rewrite [↑e_closure.elim, ↑ap_e_closure_elim_h, ap_con (ap h)],
+      refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
+      rewrite [con_inv,inv_inv,-inv2_inv],
+      exact !ap_inv2 ⬝v square_inv2 v_0
+     },
+    apply sorry
+  end
+end
+end relation

tests/lean/run/unfold_test.lean

@@ -12,7 +12,7 @@ theorem last_concat {x : A} : ∀ {l : list A} (h : concat x l ≠ []), last (co
 
 theorem reverse_append : ∀ (s t : list A), reverse (s ++ t) = (reverse t) ++ (reverse s)
 | []         t2 :=
-  by rewrite [↑append, ↑reverse, append_nil_right]
+  by esimp [append, reverse]; rewrite append_nil_right
 | (a2 :: s2) t2 :=
   by rewrite [↑append, ↑reverse, reverse_append, concat_eq_append, append.assoc, -concat_eq_append]
 end