From e969c7a8d671b3a0c5112b35501beaadcd42a4e4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jul 2015 10:13:19 -0700
Subject: [PATCH] refactor(library): remove 'simp' hack

---
 hott/types/nat/sub.hlean                 | 24 ++++++++-------
 library/data/int/basic.lean              | 38 +++++++++++++++---------
 library/data/int/order.lean              |  6 ++--
 library/data/nat/div.lean                | 35 +++++++++++-----------
 library/data/nat/gcd.lean                |  8 ++---
 library/data/nat/sub.lean                | 24 ++++++++-------
 library/data/quotient/util.lean          | 16 +++++-----
 src/frontends/lean/parse_simp_tactic.cpp |  8 +----
 8 files changed, 86 insertions(+), 73 deletions(-)

diff --git a/hott/types/nat/sub.hlean b/hott/types/nat/sub.hlean
index dff319ca9..4ffcf9117 100644
--- a/hott/types/nat/sub.hlean
+++ b/hott/types/nat/sub.hlean
@@ -425,22 +425,26 @@ definition dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
 (dist_sub_eq_dist_add_left H n ▸ !dist.comm) ▸ !dist.comm
 
 definition dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
-have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
-  by exact sorry,
-H ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
+assert (m - k) + ((k - m) + (m - n)) = (m - n) + ((m - k) + (k - m)),
+  begin
+    generalize m - k, generalize k - m, generalize m - n, intro x y z,
+    rewrite [add.comm y x, add.left_comm]
+  end,
+have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
+  by rewrite [add.assoc, this, -add.assoc],
+this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
 
 definition dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
 have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
   !dist_add_add_left ▸ !dist_add_add_right ▸ rfl,
 H ▸ !dist.triangle_inequality
 
-definition dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
-have H : Πn m, dist n m = n - m + (m - n), from take n m, rfl,
-by exact sorry
+theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
+assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl,
+by rewrite [this, this n m, mul.right_distrib, *mul_sub_right_distrib]
 
-definition dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
-have H : Πn m, dist n m = n - m + (m - n), from take n m, rfl,
-by exact sorry
+theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
+by rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm]
 
 definition dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
 have aux : Πk l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
@@ -451,7 +455,7 @@ have aux : Πk l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
   calc
     dist n m * dist k l = dist n m * (k - l)       : dist_eq_sub_of_ge H
       ... = dist (n * (k - l)) (m * (k - l))       : dist_mul_right
-      ... = dist (n * k - n * l) (m * k - m * l)   : by exact sorry
+      ... = dist (n * k - n * l) (m * k - m * l)   : by rewrite [*mul_sub_left_distrib]
       ... = dist (n * k) (m * k - m * l + n * l)   : dist_sub_eq_dist_add_left (mul_le_mul_left H n)
       ... = dist (n * k) (n * l + (m * k - m * l)) : add.comm
       ... = dist (n * k) (n * l + m * k - m * l)   : add_sub_assoc H2 (n * l)
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index edf7015c0..7213e3f8e 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -169,11 +169,11 @@ calc
 protected theorem equiv.trans [trans] {p q r : ℕ × ℕ} (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
 have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
   calc
-   pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by simp
+   pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by rewrite [*add.assoc, add.comm (pr₂ q)]
     ... = pr2 p + pr1 q + pr2 r                  : {H1}
-    ... = pr2 p + (pr1 q + pr2 r)                : by simp
+    ... = pr2 p + (pr1 q + pr2 r)                : add.assoc
     ... = pr2 p + (pr2 q + pr1 r)                : {H2}
-    ... = pr2 p + pr1 r + pr2 q                  : by simp,
+    ... = pr2 p + pr1 r + pr2 q                  : by rewrite [add.assoc, add.comm (pr₂ q)],
 show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3
 
 protected theorem equiv_equiv : is_equivalence int.equiv :=
@@ -347,10 +347,11 @@ int.cases_on a
 
 theorem padd_congr {p p' q q' : ℕ × ℕ} (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
 calc
-  pr1 (padd p q) + pr2 (padd p' q') = pr1 p + pr2 p' + (pr1 q + pr2 q') : by simp
+  pr1 (padd p q) + pr2 (padd p' q') = pr1 p + pr2 p' + (pr1 q + pr2 q') :
+                 by rewrite [↑padd, *add.assoc, add.left_comm (pr₁ q)]
     ... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha}
     ... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb}
-    ... = pr2 (padd p q) + pr1 (padd p' q') : by simp
+    ... = pr2 (padd p q) + pr1 (padd p' q') : by rewrite [↑padd, *add.assoc, add.left_comm (pr₁ p')]
 
 theorem padd_comm (p q : ℕ × ℕ) : padd p q = padd q p :=
 calc
@@ -422,7 +423,8 @@ theorem padd_pneg (p : ℕ × ℕ) : padd p (pneg p) ≡ (0, 0) :=
 show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl
 
 theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
-show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, from by simp
+show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p,
+from sorry -- by simp
 
 theorem add.left_inv (a : ℤ) : -a + a = 0 :=
 have H : repr (-a + a) ≡ repr 0, from
@@ -520,13 +522,13 @@ have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * x
   calc
     xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
           = xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm))
-            : by simp
-      ... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by simp
-      ... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by simp
+            : sorry -- by simp
+      ... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : sorry -- by simp
+      ... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : sorry -- by simp
       ... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
-            : by simp
+            : sorry -- by simp
       ... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn))
-            : by simp,
+            : sorry, -- by simp,
 nat.add.cancel_right H3
 
 theorem pmul_congr {p p' q q' : ℕ × ℕ} (H1 : p ≡ p') (H2 : q ≡ q') : pmul p q ≡ pmul p' q' :=
@@ -549,7 +551,9 @@ eq_of_repr_equiv_repr
       ... = repr (b * a) : repr_mul) ▸ !equiv.refl)
 
 theorem pmul_assoc (p q r: ℕ × ℕ) : pmul (pmul p q) r = pmul p (pmul q r) :=
-by simp
+begin
+  unfold pmul, apply sorry -- simp
+end
 
 theorem mul.assoc (a b c : ℤ) : (a * b) * c = a * (b * c) :=
 eq_of_repr_equiv_repr
@@ -560,11 +564,17 @@ eq_of_repr_equiv_repr
       ... = pmul (repr a) (repr (b * c)) : repr_mul
       ... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl)
 
+set_option pp.coercions true
+
 theorem mul_one (a : ℤ) : a * 1 = a :=
 eq_of_repr_equiv_repr (int.equiv_of_eq
   ((calc
     repr (a * 1) = pmul (repr a) (repr 1) : repr_mul
-      ... = (pr1 (repr a), pr2 (repr a)) : by simp
+      ... = (pr1 (repr a), pr2 (repr a)) :
+            begin
+              esimp [pmul, nat.of_num, num.to.int, repr],
+              rewrite [+mul_zero, +mul_one, nat.zero_add]
+            end
       ... = repr a : prod.eta)))
 
 theorem one_mul (a : ℤ) : 1 * a = a :=
@@ -575,7 +585,7 @@ eq_of_repr_equiv_repr
   (calc
     repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul
       ... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add equiv.refl
-      ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : by simp
+      ... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : sorry -- by simp
       ... = padd (repr (a * c)) (pmul (repr b) (repr c)) : {(repr_mul a c)⁻¹}
       ... = padd (repr (a * c)) (repr (b * c)) : repr_mul
       ... ≡ repr (a * c + b * c) : equiv.symm !repr_add)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 188cc3436..105358872 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -76,8 +76,8 @@ theorem lt.elim {a b : ℤ} (H : a < b) : ∃n : ℕ, a + succ n = b :=
 obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H,
 have a + succ n = b, from
   calc
-    a + succ n = a + 1 + n : by simp
-      ... = b : Hn,
+    a + succ n = a + 1 + n : by rewrite [add.assoc, add.comm 1 n]
+           ... = b         : Hn,
 exists.intro n this
 
 theorem of_nat_lt_of_nat (n m : ℕ) : of_nat n < of_nat m ↔ n < m :=
@@ -135,7 +135,7 @@ theorem lt.irrefl (a : ℤ) : ¬ a < a :=
   have a + succ n = a + 0, from
     calc
       a + succ n = a : Hn
-        ... = a + 0 : by simp,
+             ... = a + 0 : by rewrite [add_zero],
   have nat.succ n = 0, from add.left_cancel this,
   have nat.succ n = 0, from of_nat.inj this,
   absurd this !succ_ne_zero)
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 9af907260..5dfaa4e0f 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -53,9 +53,9 @@ nat.induction_on y
                        ...   = x div z + zero   : add_zero)
   (take y,
     assume IH : (x + y * z) div z = x div z + y, calc
-      (x + succ y * z) div z = (x + y * z + z) div z    : by simp
+      (x + succ y * z) div z = (x + y * z + z) div z    : by rewrite [-add_one, mul.right_distrib, one_mul, add.assoc]
                          ... = succ ((x + y * z) div z) : !add_div_self H
-                         ... = x div z + succ y         : by simp)
+                         ... = x div z + succ y         : by rewrite [IH])
 
 theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) div y = x div y + z :=
 !mul.comm ▸ add_mul_div_self H
@@ -162,15 +162,15 @@ by_cases_zero_pos y
     assume H : y > 0,
     show x = x div y * y + x mod y, from
       nat.case_strong_induction_on x
-        (show 0 = (0 div y) * y + 0 mod y, by simp)
+        (show 0 = (0 div y) * y + 0 mod y, by rewrite [zero_mod, add_zero, zero_div, zero_mul])
         (take x,
           assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y,
           show succ x = succ x div y * y + succ x mod y, from
             by_cases -- (succ x < y)
               (assume H1 : succ x < y,
-                have H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
-                have H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
-                by simp)
+                assert H2 : succ x div y = 0, from div_eq_zero_of_lt H1,
+                assert H3 : succ x mod y = succ x, from mod_eq_of_lt H1,
+                by rewrite [H2, H3, zero_mul, zero_add])
               (assume H1 : ¬ succ x < y,
                 have H2 : y ≤ succ x, from le_of_not_gt H1,
                 have H3 : succ x div y = succ ((succ x - y) div y), from div_eq_succ_sub_div H H2,
@@ -244,10 +244,10 @@ have H6 : y > 0, from lt_of_le_of_lt !zero_le H1,
 show q1 = q2, from eq_of_mul_eq_mul_right H6 H5
 
 theorem mul_div_mul_left {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
-by_cases -- (y = 0)
-  (assume H : y = 0, by simp)
-  (assume H : y ≠ 0,
-    have ypos : y > 0, from pos_of_ne_zero H,
+by_cases
+  (suppose y = 0, by rewrite [this, mul_zero, *div_zero])
+  (suppose y ≠ 0,
+    have ypos : y > 0, from pos_of_ne_zero this,
     have zypos : z * y > 0, from mul_pos zpos ypos,
     have H1 : (z * x) mod (z * y) < z * y, from !mod_lt zypos,
     have H2 : z * (x mod y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos,
@@ -288,11 +288,12 @@ theorem mul_mod_mul_right (x z y : ℕ) : (x * z) mod (y * z) = (x mod y) * z :=
 mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left
 
 theorem mod_self (n : ℕ) : n mod n = 0 :=
-nat.cases_on n (by simp)
+nat.cases_on n (by unfold modulo)
   (take n,
-    have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
+    assert (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
       from !mul_mod_mul_left,
-    (by simp) ▸ H)
+    assert (succ n) mod (succ n) = succ n * (1 mod 1), by rewrite [*mul_one at this]; exact this,
+    by rewrite this)
 
 theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) mod k = ((m mod k) * n) mod k :=
 calc
@@ -304,12 +305,12 @@ theorem mul_mod_eq_mul_mod_mod (m n k : nat) : (m * n) mod k = (m * (n mod k)) m
 !mul.comm ▸ !mul.comm ▸ !mul_mod_eq_mod_mul_mod
 
 theorem div_one (n : ℕ) : n div 1 = n :=
-have H : n div 1 * 1 + n mod 1 = n, from !eq_div_mul_add_mod⁻¹,
-(by simp) ▸ H
+assert n div 1 * 1 + n mod 1 = n, from !eq_div_mul_add_mod⁻¹,
+begin rewrite [-this at {2}, mul_one, mod_one] end
 
 theorem div_self {n : ℕ} (H : n > 0) : n div n = 1 :=
-have H1 : (n * 1) div (n * 1) = 1 div 1, from !mul_div_mul_left H,
-(by simp) ▸ H1
+assert (n * 1) div (n * 1) = 1, from !mul_div_mul_left H,
+by rewrite [-this, *mul_one]
 
 theorem div_mul_cancel_of_mod_eq_zero {m n : ℕ} (H : m mod n = 0) : m div n * n = m :=
 by rewrite [eq_div_mul_add_mod m n at {2}, H, add_zero]
diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean
index 6c17efc77..05af88c68 100644
--- a/library/data/nat/gcd.lean
+++ b/library/data/nat/gcd.lean
@@ -96,7 +96,7 @@ aux
 theorem gcd_dvd (m n : ℕ) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) :=
 gcd.induction m n
   (take m,
-    show (gcd m 0 ∣ m) ∧ (gcd m 0 ∣ 0), by simp)
+    show (gcd m 0 ∣ m) ∧ (gcd m 0 ∣ 0), by rewrite [*gcd_zero_right]; split; apply dvd.refl; apply dvd_zero)
   (take m n,
     assume npos : 0 < n,
     assume IH : (gcd n (m mod n) ∣ n) ∧ (gcd n (m mod n) ∣ (m mod n)),
@@ -119,10 +119,10 @@ gcd.induction m n
     assume IH : k ∣ n → k ∣ m mod n → k ∣ gcd n (m mod n),
     assume H1 : k ∣ m,
     assume H2 : k ∣ n,
-    have H3 : k ∣ m div n * n + m mod n, from !eq_div_mul_add_mod ▸ H1,
-    have H4 : k ∣ m mod n, from nat.dvd_of_dvd_add_left H3 (dvd.trans H2 (by simp)),
+    assert k ∣ m div n * n + m mod n, from !eq_div_mul_add_mod ▸ H1,
+    assert k ∣ m mod n, from nat.dvd_of_dvd_add_left this (dvd.trans H2 !dvd_mul_left),
     have gcd_eq : gcd n (m mod n) = gcd m n, from !gcd_rec⁻¹,
-    show k ∣ gcd m n, from gcd_eq ▸ IH H2 H4)
+    show k ∣ gcd m n, from gcd_eq ▸ IH H2 `k ∣ m mod n`)
 
 theorem gcd.comm (m n : ℕ) : gcd m n = gcd n m :=
 dvd.antisymm
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index 8a18a5c56..c54793069 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -427,22 +427,26 @@ theorem dist_sub_eq_dist_add_right {k m : ℕ} (H : k ≥ m) (n : ℕ) :
 (dist_sub_eq_dist_add_left H n ▸ !dist.comm) ▸ !dist.comm
 
 theorem dist.triangle_inequality (n m k : ℕ) : dist n k ≤ dist n m + dist m k :=
-have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
-  by simp,
-H ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
+assert (m - k) + ((k - m) + (m - n)) = (m - n) + ((m - k) + (k - m)),
+  begin
+    generalize m - k, generalize k - m, generalize m - n, intro x y z,
+    rewrite [add.comm y x, add.left_comm]
+  end,
+have (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
+  by rewrite [add.assoc, this, -add.assoc],
+this ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
 
 theorem dist_add_add_le_add_dist_dist (n m k l : ℕ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
 have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
   !dist_add_add_left ▸ !dist_add_add_right ▸ rfl,
 H ▸ !dist.triangle_inequality
 
-theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
-have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
-by simp
-
 theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k :=
-have H : ∀n m, dist n m = n - m + (m - n), from take n m, rfl,
-by simp
+assert ∀ n m, dist n m = n - m + (m - n), from take n m, rfl,
+by rewrite [this, this n m, mul.right_distrib, *mul_sub_right_distrib]
+
+theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m :=
+by rewrite [mul.comm k n, mul.comm k m, dist_mul_right, mul.comm]
 
 theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
 have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
@@ -453,7 +457,7 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
   calc
     dist n m * dist k l = dist n m * (k - l)       : dist_eq_sub_of_ge H
       ... = dist (n * (k - l)) (m * (k - l))       : dist_mul_right
-      ... = dist (n * k - n * l) (m * k - m * l)   : by simp
+      ... = dist (n * k - n * l) (m * k - m * l)   : by rewrite [*mul_sub_left_distrib]
       ... = dist (n * k) (m * k - m * l + n * l)   : dist_sub_eq_dist_add_left (!mul_le_mul_left H)
       ... = dist (n * k) (n * l + (m * k - m * l)) : add.comm
       ... = dist (n * k) (n * l + m * k - m * l)   : add_sub_assoc H2 (n * l)
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index 174bd121b..2672b5c53 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -137,13 +137,13 @@ theorem map_pair2_id_right {A B : Type} {f : A → B → A} {e : B} (Hid : ∀a
   (v : A × A) : map_pair2 f v (pair e e) = v :=
 have Hx : pr1 (map_pair2 f v (pair e e)) = pr1 v, from
   (calc
-    pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by simp
-      ... = f (pr1 v) e : by simp
+    pr1 (map_pair2 f v (pair e e)) = f (pr1 v) (pr1 (pair e e)) : by esimp
+      ... = f (pr1 v) e : by esimp
       ... = pr1 v : Hid (pr1 v)),
 have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
   (calc
-    pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
-      ... = f (pr2 v) e : by simp
+    pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by esimp
+      ... = f (pr2 v) e : by esimp
       ... = pr2 v : Hid (pr2 v)),
 prod.eq Hx Hy
 
@@ -151,13 +151,13 @@ theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a :
   (v : A × A) : map_pair2 f (pair e e) v = v :=
 have Hx : pr1 (map_pair2 f (pair e e) v) = pr1 v, from
    calc
-    pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by simp
-      ... = f e (pr1 v) : by simp
+    pr1 (map_pair2 f (pair e e) v) = f (pr1 (pair e e)) (pr1 v) : by esimp
+      ... = f e (pr1 v) : by esimp
       ... = pr1 v : Hid (pr1 v),
 have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
    calc
-    pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
-      ... = f e (pr2 v) : by simp
+    pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by esimp
+      ... = f e (pr2 v) : by esimp
       ... = pr2 v : Hid (pr2 v),
 prod.eq Hx Hy
 
diff --git a/src/frontends/lean/parse_simp_tactic.cpp b/src/frontends/lean/parse_simp_tactic.cpp
index f31887f07..6a10df64b 100644
--- a/src/frontends/lean/parse_simp_tactic.cpp
+++ b/src/frontends/lean/parse_simp_tactic.cpp
@@ -73,12 +73,6 @@ expr parse_simp_tactic(parser & p) {
     location loc = parse_tactic_location(p);
 
     // Remark: simp_tac is the actual result
-    expr simp_tac = mk_simp_tactic_expr(lemmas, ns, hiding, tac, loc);
-
-    // Using (or_else simp_tac (exact sorry)) to simplify testing
-    auto pos = p.pos();
-    expr sorry = p.mk_sorry(pos);
-    expr exact_sorry = p.mk_app(get_exact_tac_fn(), sorry, pos);
-    return mk_app(get_or_else_tac_fn(), simp_tac, exact_sorry);
+    return mk_simp_tactic_expr(lemmas, ns, hiding, tac, loc);
 }
 }