From 2c70ca83a8d50966521d3c764bacb2632b1c3307 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 3 Mar 2016 14:18:20 -0800
Subject: [PATCH] refactor(frontends/lean/calc): remove '{}' notation for
 eq.subst in calc mode

---
 library/data/list/basic.lean    |  2 +-
 library/data/list/comb.lean     |  8 ++--
 library/data/nat/basic.lean     |  6 +--
 library/data/nat/div.lean       |  4 +-
 library/data/nat/sub.lean       |  4 +-
 library/init/funext.lean        |  2 +-
 library/init/logic.lean         |  4 +-
 library/logic/identities.lean   |  8 ++--
 src/frontends/lean/calc.cpp     | 27 ++-----------
 tests/lean/K_bug.lean           |  2 +-
 tests/lean/interactive/eq2.lean |  4 +-
 tests/lean/run/class4.lean      |  2 +-
 tests/lean/run/group3.lean      | 12 +++---
 tests/lean/run/group4.lean      |  4 +-
 tests/lean/run/group5.lean      | 10 ++---
 tests/lean/run/is_nil.lean      |  2 +-
 tests/lean/run/nat_bug5.lean    | 10 ++---
 tests/lean/run/nested_rec.lean  |  2 +-
 tests/lean/slow/list_elab2.lean | 72 +++++----------------------------
 19 files changed, 55 insertions(+), 130 deletions(-)

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index bd96fa248b..f1a671ffb8 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -405,7 +405,7 @@ list.rec_on l
       calc
         find x (y::l) = if x = y then 0 else succ (find x l) : !find_cons
                   ... = succ (find x l)                      : if_neg (and.elim_left this)
-                  ... = succ (length l)                      : {iH (and.elim_right this)}
+                  ... = succ (length l)                      : by rewrite (iH (and.elim_right this))
                   ... = length (y::l)                        : !length_cons⁻¹)
 
 lemma find_le_length : ∀ {a} {l : list T}, find a l ≤ length l
diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean
index 725a0aa470..a91f305979 100644
--- a/library/data/list/comb.lean
+++ b/library/data/list/comb.lean
@@ -70,11 +70,11 @@ theorem length_map [simp] (f : A → B) : ∀ l : list A, length (map f l) = len
   by rewrite (length_map l)
 
 theorem map_ne_nil_of_ne_nil (f : A → B) {l : list A} (H : l ≠ nil) : map f l ≠ nil :=
-suppose map f l = nil,
+suppose h₁ : map f l = nil,
 have length (map f l) = length l, from !length_map,
 have 0 = length l, from calc
-     0 = length nil  : length_nil
-   ... = length (map f l) : {eq.symm `map f l = nil`}
+     0 = length (@nil B)  : length_nil
+   ... = length (map f l) : by rewrite h₁
    ... = length l : this,
 have l = nil, from eq_nil_of_length_eq_zero (eq.symm this),
 H this
@@ -369,7 +369,7 @@ theorem length_mapAccumR
   length (pr₂ (mapAccumR f x s)) = length x
 | f (a::x) s := calc
   length (pr₂ (mapAccumR f (a::x) s))
-                = length x + 1              : { length_mapAccumR f x s }
+                = length x + 1              : by rewrite -(length_mapAccumR f x s)
             ... = length (a::x)             : rfl
 | f [] s := calc
   length (pr₂ (mapAccumR f [] s))
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index f2af9cc46f..37c7790981 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -30,16 +30,16 @@ nat.induction_on x
     rfl
     (λ y₁ ih, calc
       0 + succ y₁ = succ (0 + y₁)  : rfl
-           ...    = succ (0 ⊕ y₁) : {ih}
+           ...    = succ (0 ⊕ y₁) : by rewrite ih
            ...    = 0 ⊕ (succ y₁) : rfl))
   (λ x₁ ih₁ y, nat.induction_on y
     (calc
       succ x₁ + 0  = succ (x₁ + 0)  : rfl
-               ... = succ (x₁ ⊕ 0) : {ih₁ 0}
+               ... = succ (x₁ ⊕ 0) : by rewrite (ih₁ 0)
                ... = succ x₁ ⊕ 0   : rfl)
     (λ y₁ ih₂, calc
       succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
-                   ...  = succ (succ x₁ ⊕ y₁) : {ih₂}
+                   ...  = succ (succ x₁ ⊕ y₁) : by rewrite ih₂
                    ...  = succ x₁ ⊕ succ y₁   : addl_succ_right))
 
 /- successor and predecessor -/
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index eff3a6afcf..630036d98d 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -43,7 +43,7 @@ theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = succ (x / z
 calc
   (x + z) / z = if 0 < z ∧ z ≤ x + z then (x + z - z) / z + 1 else 0 : !div_def
             ... = (x + z - z) / z + 1 : if_pos (and.intro H (le_add_left z x))
-            ... = succ (x / z)        : {!nat.add_sub_cancel}
+            ... = succ (x / z)        : by rewrite nat.add_sub_cancel
 
 theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) / x = succ (z / x) :=
 !add.comm ▸ !add_div_self H
@@ -551,7 +551,7 @@ calc
                by rewrite [mul.comm m, nat.mul_sub_right_distrib]
      ... = ((n - k / m - 1) * m + m - (k % m + 1)) / m            :
                by rewrite [H3 at {1}, right_distrib, nat.one_mul]
-     ... = ((n - k / m - 1) * m + (m - (k % m + 1))) / m          : {nat.add_sub_assoc H5 _}
+     ... = ((n - k / m - 1) * m + (m - (k % m + 1))) / m          : by rewrite (nat.add_sub_assoc H5 _)
      ... = (m - (k % m + 1)) / m + (n - k / m - 1)                :
                by rewrite [add.comm, (add_mul_div_self H4)]
      ... = n - k / m - 1                                          :
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index b850b62085..dc2999953a 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -303,7 +303,7 @@ by substvars; rewrite [↑dist, *nat.sub_self, add_zero]
 
 theorem dist_eq_sub_of_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
 calc
-  dist n m = 0 + (m - n) : {sub_eq_zero_of_le H}
+  dist n m = 0 + (m - n) : by rewrite -(sub_eq_zero_of_le H)
        ... = m - n       : zero_add
 
 theorem dist_eq_sub_of_lt {n m : ℕ} (H : n < m) : dist n m = m - n :=
@@ -337,7 +337,7 @@ begin rewrite [add.comm k n, add.comm k m]; apply dist_add_add_right end
 
 theorem dist_add_eq_of_ge {n m : ℕ} (H : n ≥ m) : dist n m + m = n :=
 calc
-  dist n m + m = n - m + m : {dist_eq_sub_of_ge H}
+  dist n m + m = n - m + m : by rewrite (dist_eq_sub_of_ge H)
            ... = n         : nat.sub_add_cancel H
 
 theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=
diff --git a/library/init/funext.lean b/library/init/funext.lean
index 761feefe91..4c74ae19ad 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -52,7 +52,7 @@ section
   theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
   assume H, calc
      f₁ = extfun_app ⟦f₁⟧ : rfl
-    ... = extfun_app ⟦f₂⟧ : {sound H}
+    ... = extfun_app ⟦f₂⟧ : by rewrite (@sound _ _ f₁ f₂ H)
     ... = f₂              : rfl
 end
 
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 947bd4e4a3..f29e1cd448 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -229,8 +229,8 @@ of_eq_true (eq_of_heq H)
 
 theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a
 | A A A (eq.refl A) (eq.refl A) a := calc
-  eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a              : rfl
-            ...             = (eq.refl A ⬝ eq.refl A) ▹ a : {proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A)}
+  eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a               : rfl
+            ...             = (eq.refl A ⬝ eq.refl A) ▹ a : by rewrite (proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A))
 
 theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ :=
 eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 9c418a47db..3f8eb4c8a4 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -12,13 +12,13 @@ open decidable
 theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
   (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc
-    ... ↔ a ∨ (c ∨ b)       : {or.comm}
+    ... ↔ a ∨ (c ∨ b)       : by rewrite (@or.comm b c)
      ... ↔ (a ∨ c) ∨ b      : iff.symm or.assoc
 
 theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
 calc
   (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc
-    ... ↔ a ∧ (c ∧ b)       : {and.comm}
+    ... ↔ a ∧ (c ∧ b)       : by rewrite (@and.comm b c)
      ... ↔ (a ∧ c) ∧ b      : iff.symm and.assoc
 
 theorem or_not_self_iff (a : Prop) [D : decidable a] : a ∨ ¬ a ↔ true :=
@@ -70,9 +70,9 @@ iff.intro
 theorem not_implies_iff_and_not (a b : Prop) [Da : decidable a] :
   ¬(a → b) ↔ a ∧ ¬b :=
 calc
-  ¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or a b}
+  ¬(a → b) ↔ ¬(¬a ∨ b) : by rewrite (imp_iff_not_or a b)
        ... ↔ ¬¬a ∧ ¬b  : not_or_iff_not_and_not
-       ... ↔ a ∧ ¬b    : {not_not_iff a}
+       ... ↔ a ∧ ¬b    : by rewrite (not_not_iff a)
 
 theorem and_not_of_not_implies {a b : Prop} [Da : decidable a] (H : ¬ (a → b)) : a ∧ ¬ b :=
 iff.mp !not_implies_iff_and_not H
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index 2931fb7ba6..249a8758ae 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -88,31 +88,10 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
 
 static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
     steps.clear();
-    auto pos = p.pos();
     p.check_token_next(get_colon_tk(), "invalid 'calc' expression, ':' expected");
-    if (p.curr_is_token(get_lcurly_tk())) {
-        p.next();
-        environment const & env = p.env();
-        expr pr = p.parse_expr();
-        p.check_token_next(get_rcurly_tk(), "invalid 'calc' expression, '}' expected");
-        for (auto const & pred : preds) {
-            if (auto refl_it = get_refl_extra_info(env, pred_op(pred))) {
-                if (auto subst_it = get_subst_extra_info(env, pred_op(pred))) {
-                    expr refl     = mk_op_fn(p, refl_it->m_name, refl_it->m_num_args-1, pos);
-                    expr refl_pr  = p.mk_app(refl, pred_lhs(pred), pos);
-                    expr subst    = mk_op_fn(p, subst_it->m_name, subst_it->m_num_args-2, pos);
-                    expr subst_pr = p.mk_app({subst, pr, refl_pr}, pos);
-                    steps.emplace_back(pred, subst_pr);
-                }
-            }
-        }
-        if (steps.empty())
-            throw parser_error("invalid 'calc' expression, reflexivity and/or substitution rule is not defined for operator", pos);
-     } else {
-        expr pr = p.parse_expr();
-        for (auto const & pred : preds)
-            steps.emplace_back(pred, mk_calc_annotation(pr));
-    }
+    expr pr = p.parse_expr();
+    for (auto const & pred : preds)
+        steps.emplace_back(pred, mk_calc_annotation(pr));
 }
 
 /** \brief Collect distinct rhs's */
diff --git a/tests/lean/K_bug.lean b/tests/lean/K_bug.lean
index 6408d202a7..59a8088aa3 100644
--- a/tests/lean/K_bug.lean
+++ b/tests/lean/K_bug.lean
@@ -12,7 +12,7 @@ theorem pred_succ (n : Nat) : pred (succ n) = n := rfl
 theorem succ.inj {n m : Nat} (H : succ n = succ m) : n = m
 := calc
     n = pred (succ n) : pred_succ n
-  ... = pred (succ m) : {H}
+  ... = pred (succ m) : by rewrite H
   ... = m             : pred_succ m
 
 end Nat
diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean
index 6d969814ec..6e391beefa 100644
--- a/tests/lean/interactive/eq2.lean
+++ b/tests/lean/interactive/eq2.lean
@@ -122,8 +122,8 @@ theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
   eq.drec_on H₁
     (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
       calc
-        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : {(eq.drec_on_id H₁ b₁)⁻¹}
-            ... = f a₁ b₂                : {H₂})
+        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : sorry -- {(eq.drec_on_id H₁ b₁)⁻¹}
+            ... = f a₁ b₂                 : sorry)
     b₂ H₁ H₂
 
 
diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean
index c66da2bd2c..f03c5ed0a4 100644
--- a/tests/lean/run/class4.lean
+++ b/tests/lean/run/class4.lean
@@ -51,7 +51,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
 := exists.elim (is_not_zero_to_eq H)
      (λ (w : nat) (Hw : y = succ w),
         have H1 : x + y = succ (x + w), from
-          calc x + y = x + succ w   : {Hw}
+          calc x + y = x + succ w   : by rewrite Hw
                  ... = succ (x + w) : refl _,
         have H2 : ¬ is_zero (succ (x + w)), from
           not_is_zero_succ (x+w),
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index b5f3fb351d..0f316dc42d 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -217,14 +217,14 @@ section examples
 
 theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
+  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
               ... = a * b * (c * d) : !mul_assoc
 
 theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
 
 theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
+  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
               ... = a * b * (c * d) : !mul_assoc
 
 -- for test4b to work, we need instances at the level of the bundled structures as well
@@ -236,21 +236,21 @@ test1 a b c d
 
 theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 end examples
diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean
index 12cb774747..6233cd0552 100644
--- a/tests/lean/run/group4.lean
+++ b/tests/lean/run/group4.lean
@@ -128,12 +128,12 @@ test1 a b c d
 
 theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : mul_assoc
 
 theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : mul_assoc
 
 theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean
index b45e06a887..df83819880 100644
--- a/tests/lean/run/group5.lean
+++ b/tests/lean/run/group5.lean
@@ -107,14 +107,14 @@ section examples
 
 theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
+  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
               ... = a * b * (c * d) : !mul_assoc
 
 theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
 
 theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
 calc
-  a * (b * c) * d = a * b * c * d   : {symm !mul_assoc}
+  a * (b * c) * d = a * b * c * d   : by rewrite -mul_assoc
               ... = a * b * (c * d) : !mul_assoc
 
 -- for test4b to work, we need instances at the level of the bundled structures as well
@@ -126,17 +126,17 @@ test1 a b c d
 
 theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
 calc
-  a * 1 * b * c = a * b * c   : {!mul_right_id}
+  a * 1 * b * c = a * b * c   : by rewrite mul_right_id
             ... = a * (b * c) : !mul_assoc
 
 end examples
diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean
index 7459b9693a..eac8eecf8f 100644
--- a/tests/lean/run/is_nil.lean
+++ b/tests/lean/run/is_nil.lean
@@ -17,7 +17,7 @@ theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil
 := not.intro (assume H : cons a l = nil,
      absurd
        (calc true = is_nil (@nil A)   : refl _
-              ... = is_nil (cons a l) : { symm H }
+              ... = is_nil (cons a l) : by rewrite H
               ... = false             : refl _)
        true_ne_false)
 
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 5b76a52e4d..eb92be8b8a 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -26,11 +26,11 @@ theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k
     (take l IH,
         calc
         (n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
-          ... = n * l + m * l + (n + m) : {IH}
+          ... = n * l + m * l + (n + m) : by rewrite IH
           ... = n * l + m * l + n + m : symm (add_assoc _ _ _)
-          ... = n * l + n + m * l + m : {add_right_comm _ _ _}
-          ... = n * l + n + (m * l + m) : add_assoc _ _ _
-          ... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
-          ... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
+          ... = n * l + n + m * l + m    : by rewrite (add_right_comm _ (m*l))
+          ... = n * l + n + (m * l + m)  : add_assoc _ _ _
+          ... = n * succ l + (m * l + m) : by rewrite mul_succ_right
+          ... = n * succ l + m * succ l  :  by rewrite mul_succ_right)
 end nat
 end foo
diff --git a/tests/lean/run/nested_rec.lean b/tests/lean/run/nested_rec.lean
index a248e4fb87..50f8b10e85 100644
--- a/tests/lean/run/nested_rec.lean
+++ b/tests/lean/run/nested_rec.lean
@@ -29,7 +29,7 @@ theorem g_succ (a : nat) : g (succ a) = g (g a) :=
 have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
   well_founded.fix_eq g.F (succ a),
 calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
-          ...   = g (g a)                             : {aux}
+          ...   = g (g a)                             : by rewrite aux
 
 theorem g_all_zero (a : nat) : g a = zero :=
 nat.induction_on a
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index cfd3d20ab1..877afba299 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -75,27 +75,14 @@ list_induction_on s (refl _)
     H ▸ refl _)
 
 theorem concat_assoc2 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
-list_induction_on s (refl _)
-  (take x l,
-    assume H : concat (concat l t) u = concat l (concat t u),
-      calc concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : refl _
-                                      ... = concat (cons x l) (concat t u) : { H })
+sorry
+
 
 theorem concat_assoc3 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
-list_induction_on s (refl _)
-  (take x l,
-    assume H : concat (concat l t) u = concat l (concat t u),
-      calc  concat (concat (cons x l) t) u = cons x (concat l (concat t u)) : { H }
-                                       ... = concat (cons x l) (concat t u) : refl _)
+sorry
 
 theorem concat_assoc4 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
-list_induction_on s (refl _)
-  (take x l,
-    assume H : concat (concat l t) u = concat l (concat t u),
-      calc
-      concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : refl _
-        ... = cons x (concat l (concat t u)) : { H }
-        ... = concat (cons x l) (concat t u) : refl _)
+sorry
 
 -- Length
 -- ------
@@ -108,18 +95,7 @@ theorem length_nil : length (@nil T) = zero := refl _
 theorem length_cons (x : T) (t : list T) : length (x :: t) = succ (length t) := refl _
 
 theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
-list_induction_on s
-  (calc
-    length (concat nil t) = length t : refl _
-      ... = 0 + length t : {symm !zero_add}
-      ... = length (@nil T) + length t : refl _)
-  (take x s,
-    assume H : length (concat s t) = length s + length t,
-    calc
-      length (concat (cons x s) t ) = succ (length (concat s t))  : refl _
-        ... = succ (length s + length t)  : { H }
-        ... = succ (length s) + length t  : {symm !succ_add}
-        ... = length (cons x s) + length t : refl _)
+sorry
 
 -- Reverse
 -- -------
@@ -133,30 +109,11 @@ theorem reverse_cons (x : T) (l : list T) : reverse (x :: l) = (reverse l) ++ (c
 -- opaque_hint (hiding reverse)
 
 theorem reverse_concat (s t : list T) : reverse (s ++ t) = (reverse t) ++ (reverse s) :=
-list_induction_on s
-  (calc
-    reverse (concat nil t) = reverse t : { nil_concat _ }
-      ... = concat (reverse t) nil : symm (concat_nil _)
-      ... = concat (reverse t) (reverse nil) : {symm (reverse_nil)})
-  (take x l,
-    assume H : reverse (concat l t) = concat (reverse t) (reverse l),
-    calc
-      reverse (concat (cons x l) t) = concat (reverse (concat l t)) (cons x nil) : refl _
-        ... = concat (concat (reverse t) (reverse l)) (cons x nil) : { H }
-        ... = concat (reverse t) (concat (reverse l) (cons x nil)) : concat_assoc _ _ _
-        ... = concat (reverse t) (reverse (cons x l)) : refl _)
-
+sorry
 
 -- -- add_rewrite length_nil length_cons
 theorem reverse_reverse (l : list T) : reverse (reverse l) = l :=
-list_induction_on l (refl _)
-  (take x l',
-    assume H: reverse (reverse l') = l',
-    show reverse (reverse (cons x l')) = cons x l', from
-      calc
-        reverse (reverse (cons x l')) =
-            concat (reverse (cons x nil)) (reverse (reverse l')) : {reverse_concat _ _}
-          ... = cons x l' : {H})
+sorry
 -- Append
 -- ------
 
@@ -175,18 +132,7 @@ list_induction_on l (refl _)
     P ▸ refl _)
 
 theorem append_eq_reverse_cons  (x : T) (l : list T) : append x l = reverse (x :: reverse l) :=
-list_induction_on l
-  (calc
-    append x nil = [x] : (refl _)
-      ... = concat nil [x] : {symm (nil_concat _)}
-      ... = concat (reverse nil) [x] : {symm (reverse_nil)}
-      ... = reverse [x] : {symm (reverse_cons _ _)}
-      ... = reverse (x :: (reverse nil)) : {symm (reverse_nil)})
-  (take y l',
-    assume H : append x l' = reverse (x :: reverse l'),
-    calc
-      append x (y :: l') = (y :: l') ++ [ x ] : append_eq_concat _ _
-        ... = concat (reverse (reverse (y :: l'))) [ x ] : {symm (reverse_reverse _)}
-        ... = reverse (x :: (reverse (y :: l'))) : refl _)
+sorry
+
 end
 end list