wip: first run with normal form success

src/Init/Data/Fin/Lemmas.lean

@@ -682,7 +682,7 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
     cast _ (reverseInduction last cast j.succ)
 termination_by n + 1 - i
 decreasing_by decreasing_with
-  -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
+  simp [Nat.succ_sub_succ_eq_sub]
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
 
 @[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :

src/Init/Data/Int.lean

@@ -8,6 +8,7 @@ import Init.Data.Int.Basic
 import Init.Data.Int.Bitwise
 import Init.Data.Int.DivMod
 import Init.Data.Int.DivModLemmas
+import Init.Data.Int.DivModExt
 import Init.Data.Int.Gcd
 import Init.Data.Int.Lemmas
 import Init.Data.Int.Order

src/Init/Data/Int/DivModExt.lean

@@ -0,0 +1,83 @@
+prelude
+import Init.Data.Int.DivModLemmas
+import Init.Data.Nat.Lemmas
+
+namespace Int
+
+theorem ediv_ofNat_negSucc (m n : Nat) : m / -[n+1] = -ofNat (m / Nat.succ n) := rfl
+theorem ediv_negSucc_zero (m : Nat) : -[m+1] / 0 = 0 := rfl
+theorem ediv_negSucc_succ (m n : Nat) : -[m+1] / (n + 1 : Nat) = -((m / (n + 1)) : Nat) + (-1) := by
+  simp [HDiv.hDiv, Div.div, Int.ediv, Int.negSucc_coe', Int.sub_eq_add_neg]
+theorem ediv_negSucc_negSucc (m n : Nat) : -[m+1] / -[n+1] = ((m / (n + 1) + 1) : Nat) := rfl
+
+theorem emod_ofNat   (a : Nat) (b : Int) : Nat.cast a % b = Nat.cast (a % b.natAbs) := rfl
+theorem emod_negSucc (a : Nat) (b : Int) : -[a+1] % b = (b.natAbs : Int) - (a % b.natAbs + 1) := rfl
+
+@[simp] theorem dvd_natCast_natCast (a b : Nat) : (a : Int) ∣ (b : Int) ↔ a ∣ b := by
+  simp [Int.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, mod, Int.emod_ofNat,
+    -emod_ofNat]
+  apply Int.ofNat_inj
+
+@[simp] theorem dvd_negSucc (a : Int) (b : Nat) : a ∣ -[b +1] ↔ a ∣ (b+1 : Nat) := by
+  simp only [Int.dvd_def]
+  apply Iff.intro
+  · intro ⟨c, p⟩
+    apply Exists.intro (-c)
+    simp only [Int.mul_neg, ← p]
+    rfl
+  · intro ⟨c, p⟩
+    apply Exists.intro (-c)
+    simp only [Int.mul_neg, ← p]
+    rfl
+
+@[simp] theorem negSucc_dvd (a : Nat) (b : Int) : -[a +1] ∣ b ↔ (((a+1 : Nat) : Int) ∣ b) := by
+  apply Iff.intro
+  · intro ⟨c, p⟩
+    apply Exists.intro (-c)
+    match c with
+    | .ofNat 0 =>
+      simp_all
+    | .ofNat (.succ c) =>
+      simp_all [-natCast_add, Int.mul_neg]
+    | -[c+1] =>
+      simp_all [-natCast_add, Int.mul_neg]
+  · intro ⟨c, p⟩
+    apply Exists.intro (-c)
+    match c with
+    | .ofNat 0 =>
+      simp_all
+    | .ofNat (.succ c) =>
+      simp_all [-natCast_add, Int.mul_neg]
+    | -[c+1] =>
+      simp_all [-natCast_add, Int.mul_neg]
+
+theorem fdiv_eq_ediv' (a b : Int) : Int.fdiv a b = a / b + if b < 0 ∧ ¬(b ∣ a) then (-1) else 0 := by
+  match a, b with
+  | 0,       b       =>
+    simp [Int.fdiv, Int.dvd_zero]
+  | ofNat (Nat.succ m), ofNat n =>
+    simp [Int.fdiv, Int.ofNat_not_neg]
+  | ofNat (Nat.succ m), -[n+1] =>
+    simp only [fdiv,Int.negSucc_lt_zero, true_and, Int.ofNat_eq_coe, ediv_ofNat_negSucc,
+               Int.negSucc_dvd, Int.dvd_natCast_natCast, ite_not,
+               Nat.succ_div, Nat.succ_eq_add_one]
+    split <;> rename_i h
+    · rw [Int.add_zero]; rfl
+    · rw [← Int.neg_add]; rfl
+  | -[_+1],  0       =>
+    simp
+  | -[m+1],  ofNat (Nat.succ n) => rfl
+  | -[m+1],  -[n+1]  =>
+    simp only [Int.fdiv, Int.ediv_negSucc_negSucc, Nat.succ_div, Int.negSucc_lt_zero, true_and,
+      Int.dvd_negSucc, Int.negSucc_dvd, Int.dvd_natCast_natCast]
+    split <;> rename_i h
+    · simp only [Int.add_zero]
+      rfl
+    · simp only [Int.natCast_add, Int.Nat.cast_ofNat_Int, Int.add_neg_cancel_right]
+      rfl
+
+theorem fmod_eq_emod' (a b : Int) : Int.fmod a b = a % b - b * ite (b < 0 ∧ ¬(b ∣ a)) (-1) 0 := by
+  simp [fmod_def, emod_def, fdiv_eq_ediv', Int.sub_eq_add_neg, Int.mul_add, Int.neg_add,
+        Int.add_assoc]
+
+end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -22,55 +22,40 @@ namespace Int
 
 protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
 
-protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
-
 protected theorem dvd_refl (n : Int) : n ∣ n := ⟨1, (Int.mul_one _).symm⟩
 
-protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
-
-protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
-  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (by rw [Int.mul_assoc])
-
-@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
-  refine ⟨fun ⟨a, ae⟩ => ?_, fun ⟨k, e⟩ => ⟨k, by rw [e, Int.ofNat_mul]⟩⟩
-  match Int.le_total a 0 with
-  | .inl h =>
-    have := ae.symm ▸ Int.mul_nonpos_of_nonneg_of_nonpos (ofNat_zero_le _) h
-    rw [Nat.le_antisymm (ofNat_le.1 this) (Nat.zero_le _)]
-    apply Nat.dvd_zero
-  | .inr h => match a, eq_ofNat_of_zero_le h with
-    | _, ⟨k, rfl⟩ => exact ⟨k, Int.ofNat.inj ae⟩
-
-theorem dvd_antisymm {a b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b := by
-  rw [← natAbs_of_nonneg H1, ← natAbs_of_nonneg H2]
-  rw [ofNat_dvd, ofNat_dvd, ofNat_inj]
-  apply Nat.dvd_antisymm
+protected theorem dvd_zero (n : Int) : n ∣ 0 := ⟨0, (Int.mul_zero _).symm⟩
 
 @[simp] protected theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
   Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
             (fun h => h.symm ▸ Int.dvd_refl _)
 
+protected theorem one_dvd (n : Int) : 1 ∣ n := ⟨n, (Int.one_mul n).symm⟩
+
+protected theorem dvd_trans : ∀ {a b c : Int}, a ∣ b → b ∣ c → a ∣ c
+  | a, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => Exists.intro (d * e) (Int.mul_assoc a d e)
+
+protected theorem dvd_mul_left (a b : Int) :  a ∣ b * a := ⟨_, Int.mul_comm ..⟩
 protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩
 
-protected theorem dvd_mul_left (a b : Int) : b ∣ a * b := ⟨_, Int.mul_comm ..⟩
-
-protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
-  constructor <;> exact fun ⟨k, e⟩ =>
-    ⟨-k, by simp [e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
-
-protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
-  constructor <;> exact fun ⟨k, e⟩ =>
-    ⟨-k, by simp [← e, Int.neg_mul, Int.mul_neg, Int.neg_neg]⟩
-
-@[simp] theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
+theorem natAbs_dvd_natAbs {a b : Int} : natAbs a ∣ natAbs b ↔ a ∣ b := by
   refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
   rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
   cases hk <;> subst b
   · apply Int.dvd_mul_right
   · rw [← Int.mul_neg]; apply Int.dvd_mul_right
 
+protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
+
+protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
+
+@[norm_cast] theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
+  simp [←natAbs_dvd_natAbs]
+
 theorem ofNat_dvd_left {n : Nat} {z : Int} : (↑n : Int) ∣ z ↔ n ∣ z.natAbs := by
-  rw [← natAbs_dvd_natAbs, natAbs_ofNat]
+  simp [←natAbs_dvd_natAbs]
 
 protected theorem dvd_add : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b + c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d + e, by rw [Int.mul_add]⟩
@@ -78,15 +63,19 @@ protected theorem dvd_add : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b +
 protected theorem dvd_sub : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b - c
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Int.mul_sub]⟩
 
-protected theorem dvd_add_left {a b c : Int} (H : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
-  ⟨fun h => by have := Int.dvd_sub h H; rwa [Int.add_sub_cancel] at this, (Int.dvd_add · H)⟩
+protected theorem dvd_add_left {a b c : Int} (H : a ∣ c) : a ∣ b + c ↔ a ∣ b := by
+  apply Iff.intro
+  · intro h
+    have := Int.dvd_sub h H
+    rwa [Int.add_sub_cancel] at this
+  · exact (Int.dvd_add · H)
 
 protected theorem dvd_add_right {a b c : Int} (H : a ∣ b) : a ∣ b + c ↔ a ∣ c := by
   rw [Int.add_comm, Int.dvd_add_left H]
 
 protected theorem dvd_iff_dvd_of_dvd_sub {a b c : Int} (H : a ∣ b - c) : a ∣ b ↔ a ∣ c :=
-  ⟨fun h => Int.sub_sub_self b c ▸ Int.dvd_sub h H,
-   fun h => Int.sub_add_cancel b c ▸ Int.dvd_add H h⟩
+  Iff.intro (fun h => Int.sub_sub_self b c ▸ Int.dvd_sub h H)
+            (fun h => Int.sub_add_cancel b c ▸ Int.dvd_add H h)
 
 protected theorem dvd_iff_dvd_of_dvd_add {a b c : Int} (H : a ∣ b + c) : a ∣ b ↔ a ∣ c := by
   rw [← Int.sub_neg] at H; rw [Int.dvd_iff_dvd_of_dvd_sub H, Int.dvd_neg]
@@ -96,26 +85,25 @@ theorem le_of_dvd {a b : Int} (bpos : 0 < b) (H : a ∣ b) : a ≤ b :=
   | ofNat _, _, ⟨n, rfl⟩, H => ofNat_le.2 <| Nat.le_of_dvd n.succ_pos <| ofNat_dvd.1 H
   | -[_+1], _, ⟨_, rfl⟩, _ => Int.le_trans (Int.le_of_lt <| negSucc_lt_zero _) (ofNat_zero_le _)
 
-theorem natAbs_dvd {a b : Int} : (a.natAbs : Int) ∣ b ↔ a ∣ b :=
-  match natAbs_eq a with
-  | .inl e => by rw [← e]
-  | .inr e => by rw [← Int.neg_dvd, ← e]
+theorem dvd_antisymm {a b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b ∣ a → a = b := by
+  rw [← natAbs_of_nonneg H1, ← natAbs_of_nonneg H2]
+  rw [ofNat_dvd, ofNat_dvd, ofNat_inj]
+  apply Nat.dvd_antisymm
 
-theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b :=
-  match natAbs_eq b with
-  | .inl e => by rw [← e]
-  | .inr e => by rw [← Int.dvd_neg, ← e]
+theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
 
-theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a := by
-  rw [Int.natAbs_dvd]
-  exact Int.dvd_refl a
+theorem natAbs_dvd {a b : Int} : (a.natAbs : Int) ∣ b ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
 
 theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by
-  rw [Int.dvd_natAbs]
-  exact Int.dvd_refl a
+  simp [←natAbs_dvd_natAbs, Nat.dvd_refl]
+
+theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a := by
+  simp [←natAbs_dvd_natAbs, Nat.dvd_refl]
 
 theorem ofNat_dvd_right {n : Nat} {z : Int} : z ∣ (↑n : Int) ↔ z.natAbs ∣ n := by
-  rw [← natAbs_dvd_natAbs, natAbs_ofNat]
+  simp [←natAbs_dvd_natAbs]
 
 theorem eq_one_of_dvd_one {a : Int} (H : 0 ≤ a) (H' : a ∣ 1) : a = 1 :=
   match a, eq_ofNat_of_zero_le H, H' with
@@ -127,6 +115,8 @@ theorem eq_one_of_mul_eq_one_right {a b : Int} (H : 0 ≤ a) (H' : a * b = 1) :
 theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b = 1 :=
   eq_one_of_mul_eq_one_right H <| by rw [Int.mul_comm, H']
 
+attribute [simp] natAbs_dvd_natAbs
+
 /-! ### *div zero  -/
 
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
@@ -152,19 +142,6 @@ theorem eq_one_of_mul_eq_one_left {a b : Int} (H : 0 ≤ b) (H' : a * b = 1) : b
   | succ _ => rfl
   | -[_+1] => rfl
 
-/-! ### div equivalences  -/
-
-theorem div_eq_ediv : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → a.div b = a / b
-  | 0, _, _, _ | _, 0, _, _ => by simp
-  | succ _, succ _, _, _ => rfl
-
-theorem fdiv_eq_ediv : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
-  | 0, _, _ | -[_+1], 0, _ => by simp
-  | succ _, ofNat _, _ | -[_+1], succ _, _ => rfl
-
-theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a b :=
-  div_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
-
 /-! ### mod zero -/
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := rfl
@@ -193,6 +170,19 @@ theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a
 
 /-! ### mod definitiions -/
 
+theorem emod_as_nat_mod (m n : Int) : (m % n) =
+  (if m ≥ 0 then
+    (((m.natAbs % n.natAbs) : Nat) : Int)
+  else
+    ((n.natAbs : Int) - (((((m.natAbs - 1) % n.natAbs + 1) : Nat) : Int)))) := by
+cases m <;> cases n <;> (rename_i m n ; simp [HMod.hMod, Mod.mod, emod, ofNat_nonneg])
+· have p : (Nat.cast (Nat.succ m) : Int) - 1 = m := by simp [Nat.succ_eq_add_one]
+  simp [p, Int.subNatNat_eq_coe, Nat.succ_eq_add_one]
+· have p : (Nat.cast (Nat.succ m) : Int) - 1 = m := by simp [Nat.succ_eq_add_one]
+  have q : (Nat.cast n : Int) + 1 = Nat.cast (n + 1) := by rfl
+  simp [p, Int.subNatNat_eq_coe, Nat.succ_eq_add_one, q, -Int.natCast_add]
+  rfl
+
 theorem emod_add_ediv : ∀ a b : Int, a % b + b * (a / b) = a
   | ofNat _, ofNat _ => congrArg ofNat <| Nat.mod_add_div ..
   | ofNat m, -[n+1] => by
@@ -219,67 +209,6 @@ theorem ediv_add_emod' (a b : Int) : a / b * b + a % b = a := by
 theorem emod_def (a b : Int) : a % b = a - b * (a / b) := by
   rw [← Int.add_sub_cancel (a % b), emod_add_ediv]
 
-theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
-  | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
-  | ofNat m, -[n+1] => by
-    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
-    rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
-  | -[_+1], 0 => rfl
-  | -[m+1], ofNat n => by
-    show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
-    rw [Int.mul_neg, ← Int.neg_add]
-    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
-  | -[m+1], -[n+1] => by
-    show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
-    rw [Int.neg_mul, ← Int.neg_add]
-    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
-
-theorem div_add_mod (a b : Int) : b * a.div b + mod a b = a := by
-  rw [Int.add_comm]; apply mod_add_div ..
-
-theorem mod_add_div' (m k : Int) : mod m k + m.div k * k = m := by
-  rw [Int.mul_comm]; apply mod_add_div
-
-theorem div_add_mod' (m k : Int) : m.div k * k + mod m k = m := by
-  rw [Int.mul_comm]; apply div_add_mod
-
-theorem mod_def (a b : Int) : mod a b = a - b * a.div b := by
-  rw [← Int.add_sub_cancel (mod a b), mod_add_div]
-
-theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
-  | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
-  | succ m, ofNat n => congrArg ofNat <| Nat.mod_add_div ..
-  | succ m, -[n+1] => by
-    show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
-    rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
-      Int.subNatNat_eq_coe, Int.sub_add_cancel]
-    exact congrArg (ofNat · + 1) <| Nat.mod_add_div ..
-  | -[_+1], 0 => by rw [fmod_zero]; rfl
-  | -[m+1], succ n => by
-    show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
-    rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]
-    exact congrArg (-ofNat ·) <| Nat.succ_add .. ▸ Nat.mod_add_div .. ▸ rfl
-  | -[m+1], -[n+1] => by
-    show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
-    rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
-
-theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
-  rw [Int.add_comm]; exact fmod_add_fdiv ..
-
-theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
-  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]
-
-/-! ### mod equivalences  -/
-
-theorem fmod_eq_emod (a : Int) {b : Int} (hb : 0 ≤ b) : fmod a b = a % b := by
-  simp [fmod_def, emod_def, fdiv_eq_ediv _ hb]
-
-theorem mod_eq_emod {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : mod a b = a % b := by
-  simp [emod_def, mod_def, div_eq_ediv ha hb]
-
-theorem fmod_eq_mod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = mod a b :=
-  mod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
-
 /-! ### `/` ediv -/
 
 @[simp] protected theorem ediv_neg : ∀ a b : Int, a / (-b) = -(a / b)
@@ -304,6 +233,10 @@ theorem ediv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a / b :=
 theorem ediv_nonpos {a b : Int} (Ha : 0 ≤ a) (Hb : b ≤ 0) : a / b ≤ 0 :=
   Int.nonpos_of_neg_nonneg <| Int.ediv_neg .. ▸ Int.ediv_nonneg Ha (Int.neg_nonneg_of_nonpos Hb)
 
+theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
+  | ofNat _, _, _ => ofNat_zero_le _
+  | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
+
 theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c = a / c + b :=
   suffices ∀ {{a b c : Int}}, 0 < c → (a + b * c).ediv c = a.ediv c + b from
     match Int.lt_trichotomy c 0 with
@@ -334,19 +267,24 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       apply congrArg negSucc
       rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
 
-theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
-  if h : c = 0 then by simp [h] else by
-    let ⟨k, hk⟩ := H
-    rw [hk, Int.mul_comm c k, Int.add_mul_ediv_right _ _ h,
-      ← Int.zero_add (k * c), Int.add_mul_ediv_right _ _ h, Int.zero_ediv, Int.zero_add]
-
-theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
-  rw [Int.add_comm, Int.add_ediv_of_dvd_right H, Int.add_comm]
+theorem add_mul_ediv_left (a : Int) {b : Int}
+    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
+  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
 
 @[simp] theorem mul_ediv_cancel (a : Int) {b : Int} (H : b ≠ 0) : (a * b) / b = a := by
   have := Int.add_mul_ediv_right 0 a H
   rwa [Int.zero_add, Int.zero_ediv, Int.zero_add] at this
 
+theorem add_ediv_of_dvd_right {a b c : Int} (H : c ∣ b) : (a + b) / c = a / c + b / c :=
+  if z : c = 0 then by
+    simp [z]
+  else by
+    let ⟨d, h⟩ := H
+    simp [h, Int.mul_comm c _, Int.add_mul_ediv_right, z]
+
+theorem add_ediv_of_dvd_left {a b c : Int} (H : c ∣ a) : (a + b) / c = a / c + b / c := by
+  rw [Int.add_comm a b, Int.add_comm (a/c) _, Int.add_ediv_of_dvd_right H]
+
 @[simp] theorem mul_ediv_cancel_left (b : Int) (H : a ≠ 0) : (a * b) / a = b :=
   Int.mul_comm .. ▸ Int.mul_ediv_cancel _ H
 
@@ -361,10 +299,6 @@ theorem ediv_eq_zero_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a / b = 0 :
   match a, b, eq_ofNat_of_zero_le H1, eq_succ_of_zero_lt (Int.lt_of_le_of_lt H1 H2) with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg Nat.cast <| Nat.div_eq_of_lt <| ofNat_lt.1 H2
 
-theorem add_mul_ediv_left (a : Int) {b : Int}
-    (c : Int) (H : b ≠ 0) : (a + b * c) / b = a / b + c :=
-  Int.mul_comm .. ▸ Int.add_mul_ediv_right _ _ H
-
 @[simp] theorem mul_ediv_mul_of_pos {a : Int}
     (b c : Int) (H : 0 < a) : (a * b) / (a * c) = b / c :=
   suffices ∀ (m k : Nat) (b : Int), (m.succ * b) / (m.succ * k) = b / k from
@@ -413,11 +347,7 @@ theorem negSucc_emod (m : Nat) {b : Int} (bpos : 0 < b) : -[m+1] % b = b - 1 - m
   match b, eq_succ_of_zero_lt bpos with
   | _, ⟨n, rfl⟩ => rfl
 
-theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
-
-theorem emod_nonneg : ∀ (a : Int) {b : Int}, b ≠ 0 → 0 ≤ a % b
-  | ofNat _, _, _ => ofNat_zero_le _
-  | -[_+1], _, H => Int.sub_nonneg_of_le <| ofNat_le.2 <| Nat.mod_lt _ (natAbs_pos.2 H)
+theorem ofNat_mod_ofNat (m n : Nat) : ↑m % (↑n : Int) = ↑(m % n) := rfl
 
 theorem emod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a % b < b :=
   match a, b, eq_succ_of_zero_lt H with
@@ -439,11 +369,15 @@ theorem lt_mul_ediv_self_add {x k : Int} (h : 0 < k) : x < k * (x / k) + k :=
     rw [cz, Int.mul_zero, Int.add_zero]
   else by
     rw [Int.emod_def, Int.emod_def, Int.add_mul_ediv_right _ _ cz, Int.add_comm _ b,
-      Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]
+        Int.mul_add, Int.mul_comm, ← Int.sub_sub, Int.add_sub_cancel]
 
 @[simp] theorem add_mul_emod_self_left (a b c : Int) : (a + b * c) % b = a % b := by
   rw [Int.mul_comm, Int.add_mul_emod_self]
 
+theorem add_emod_of_dvd (a b c : Int) (p : c ∣ b) : (a + b) % c = a % c := by
+  let ⟨d, eq⟩ := p
+  simp only [eq,  Int.add_mul_emod_self_left]
+
 @[simp] theorem add_emod_self {a b : Int} : (a + b) % b = a % b := by
   have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
 
@@ -497,6 +431,11 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
   match k, h with
   | _, ⟨t, rfl⟩ => rw [Int.mul_assoc, add_mul_emod_self_left]
 
+theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
+  have b0 := Int.le_trans H1 (Int.le_of_lt H2)
+  match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
+  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
+
 @[simp] theorem emod_emod (a b : Int) : (a % b) % b = a % b := by
   conv => rhs; rw [← emod_add_ediv a b, add_mul_emod_self_left]
 
@@ -504,10 +443,6 @@ theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n := by
   apply (emod_add_cancel_right b).mp
   rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]
 
-theorem emod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : a % b = a :=
-  have b0 := Int.le_trans H1 (Int.le_of_lt H2)
-  match a, b, eq_ofNat_of_zero_le H1, eq_ofNat_of_zero_le b0 with
-  | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => congrArg ofNat <| Nat.mod_eq_of_lt (Int.ofNat_lt.1 H2)
 
 @[simp] theorem emod_self_add_one {x : Int} (h : 0 ≤ x) : x % (x + 1) = x :=
   emod_eq_of_lt h (Int.lt_succ x)
@@ -758,6 +693,34 @@ theorem ediv_eq_ediv_of_mul_eq_mul {a b c d : Int}
 
 /-! ### div -/
 
+
+theorem mod_add_div : ∀ a b : Int, mod a b + b * (a.div b) = a
+  | ofNat _, ofNat _ => congrArg ofNat (Nat.mod_add_div ..)
+  | ofNat m, -[n+1] => by
+    show (m % succ n + -↑(succ n) * -↑(m / succ n) : Int) = m
+    rw [Int.neg_mul_neg]; exact congrArg ofNat (Nat.mod_add_div ..)
+  | -[_+1], 0 => rfl
+  | -[m+1], ofNat n => by
+    show -(↑((succ m) % n) : Int) + ↑n * -↑(succ m / n) = -↑(succ m)
+    rw [Int.mul_neg, ← Int.neg_add]
+    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
+  | -[m+1], -[n+1] => by
+    show -(↑(succ m % succ n) : Int) + -↑(succ n) * ↑(succ m / succ n) = -↑(succ m)
+    rw [Int.neg_mul, ← Int.neg_add]
+    exact congrArg (-ofNat ·) (Nat.mod_add_div ..)
+
+theorem div_add_mod (a b : Int) : b * a.div b + mod a b = a := by
+  rw [Int.add_comm]; apply mod_add_div ..
+
+theorem mod_add_div' (m k : Int) : mod m k + m.div k * k = m := by
+  rw [Int.mul_comm]; apply mod_add_div
+
+theorem div_add_mod' (m k : Int) : m.div k * k + mod m k = m := by
+  rw [Int.mul_comm]; apply div_add_mod
+
+theorem mod_def (a b : Int) : mod a b = a - b * a.div b := by
+  rw [← Int.add_sub_cancel (mod a b), mod_add_div]
+
 @[simp] protected theorem div_one : ∀ a : Int, a.div 1 = a
   | (n:Nat) => congrArg ofNat (Nat.div_one _)
   | -[n+1] => by simp [Int.div, neg_ofNat_succ]; rfl
@@ -844,6 +807,10 @@ protected theorem eq_div_of_mul_eq_right {a b c : Int}
     (H1 : a ≠ 0) (H2 : a * b = c) : b = c.div a :=
   (Int.div_eq_of_eq_mul_right H1 H2.symm).symm
 
+theorem div_eq_ediv : ∀ {a b : Int}, 0 ≤ a → 0 ≤ b → a.div b = a / b
+  | 0, _, _, _ | _, 0, _, _ => by simp
+  | succ _, succ _, _, _ => rfl
+
 /-! ### (t-)mod -/
 
 theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
@@ -851,6 +818,11 @@ theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
 @[simp] theorem mod_one (a : Int) : mod a 1 = 0 := by
   simp [mod_def, Int.div_one, Int.one_mul, Int.sub_self]
 
+/-! ### mod equivalences  -/
+
+theorem mod_eq_emod {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : mod a b = a % b := by
+  simp [emod_def, mod_def, div_eq_ediv ha hb]
+
 theorem mod_eq_of_lt {a b : Int} (H1 : 0 ≤ a) (H2 : a < b) : mod a b = a := by
   rw [mod_eq_emod H1 (Int.le_trans H1 (Int.le_of_lt H2)), emod_eq_of_lt H1 H2]
 
@@ -931,6 +903,36 @@ protected theorem sign_eq_div_abs (a : Int) : sign a = a.div (natAbs a) :=
 
 /-! ### fdiv -/
 
+theorem fmod_add_fdiv : ∀ a b : Int, a.fmod b + b * a.fdiv b = a
+  | 0, ofNat _ | 0, -[_+1] => congrArg ofNat <| by simp
+  | succ m, ofNat n => congrArg ofNat <| Nat.mod_add_div ..
+  | succ m, -[n+1] => by
+    show subNatNat (m % succ n) n + (↑(succ n * (m / succ n)) + n + 1) = (m + 1)
+    rw [Int.add_comm _ n, ← Int.add_assoc, ← Int.add_assoc,
+      Int.subNatNat_eq_coe, Int.sub_add_cancel]
+    exact congrArg (ofNat · + 1) <| Nat.mod_add_div ..
+  | -[_+1], 0 => by rw [fmod_zero]; rfl
+  | -[m+1], succ n => by
+    show subNatNat .. - (↑(succ n * (m / succ n)) + ↑(succ n)) = -↑(succ m)
+    rw [Int.subNatNat_eq_coe, ← Int.sub_sub, ← Int.neg_sub, Int.sub_sub, Int.sub_sub_self]
+    exact congrArg (-ofNat ·) <| Nat.succ_add .. ▸ Nat.mod_add_div .. ▸ rfl
+  | -[m+1], -[n+1] => by
+    show -(↑(succ m % succ n) : Int) + -↑(succ n * (succ m / succ n)) = -↑(succ m)
+    rw [← Int.neg_add]; exact congrArg (-ofNat ·) <| Nat.mod_add_div ..
+
+theorem fdiv_add_fmod (a b : Int) : b * a.fdiv b + a.fmod b = a := by
+  rw [Int.add_comm]; exact fmod_add_fdiv ..
+
+theorem fmod_def (a b : Int) : a.fmod b = a - b * a.fdiv b := by
+  rw [← Int.add_sub_cancel (a.fmod b), fmod_add_fdiv]
+
+theorem fdiv_eq_ediv : ∀ (a : Int) {b : Int}, 0 ≤ b → fdiv a b = a / b
+  | 0, _, _ | -[_+1], 0, _ => by simp
+  | succ _, ofNat _, _ | -[_+1], succ _, _ => rfl
+
+theorem fdiv_eq_div {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fdiv a b = div a b :=
+  div_eq_ediv Ha Hb ▸ fdiv_eq_ediv _ Hb
+
 theorem fdiv_nonneg {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a.fdiv b :=
   match a, b, eq_ofNat_of_zero_le Ha, eq_ofNat_of_zero_le Hb with
   | _, _, ⟨_, rfl⟩, ⟨_, rfl⟩ => ofNat_fdiv .. ▸ ofNat_zero_le _
@@ -968,8 +970,13 @@ theorem lt_fdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.fdiv b
 
 /-! ### fmod -/
 
-theorem ofNat_fmod (m n : Nat) : ↑(m % n) = fmod m n := by
-  cases m <;> simp [fmod, Nat.succ_eq_add_one]
+theorem fmod_eq_emod (a : Int) {b : Int} (hb : 0 ≤ b) : fmod a b = a % b := by
+  simp [fmod_def, emod_def, fdiv_eq_ediv _ hb]
+
+theorem fmod_eq_mod {a b : Int} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : fmod a b = mod a b :=
+  mod_eq_emod Ha Hb ▸ fmod_eq_emod _ Hb
+
+theorem ofNat_fmod (m n : Nat) : ↑(m % n) = fmod m n := by cases m <;> simp [fmod]
 
 @[simp] theorem fmod_one (a : Int) : a.fmod 1 = 0 := by
   simp [fmod_def, Int.one_mul, Int.sub_self]
@@ -998,7 +1005,7 @@ theorem fmod_lt_of_pos (a : Int) {b : Int} (H : 0 < b) : a.fmod b < b :=
 
 /-! ### Theorems crossing div/mod versions -/
 
-theorem div_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : a.div b = a / b := by
+theorem div_eq_ediv_of_dvd {a b : Int} (h : b ∣ a) : Int.div a b = a / b := by
   by_cases b0 : b = 0
   · simp [b0]
   · rw [Int.div_eq_iff_eq_mul_left b0 h, ← Int.ediv_eq_iff_eq_mul_left b0 h]
@@ -1074,7 +1081,8 @@ theorem emod_bmod {x : Int} {m : Nat} : bmod (x % m) m = bmod x m := by
   rw [bmod, bmod_emod]
   rfl
 
-@[simp] theorem bmod_zero : Int.bmod 0 m = 0 := by
+-- N.B. This is renamed from bmod_zero.
+@[simp] theorem zero_bmod : Int.bmod 0 m = 0 := by
   dsimp [bmod]
   simp only [zero_emod, Int.zero_sub, ite_eq_left_iff, Int.neg_eq_zero]
   intro h

src/Init/Data/Int/Order.lean

@@ -128,9 +128,14 @@ protected theorem lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a
   · exact Int.le_antisymm h h'
   · subst h'; apply Int.le_refl
 
+protected theorem lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a :=
+  Int.lt_iff_le_not_le.2 ⟨(Int.le_total ..).resolve_right h, h⟩
+
+protected theorem not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b :=
+  (Int.lt_iff_le_not_le.1 h).2
+
 protected theorem not_le {a b : Int} : ¬a ≤ b ↔ b < a :=
-  ⟨fun h => Int.lt_iff_le_not_le.2 ⟨(Int.le_total ..).resolve_right h, h⟩,
-   fun h => (Int.lt_iff_le_not_le.1 h).2⟩
+  Iff.intro Int.lt_of_not_ge Int.not_le_of_gt
 
 protected theorem not_lt {a b : Int} : ¬a < b ↔ b ≤ a :=
   by rw [← Int.not_le, Decidable.not_not]
@@ -508,9 +513,6 @@ theorem mem_toNat' : ∀ (a : Int) (n : Nat), toNat' a = some n ↔ a = n
 
 /-! ## Order properties of the integers -/
 
-protected theorem lt_of_not_ge {a b : Int} : ¬a ≤ b → b < a := Int.not_le.mp
-protected theorem not_le_of_gt {a b : Int} : b < a → ¬a ≤ b := Int.not_le.mpr
-
 protected theorem le_of_not_le {a b : Int} : ¬ a ≤ b → b ≤ a := (Int.le_total a b).resolve_left
 
 @[simp] theorem negSucc_not_pos (n : Nat) : 0 < -[n+1] ↔ False := by
@@ -585,7 +587,11 @@ theorem add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b := .rfl
 theorem lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b := Int.add_le_add_iff_right _
 
 @[simp] theorem succ_ofNat_pos (n : Nat) : 0 < (n : Int) + 1 :=
-  lt_add_one_iff.2 (ofNat_zero_le _)
+  lt_add_one_iff.mpr (ofNat_zero_le _)
+
+theorem ofNat_not_neg (n : Nat) : (n : Int) < 0 ↔ False :=
+  (iff_false _).mpr
+  (Int.not_le_of_gt (lt_add_one_iff.mpr (ofNat_zero_le _)))
 
 theorem le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1 :=
   Int.le_of_lt (Int.lt_add_one_iff.2 h)

src/Init/Data/List/Lemmas.lean

@@ -249,7 +249,9 @@ theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a
 theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
   (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
 | [], _, n, _ => rfl
-| a :: l, _, n+1, h₁ => by rw [cons_append]; simp [get?_append_right (Nat.lt_succ.1 h₁)]
+| a :: l, _, n+1, h₁ => by
+  rw [cons_append]
+  simp [succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)]
 
 theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l →
     get? l.reverse i = get? l j

src/Init/Data/Nat/Basic.lean

@@ -248,7 +248,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m := succ_le_succ
 
 @[simp] protected theorem sub_zero (n : Nat) : n - 0 = n := rfl
 
-@[simp] theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
+theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
   | succ m ih => apply congrArg pred ih
@@ -750,15 +750,26 @@ theorem sub_one_add_one_eq_of_pos : ∀ {n}, 0 < n → (n - 1) + 1 = n
 
 /-! # sub theorems -/
 
-theorem add_sub_self_left (a b : Nat) : (a + b) - a = b := by
-  induction a with
+protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
+  induction k with
   | zero => simp
-  | succ a ih =>
-    rw [Nat.succ_add, Nat.succ_sub_succ]
-    apply ih
+  | succ k ih => simp [← Nat.add_assoc, succ_sub_succ_eq_sub, ih]
 
-theorem add_sub_self_right (a b : Nat) : (a + b) - b = a := by
-  rw [Nat.add_comm]; apply add_sub_self_left
+protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
+  rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
+
+@[simp] protected theorem add_sub_cancel (a b : Nat) : a + b - b = a :=
+  suffices a + b - (0 + b) = a by rw [Nat.zero_add] at this; assumption
+  by rw [Nat.add_sub_add_right, Nat.sub_zero]
+
+protected theorem add_sub_cancel_left (a b : Nat) : a + b - a = b := by
+  rw [Nat.add_comm]; apply Nat.add_sub_cancel
+
+@[deprecated Nat.add_sub_cancel]
+theorem add_sub_self_right : ∀(a b : Nat), (a + b) - b = a := Nat.add_sub_cancel
+
+@[deprecated Nat.add_sub_cancel_left]
+theorem add_sub_self_left : ∀(a b : Nat), (a + b) - a = b := Nat.add_sub_cancel_left
 
 theorem sub_le_succ_sub (a i : Nat) : a - i ≤ a.succ - i := by
   cases i with
@@ -770,7 +781,7 @@ theorem zero_lt_sub_of_lt (h : i < a) : 0 < a - i := by
   | zero => contradiction
   | succ a ih =>
     match Nat.eq_or_lt_of_le h with
-    | Or.inl h => injection h with h; subst h; rw [Nat.add_sub_self_left]; decide
+    | Or.inl h => injection h with h; subst h; rw [Nat.add_sub_cancel_left]; decide
     | Or.inr h =>
       have : 0 < a - i := ih (Nat.lt_of_succ_lt_succ h)
       exact Nat.lt_of_lt_of_le this (Nat.sub_le_succ_sub _ _)
@@ -799,22 +810,6 @@ theorem add_sub_of_le {a b : Nat} (h : a ≤ b) : a + (b - a) = b := by
 @[simp] protected theorem sub_add_cancel {n m : Nat} (h : m ≤ n) : n - m + m = n := by
   rw [Nat.add_comm, Nat.add_sub_of_le h]
 
-protected theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m := by
-  induction k with
-  | zero => simp
-  | succ k ih => simp [← Nat.add_assoc, ih]
-
-protected theorem add_sub_add_left (k n m : Nat) : (k + n) - (k + m) = n - m := by
-  rw [Nat.add_comm k n, Nat.add_comm k m, Nat.add_sub_add_right]
-
-@[simp] protected theorem add_sub_cancel (n m : Nat) : n + m - m = n :=
-  suffices n + m - (0 + m) = n by rw [Nat.zero_add] at this; assumption
-  by rw [Nat.add_sub_add_right, Nat.sub_zero]
-
-protected theorem add_sub_cancel_left (n m : Nat) : n + m - n = m :=
-  show n + m - (n + 0) = m from
-  by rw [Nat.add_sub_add_left, Nat.sub_zero]
-
 protected theorem add_sub_assoc {m k : Nat} (h : k ≤ m) (n : Nat) : n + m - k = n + (m - k) := by
  cases Nat.le.dest h
  rename_i l hl
@@ -1001,7 +996,7 @@ theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   funext fun α => funext fun f => funext fun n => funext fun init =>
   let rec go : ∀ m n, foldTR.loop f (m + n) m (fold f n init) = fold f (m + n) init
     | 0,      n => by simp [foldTR.loop]
-    | succ m, n => by rw [foldTR.loop, add_sub_self_left, succ_add]; exact go m (succ n)
+    | succ m, n => by rw [foldTR.loop, Nat.add_sub_cancel_left, succ_add]; exact go m (succ n)
   (go n 0).symm
 
 @[csimp] theorem any_eq_anyTR : @any = @anyTR :=
@@ -1009,7 +1004,7 @@ theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   let rec go : ∀ m n,  (any f n || anyTR.loop f (m + n) m) = any f (m + n)
     | 0,      n => by simp [anyTR.loop]
     | succ m, n => by
-      rw [anyTR.loop, add_sub_self_left, ← Bool.or_assoc, succ_add]
+      rw [anyTR.loop, Nat.add_sub_cancel_left, ← Bool.or_assoc, succ_add]
       exact go m (succ n)
   (go n 0).symm
 
@@ -1018,7 +1013,7 @@ theorem not_gt_eq (a b : Nat) : (¬ (a > b)) = (a ≤ b) :=
   let rec go : ∀ m n,  (all f n && allTR.loop f (m + n) m) = all f (m + n)
     | 0,      n => by simp [allTR.loop]
     | succ m, n => by
-      rw [allTR.loop, add_sub_self_left, ← Bool.and_assoc, succ_add]
+      rw [allTR.loop, Nat.add_sub_cancel_left, ← Bool.and_assoc, succ_add]
       exact go m (succ n)
   (go n 0).symm
 

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -271,7 +271,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
   induction i generalizing n x with
   | zero =>
     match n with
-    | 0 => simp
+    | 0 => simp [succ_sub_succ_eq_sub]
     | n+1 =>
       simp [not_decide_mod_two_eq_one]
       omega
@@ -279,7 +279,7 @@ theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
     simp only [testBit_succ]
     match n with
     | 0 =>
-      simp [decide_eq_false]
+      simp [succ_sub_succ_eq_sub, decide_eq_false]
     | n+1 =>
       rw [Nat.two_pow_succ_sub_succ_div_two, ih]
       · simp [Nat.succ_lt_succ_iff]

src/Init/Data/Nat/Div.lean

@@ -379,5 +379,4 @@ theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
   | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
   | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
 
-
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -9,39 +9,59 @@ import Init.Meta
 
 namespace Nat
 
-protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
+protected theorem dvd_def (a b : Nat) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
 
-protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
+@[simp] protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
 
-protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
-protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩
+@[simp] protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
+
+protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
+  let ⟨c, H'⟩ := h; H'.trans c.zero_mul
+
+@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
+  Iff.intro Nat.eq_zero_of_zero_dvd
+            (fun h => h.symm ▸ Nat.dvd_refl 0)
+
+@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
 
 protected theorem dvd_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
   match h₁, h₂ with
   | ⟨d, (h₃ : b = a * d)⟩, ⟨e, (h₄ : c = b * e)⟩ =>
     ⟨d * e, show c = a * (d * e) by simp[h₃,h₄, Nat.mul_assoc]⟩
 
-protected theorem eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0 :=
-  let ⟨c, H'⟩ := h; H'.trans c.zero_mul
-
-@[simp] protected theorem zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0 :=
-  ⟨Nat.eq_zero_of_zero_dvd, fun h => h.symm ▸ Nat.dvd_zero 0⟩
+protected theorem dvd_mul_left  (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
+protected theorem dvd_mul_right (a b : Nat) : a ∣ a * b := ⟨b, rfl⟩
 
 protected theorem dvd_add {a b c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c :=
   let ⟨d, hd⟩ := h₁; let ⟨e, he⟩ := h₂; ⟨d + e, by simp [Nat.left_distrib, hd, he]⟩
 
-protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
-  ⟨Nat.dvd_add h,
-    match m, h with
+-- Note. This removes unnecessary condition
+protected theorem dvd_sub : ∀ {a b c : Nat}, a ∣ b → a ∣ c → a ∣ b - c
+  | a, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Nat.mul_sub_left_distrib]⟩
+
+protected theorem dvd_add_left {a b c : Nat} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b :=
+  Iff.intro
+    (match c, h with
     | _, ⟨d, rfl⟩ => fun ⟨e, he⟩ =>
-      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel_left]⟩⟩
+      ⟨e - d, by rw [Nat.mul_sub_left_distrib, ← he, Nat.add_sub_cancel]⟩)
+    (Nat.dvd_add · h)
 
-protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := by
-  rw [Nat.add_comm]; exact Nat.dvd_add_iff_right h
+protected theorem dvd_add_right {a b c : Nat} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c := by
+  rw [Nat.add_comm]; exact Nat.dvd_add_left h
 
-theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
-  have := Nat.dvd_add_iff_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)
-  by rwa [mod_add_div] at this
+/--
+This is replaced by (dvd_add_left _).symm for consistency with Int version.
+-/
+@[deprecated Nat.dvd_add_left]
+protected theorem dvd_add_iff_left {k m n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n :=
+  (Nat.dvd_add_left h).symm
+
+/--
+This is replaced by (dvd_add_right _).symm for consistency with Int version.
+-/
+@[deprecated Nat.dvd_add_right]
+protected theorem dvd_add_iff_right {k m n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n :=
+  (Nat.dvd_add_right h).symm
 
 theorem le_of_dvd {m n : Nat} (h : 0 < n) : m ∣ n → m ≤ n
   | ⟨k, e⟩ => by
@@ -59,11 +79,13 @@ protected theorem dvd_antisymm : ∀ {m n : Nat}, m ∣ n → n ∣ m → m = n
   | 0, _, h₁, _ => (Nat.eq_zero_of_zero_dvd h₁).symm
   | _+1, _+1, h₁, h₂ => Nat.le_antisymm (le_of_dvd (succ_pos _) h₁) (le_of_dvd (succ_pos _) h₂)
 
+theorem dvd_mod_iff {k m n : Nat} (h: k ∣ n) : k ∣ m % n ↔ k ∣ m :=
+  have := (Nat.dvd_add_left <| Nat.dvd_trans h <| Nat.dvd_mul_right n (m / n)).symm
+  by rwa [mod_add_div] at this
+
 theorem pos_of_dvd_of_pos {m n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m :=
   Nat.pos_of_ne_zero fun m0 => Nat.ne_of_gt H2 <| Nat.eq_zero_of_zero_dvd (m0 ▸ H1)
 
-@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
-
 theorem eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1 := Nat.dvd_antisymm H n.one_dvd
 
 theorem mod_eq_zero_of_dvd {m n : Nat} (H : m ∣ n) : n % m = 0 := by
@@ -75,7 +97,7 @@ theorem dvd_of_mod_eq_zero {m n : Nat} (H : n % m = 0) : m ∣ n := by
   rwa [H, Nat.zero_add] at this
 
 theorem dvd_iff_mod_eq_zero (m n : Nat) : m ∣ n ↔ n % m = 0 :=
-  ⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩
+  Iff.intro mod_eq_zero_of_dvd dvd_of_mod_eq_zero
 
 instance decidable_dvd : @DecidableRel Nat (·∣·) :=
   fun _ _ => decidable_of_decidable_of_iff (dvd_iff_mod_eq_zero _ _).symm
@@ -106,9 +128,6 @@ protected theorem dvd_of_mul_dvd_mul_left
 protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
   rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
 
-theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
-  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
-
 protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
   | ⟨e, he⟩, ⟨f, hf⟩ =>
     ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩

src/Init/Data/Nat/Lemmas.lean

@@ -830,3 +830,42 @@ instance decidableExistsLT [h : DecidablePred p] : DecidablePred fun n => ∃ m
 instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Nat, m ≤ n ∧ p m :=
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
+
+theorem dvd_sub_iff {a b : Nat} (h : a ≥ b) : b ∣ (a - b) ↔ b ∣ a := by
+  apply Iff.intro
+  · intro ⟨c, p⟩
+    replace p := Nat.eq_add_of_sub_eq h p
+    apply Exists.intro (c+1)
+    simp [Nat.mul_add, p]
+  · intro ⟨c, p⟩
+    match c with
+    | 0 =>
+      simp_all
+    | c + 1 =>
+      apply Exists.intro c
+      simp [p, Nat.mul_add]
+
+theorem succ_div (a b : Nat) : (a + 1) / b = if b ∣ (a+1) then a / b + 1 else a / b := by
+  match b with
+  | 0 =>
+    simp
+  | b + 1 =>
+    match Nat.lt_trichotomy (a+1) (b+1) with
+    | Or.inl q =>
+      have p : a < b + 1 := Nat.le_succ_of_le (Nat.le_of_succ_le_succ q)
+      split
+      · rename_i dvd
+        replace dvd := Nat.mod_eq_zero_of_dvd dvd
+        simp only [Nat.mod_eq_of_lt q] at dvd
+      · rename_i dvd
+        simp only [Nat.div_eq_of_lt, p, q]
+    | Or.inr (Or.inl p) =>
+      simp [←p, Nat.div_self, Nat.div_eq_of_lt]
+    | Or.inr (Or.inr p) =>
+      replace p : a ≥ b + 1 := Nat.le_of_succ_le_succ p
+      have q : a + 1 ≥ b + 1 := Nat.le_succ_of_le p
+      have r := succ_div (a - (b + 1)) (b + 1)
+      simp only [←Nat.sub_add_comm p, Nat.dvd_sub_iff q] at r
+      have b_pos : 0 < b + 1 := Nat.succ_le_succ (Nat.zero_le b)
+      rw [Nat.div_eq_sub_div b_pos p, Nat.div_eq_sub_div b_pos q, r]
+      split <;> simp

src/Init/Omega/IntList.lean

@@ -307,7 +307,7 @@ theorem dvd_gcd (xs : IntList) (c : Nat) (w : ∀ {a : Int}, a ∈ xs → (c : I
     c ∣ xs.gcd := by
   simp only [Int.ofNat_dvd_left] at w
   induction xs with
-  | nil => have := Nat.dvd_zero c; simp at this; exact this
+  | nil => have := Nat.dvd_zero c; simp
   | cons x xs ih =>
     simp
     apply Nat.dvd_gcd

src/Lean/Elab/CheckTactic.lean

@@ -32,16 +32,13 @@ def elabCheckTactic : CommandElab := fun stx => do
       let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
       match goals with
       | [] =>
-        throwErrorAt stx
-          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
+        throwError m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
       | [next] => do
-        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
+        let (val, _, _) ← matchCheckGoalType (←next.getType)
         if !(← Meta.withReducible <| isDefEq val expTerm) then
-          throwErrorAt stx
-            m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
+          throwError m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
       | _ => do
-        throwErrorAt stx
-          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
+        throwError m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
 
 @[builtin_command_elab Lean.Parser.checkTacticFailure]
 def elabCheckTacticFailure : CommandElab := fun stx => do
@@ -58,7 +55,7 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
           pure ()
         | some (gls, _) =>
           let ppGoal (g : MVarId) := do
-                let (val, _type, _u) ← matchCheckGoalType stx (← g.getType)
+                let (val, _type, _u) ← matchCheckGoalType (← g.getType)
                 pure m!"{indentExpr val}"
           let msg ←
             match gls with
@@ -69,7 +66,7 @@ def elabCheckTacticFailure : CommandElab := fun stx => do
                 let app m g := do pure <| m ++ (←ppGoal g)
                 let init := m!"{tactic} expected to fail on {t}, but returned goals:"
                 gls.foldlM (init := init) app
-          throwErrorAt stx msg
+          throwError msg
 
 @[builtin_macro Lean.Parser.checkSimp]
 def expandCheckSimp : Macro := fun stx => do

src/Lean/Meta/CheckTactic.lean

@@ -12,13 +12,13 @@ def mkCheckGoalType (val type : Expr) : MetaM Expr := do
   let lvl ← mkFreshLevelMVar
   pure <| mkApp2 (mkConst ``CheckGoalType [lvl]) type val
 
-def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := do
+def matchCheckGoalType (goalType : Expr) : MetaM (Expr × Expr × Level) := do
   let u ← mkFreshLevelMVar
   let type ← mkFreshExprMVar (some (.sort u))
   let val  ← mkFreshExprMVar (some type)
   let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
   if !(← isDefEq goalType extType) then
-    throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
+    throwError "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
   pure (val, type, u)
 
 end Lean.Meta.CheckTactic

src/Lean/Util.lean

@@ -25,6 +25,7 @@ import Lean.Util.ReplaceLevel
 import Lean.Util.FoldConsts
 import Lean.Util.SCC
 import Lean.Util.TestExtern
+import Lean.Util.TestNormalForms
 import Lean.Util.OccursCheck
 import Lean.Util.HasConstCache
 import Lean.Util.FileSetupInfo

src/Lean/Util/TestNormalForms.lean

@@ -0,0 +1,493 @@
+import Lean.Elab.Command
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Meta
+import Lean.Meta.CheckTactic
+import Lean.Parser.Term
+
+open Lean Meta Elab Term Command CheckTactic
+
+/-
+This module defines a term generation and testing framework that
+checks whether generated terms have a specified normal form.  It
+is defined in the `Lean.Test.NormalForms` namespace.
+
+To use it, you need to define a few things:
+
+1. a new datatype for representing terms in the language
+2. a data type for representing types
+3. a function for computing the type from the term
+4. a function for rendering the term into Lean syntax
+5. an evaluation function for producing the expected normal form from the term syntax
+6. a list of variable generators for generating variables with different types in the language
+7. a list of operators `Op` for building up terms in the language.
+
+Once this is done, you can pass this information into
+`testNormalForms`.
+-/
+namespace Lean.Test.NormalForms
+
+-- | A `Op` is a first order operation for generating values with a given type.
+structure Op (tp : Type) (val : Type) where
+  args : Array tp
+  result : tp
+  apply : Array val → val
+ deriving Inhabited
+
+def mkOp (args : List tp) (result : tp) (apply : Array val → val) : Op tp val :=
+  { apply := apply, args := args.toArray, result }
+
+def Op.map (op : Op x val) (f : x → y) : Op y val :=
+  { apply := op.apply, args := op.args.map f, result := f op.result }
+
+/--
+Contextual information needed to generate terms.
+-/
+structure GenCtx (term : Type) where
+  -- Maps type indices to operator for corresponding type.
+  -- Types use type indices.
+  ops : Array (Array (Op Nat term))
+  /-- Maps type indices to variables for that type. -/
+  vars : Array (Array term)
+  /- Operators to use for patterns at top of terms -/
+  topOps : Array (Op Nat term)
+  /- Returns the expected reduction of a term -/
+  expected : term → term
+  /- Predicate that returns true if terms are equal-/
+  eq : term → term → Bool
+  /-- Maximum term size -/
+  maxTermSize : Nat
+  /-- Maximum depth of terms -/
+  maxDepth : Nat
+  /-- Maximum number of variables -/
+  maxVarCount : Nat
+  /- Local context variables defined in -/
+  lctx : LocalContext
+  /- Local instances for variables -/
+  linst : LocalInstances
+
+namespace GenCtx
+
+/-- `var ctx tp idx` returns a term denoting `i`th variable with type `tp`. -/
+def var (ctx : GenCtx term) (tp : Nat) (idx : Nat) : Option term :=
+  if g : tp < ctx.vars.size then
+    let a := ctx.vars[tp]'g
+    if h : idx < a.size then
+      some (a[idx]'h)
+    else
+      none
+  else
+    none
+
+end GenCtx
+
+/-- An operator together with a set of terms to apply to it. -/
+structure PartialApp (term : Type) where
+  /-- Operator to generate -/
+  op : Op Nat term
+  /-- Terms constructed so far -/
+  terms : Array term
+
+namespace PartialApp
+
+def fromOp (op : Op Nat term) : PartialApp term :=
+  { op, terms := .mkEmpty op.args.size }
+
+end PartialApp
+
+/--
+A partial term contains the initial part of a term as constructed from a
+left-to-right preorder traversal.
+
+It stores additional information needed to ensure the ultimate term satisfies
+the generation constraints on term size and number of variables.
+
+The operations for constructing this ensures the term is well-formed
+with respect to the signature and is not a complete term.
+-/
+structure PartialTerm (term : Type) where
+  /-- Stack of partially built term (must be non-empty) -/
+  termStack : Array (PartialApp term)
+  /-- Maximum number of additional operations that may be added. -/
+  remTermSize : Nat
+  /-- Variables used with type index. -/
+  usedVars : Array Nat
+  deriving Inhabited
+
+namespace PartialTerm
+
+/--
+Create an initial partial term from an operator.
+
+If the operator is a constant, then this just returns a complete terms.
+-/
+def init (maxTermSize : Nat) (maxDepth : Nat) (op : Op Nat term) : term ⊕ PartialTerm term :=
+  if op.args.isEmpty then
+    .inl (op.apply #[])
+  else
+    .inr {
+      termStack := #[PartialApp.fromOp op],
+      remTermSize := maxTermSize - (1 + op.args.size),
+      usedVars := #[]
+    }
+
+partial def push (p : PartialTerm term) (t : term) : term ⊕ PartialTerm term :=
+  match p.termStack.back? with
+  | none => .inl t
+  | some { op, terms } =>
+    let p := { p with termStack := p.termStack.pop }
+    let terms := terms.push t
+    if terms.size = op.args.size then
+      let v := op.apply terms
+      push p v
+    else
+      .inr { p with termStack := p.termStack.push { op, terms } }
+
+/-- Push an operator to the stack -/
+def pushOp (p : PartialTerm term) (op : Op Nat term) : PartialTerm term :=
+  { termStack   := p.termStack.push (.fromOp op)
+    remTermSize := p.remTermSize - op.args.size,
+    usedVars := p.usedVars
+  }
+
+end PartialTerm
+
+/--
+Term generator
+-/
+structure TermGen (term : Type) where
+  sofar : Array term := #[]
+  pending : Array (PartialTerm term) := #[]
+  deriving Inhabited
+
+namespace TermGen
+
+/-- Return true if generator will return no more terms. -/
+def isEmpty (s: TermGen term) : Bool := s.sofar.isEmpty && s.pending.isEmpty
+
+def pop (s : TermGen term) : Option (Nat × PartialTerm term × TermGen term) :=
+  if s.pending.isEmpty then
+    .none
+  else
+    let { sofar, pending } := s
+    let next := pending.back
+    let pending := pending.pop
+    match next.termStack.back? with
+    | none =>
+      panic! "Term stack empty"
+    | some app =>
+      let tp := app.op.args[app.terms.size]!
+      some (tp, next, { sofar, pending })
+
+def add (gen : TermGen term)  (val : term ⊕ PartialTerm term) : TermGen term :=
+  let { sofar, pending } := gen
+  match val with
+  | .inl v =>  { sofar := sofar.push v, pending }
+  | .inr p => { sofar, pending := pending.push p }
+
+/-
+`push s next v` adds the result of `next.push v` to the state.
+
+This only adds terms that are irreducible.
+-/
+def push (gen : TermGen term) (ctx : GenCtx term) (next : PartialTerm term) (v : term) : TermGen term :=
+  let exp := ctx.expected v
+  if ctx.eq exp v then
+    gen.add (next.push v)
+  else
+    gen
+
+def pushOp (gen : TermGen term) (ctx : GenCtx term) (next : PartialTerm term) (op : Op Nat term) :=
+  if op.args.isEmpty then
+    gen.push ctx next (op.apply #[])
+  else if op.args.size ≤ next.remTermSize ∧ next.termStack.size + 1 < ctx.maxDepth then
+    { gen with pending := gen.pending.push (next.pushOp op) }
+  else
+    gen
+
+/-- Create state that will explore all terms in context -/
+def addOpInstances (s : TermGen term) (ctx : GenCtx term) (op : Op Nat term) : TermGen term :=
+  s.add (PartialTerm.init ctx.maxTermSize ctx.maxDepth op)
+
+/-- Create state that will explore all terms in context -/
+def init (ctx : GenCtx term) : TermGen term :=
+  ctx.topOps.foldl (init := {}) (·.addOpInstances ctx ·)
+
+end TermGen
+
+/--
+Generate terms until we reach the limit.
+-/
+partial
+def generateTerms
+    (ctx : GenCtx term)
+    (gen : TermGen term)
+    (limit : Nat := 0) :
+    Array term × TermGen term :=
+  if limit > 0 ∧ gen.sofar.size ≥ limit then
+    -- Stop if we hit term limit
+    (gen.sofar, { gen with sofar := #[] })
+  else
+    match gen.pop with
+    | none =>
+      -- stop when out of terms
+      (gen.sofar, { gen with sofar := #[] })
+    | some (tp, next, gen) =>
+      -- Add previously used variables to term
+      let addVar (next : PartialTerm term) (i : Nat) (gen : TermGen term) : TermGen term :=
+            -- If the previous variable i matches type, then add it to generator
+            if next.usedVars[i]! = tp then
+              match ctx.var tp i with
+              | some v => gen.push ctx next v
+              | none => gen
+            else
+              gen
+      let s := next.usedVars.size.fold (init := gen) (addVar next)
+      let s :=
+        let var := next.usedVars.size
+        if var < ctx.maxVarCount then
+          let next := { next with usedVars := next.usedVars.push tp }
+          addVar next var s
+        else
+          s
+      generateTerms ctx (ctx.ops[tp]!.foldl (init := s) (·.pushOp ctx next ·)) limit
+
+/-
+`addScopeVariables` extends the local context and instances with a copy of the
+variables in the scope (which must be non-empty).
+-/
+def addScopeVariables (lctx : LocalContext) (linst : LocalInstances) (scope : Scope) (idx : Nat) :
+    CoreM (LocalContext × LocalInstances × Ident) := do
+  let act := Term.elabBindersEx scope.varDecls fun vars => do pure (vars, ← (read : MetaM Meta.Context))
+  let mctx := { lctx := lctx, localInstances := linst }
+  let (((vars, mctx), _tstate), _mstate) ← act |>.run |>.run mctx
+  if vars.isEmpty then
+    throwError "No variables declared"
+  let fv := vars[0]!.snd |>.fvarId!
+  let rec drop (nm : Name) :=
+        match nm with
+        | .str .anonymous s => pure (.str .anonymous s!"{s}{idx}")
+        | .str nm _ => drop nm
+        | .num nm _ => drop nm
+        | .anonymous => throwError "Anonymous variable declared."
+  let nm ← drop (mctx.lctx.get! fv |>.userName)
+  let lctx := mctx.lctx.setUserName fv nm
+  pure (lctx, mctx.localInstances, mkIdent nm)
+
+def addVariables (cmdCtx : Command.Context) (cmdState : Command.State) (lctx : LocalContext) (linst : LocalInstances) (n : Nat) (cmd : Command) :
+    CoreM (LocalContext × LocalInstances × Array Ident) := do
+  let (_, s) ←  elabCommand cmd.raw |>.run cmdCtx |>.run cmdState
+  let scope := s.scopes.head!
+  Nat.foldM (n := n) (init := (lctx, linst, .mkEmpty n)) fun i (lctx, linst, a) => do
+    let (lctx, linst, ident) ← addScopeVariables lctx linst scope i
+    pure (lctx, linst, a.push ident)
+
+structure GenStats where
+  maxTermSize : Nat := 9
+  maxDepth : Nat := 3
+  maxVarCount : Nat := 3
+
+
+structure VarDecl (tp : Type) where
+  idx : Nat
+  ident : TSyntax `ident
+  type : tp
+  deriving Inhabited, Repr
+
+instance : BEq (VarDecl tp) where
+  beq x y := x.idx == y.idx
+
+instance : Hashable (VarDecl tp) where
+  hash v := hash v.idx
+
+/--
+
+-/
+class GenTerm (term : Type) (type : outParam Type) extends BEq term where
+  mkVar : VarDecl type → term
+  render : term → TermElabM Term
+
+def mkCtx [BEq tp] [Hashable tp] [BEq term]
+    (types : Array tp)
+    (ops : List (Op tp term))
+    (varGen : List (tp × CoreM Command))
+    (mkVar : VarDecl tp → term)
+    (expected : term → term)
+    (stats : GenStats)
+    (topOps : List (Op tp term) := ops) : CommandElabM (GenCtx term) := do
+  let typeMap : HashMap tp Nat := Nat.fold (n := types.size) (init := {}) fun i s =>
+        if p : i < types.size then
+          s.insert types[i] i
+        else
+          s
+  let typeFn (t : tp) := typeMap.findD t 0
+  let addOp (a : Array (Array (Op Nat term))) (op : Op tp term) :=
+        let op := op.map typeFn
+        a.modify op.result (·.push op)
+  let init := Array.ofFn (n := types.size) (fun _ => #[])
+  let ops := ops.foldl (init := init) addOp
+  let ops := ops.map (·.reverse)
+  let topOps := topOps.toArray.map (·.map typeFn)
+  let (lctx, linst, vars) ← liftCoreM do
+    let coreCtx ← read
+    let coreState ← get
+    let fileName := coreCtx.fileName
+    let fileMap  := coreCtx.fileMap
+    let env := coreState.env
+    let maxRecDepth := coreCtx.maxRecDepth
+    let cmdCtx : Command.Context := { fileName, fileMap, tacticCache? := none }
+    let cmdState : Command.State := { env, maxRecDepth }
+    let addVars (p : LocalContext × LocalInstances × Array (Array term))
+                (q : tp × CoreM Command) :
+                CoreM (LocalContext × LocalInstances × _) := do
+          let (lctx, linst, a) := p
+          let (type, gen) := q
+          let cmd ← gen
+          let (lctx, linst, vars) ← addVariables cmdCtx cmdState lctx linst stats.maxVarCount cmd
+          let vars := Array.ofFn (n := vars.size) fun j => mkVar { idx := j.val, ident := vars[j], type }
+          let type := typeFn type
+          pure (lctx, linst, a.modify type (fun _ => vars))
+    let vars := Array.ofFn (n := types.size) fun _ => #[]
+    varGen.foldlM (init := ({}, {}, vars)) addVars
+  let maxTermSize : Nat := stats.maxTermSize
+  let maxDepth : Nat := stats.maxDepth
+  let maxVarCount : Nat := stats.maxVarCount
+  pure { ops, vars, expected := @expected, eq := BEq.beq, topOps, maxTermSize, maxDepth, maxVarCount, lctx, linst }
+
+/-
+runTest
+-/
+def runTest (render : term → TermElabM Syntax.Term) (simp : term → term) (tac : Syntax.Tactic) (tm : term) : TermElabM Unit := do
+  withoutModifyingEnv $ do
+    let res := simp tm
+    let t ← render tm
+    let exp ← render res
+    let u ← Lean.Elab.Term.elabTerm t none
+    let type ← inferType u
+    let checkGoalType ← mkCheckGoalType u type
+    let expTerm ← Lean.Elab.Term.elabTerm exp (some type)
+    let mvar ← mkFreshExprMVar (.some checkGoalType)
+    let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
+    match goals with
+    | [next] => do
+      let (val, _, _) ← matchCheckGoalType (←next.getType)
+      if !(← Meta.withReducible <| isDefEq val expTerm) then
+        logError m!"{indentExpr u} reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
+    | [] =>
+      logError m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
+    | _ =>
+      logError m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
+
+/-
+Create core context for running tactic tests in.
+-/
+private def mkCoreContext (ctx : Command.Context) (options : Options) (maxRecDepth : Nat) (initHeartbeats : Nat) : Core.Context :=
+  { fileName       := ctx.fileName
+    fileMap        := ctx.fileMap
+    options,
+    currRecDepth   := ctx.currRecDepth
+    maxRecDepth,
+    ref            := ctx.ref
+    initHeartbeats,
+    currMacroScope := ctx.currMacroScope }
+
+/-- Runs term elaborator in base context. -/
+def runTermElabM (cctx : Core.Context) (cstate : Core.State) (mctx : Meta.Context) (act : TermElabM Unit)
+    : BaseIO (Except Exception MessageLog) := do
+  let r ← act.run |>.run mctx |>.run cctx cstate |>.toBaseIO
+  match r with
+  | .error e =>
+    pure (.error e)
+  | .ok ((((), _termS), _metaS), coreS) =>
+    pure (.ok coreS.messages)
+
+/--
+Tests that a tactic applied to exhaustively generated terms matches
+expectations.
+
+To allow testing consistent treatment of operators on multiple types, the normal
+form testing facility is defined using terms over an arbitrary simply-typed
+`term` data type that uses types using the `type` parameter.  This
+representation should be chosen to make specifying the semantics of the tactic
+as simple as possible.
+
+Term must be an instance of the `GenTerm` class so the testing facility knows
+how to render user terms into Lean terms.  Additionally, users should provide
+operators and variable constructors for building terms up.
+
+`stats` controls parameters on the size of terms generated.
+-/
+partial def testNormalForms {val type : Type} [BEq type] [Hashable type] [GenTerm val type]
+      (types : List type)
+      (ops : List (Op type val))
+      (vars : List (type × CoreM Command))
+      (expected : val → val)
+      (stats : GenStats)
+      (tac : Option Syntax.Tactic := none)
+      (topOps : List (Op type val) := ops)
+      (concurrent : Bool := true) : CommandElabM Unit := do
+
+  let tac ← tac.getDM `(tactic|try simp)
+  let ctx ← mkCtx (types := types.toArray) (ops := ops) (topOps := topOps) (varGen := vars) (mkVar := GenTerm.mkVar) expected (stats := stats)
+
+  let cmdCtx : Command.Context ← read
+  let s ← get
+  let maxRecDepth := s.maxRecDepth
+  let heartbeats ← IO.getNumHeartbeats
+  let options ← getOptions
+  -- Create core context for running tests.
+  let cctx := mkCoreContext cmdCtx options maxRecDepth heartbeats
+  -- Create core context for running tests.
+  let cstate : Core.State := {
+        env := s.env,
+        ngen := s.ngen,
+        traceState := s.traceState,
+        infoState.enabled := s.infoState.enabled
+    }
+  -- Meta context setup for variables created by mkCtx
+  let mctx : Meta.Context := { lctx := ctx.lctx, localInstances := ctx.linst }
+  let gen := TermGen.init ctx
+  if concurrent then
+    let limit := 800
+    let rec loop (gen : TermGen val) (cnt : Nat) (tasks : Array (Task (Except Exception MessageLog))) : BaseIO (Nat × Array (Task _)) := do
+      if gen.isEmpty then
+        return (cnt, tasks)
+      else
+        let (terms, gen) := generateTerms ctx gen (limit := limit)
+        let runTests := do
+              for tm in terms do
+                if ← IO.checkCanceled then
+                  break
+                runTest GenTerm.render expected tac tm
+        let t ← runTests |> runTermElabM cctx cstate mctx |>.asTask
+        loop gen (cnt + terms.size) (tasks.push t)
+    let (cnt, tasks) ←
+      profileitM Exception "normal form generation" (←getOptions) (decl := .anonymous) do
+        liftIO (loop gen 0 #[])
+    trace[Test.normalforms] "generated {cnt} tests running in {tasks.size} threads."
+    profileitM Exception "normal form execution" (←getOptions) do
+      for i in [0:tasks.size] do
+        if ← IO.checkCanceled then
+          break
+        let act := tasks[i]!
+        match act.get with
+        | .error e =>
+          -- Cancel all tasks after this one
+          (tasks |>.toSubarray (start := i+1) |>.forM IO.cancel : BaseIO Unit)
+          throw e
+        | .ok m =>
+          modify fun s => { s with messages := s.messages ++ m }
+  else
+    let r ← runTermElabM cctx cstate mctx <|
+      let (terms, _) := generateTerms ctx gen (limit := 0)
+      for tm in terms do
+        if ← IO.checkCanceled then
+          break
+        runTest GenTerm.render expected tac tm
+    match r with
+    | .error e => throw e
+    | .ok m => modify fun s => { s with messages := s.messages ++ m }
+
+builtin_initialize
+  registerTraceClass `Test.normalforms
+
+end Lean.Test.NormalForms

tests/playground/bool_exhaust_test.lean

@@ -1,439 +1,10 @@
-import Lean.Elab.Command
-import Lean.Elab.Tactic.ElabTerm
-import Lean.Elab.Tactic.Meta
-import Lean.Meta.CheckTactic
-import Lean.Parser.Term
+import Lean.Util.TestNormalForms
 
-open Lean Lean.Meta Lean.Elab Lean.Elab.Term Lean.Elab.Command
-open Lean.Meta.CheckTactic
-
-
--- | A `Op` is a first order operation for generating values with a given type.
-structure Op (tp : Type) (val : Type) where
-  args : Array tp
-  result : tp
-  apply : Array val → val
- deriving Inhabited
-
-def mkOp (args : List tp) (result : tp) (apply : Array val → val) : Op tp val :=
-  { apply := apply, args := args.toArray, result }
-
-def Op.map (op : Op x val) (f : x → y) : Op y val :=
-  { apply := op.apply, args := op.args.map f, result := f op.result }
-
-class HasType (val : Type) (type : outParam Type) where
-  typeOf : val → type
-
-class Value (val : Type) where
-  render : val → TermElabM Term
-
-/--
-Contextual information needed to generate terms.
--/
-structure GenCtx (val : Type) where
-  -- Maps type indices to operator for corresponding type.
-  -- Types use type indices.
-  ops : Array (Array (Op Nat val))
-  /- Operators to use for patterns at top of terms -/
-  topOps : Array (Op Nat val)
-  /-- Maximum term size -/
-  maxTermSize : Nat
-  /-- Maximum depth of terms -/
-  maxDepth : Nat
-  /-- Maximum number of variables -/
-  maxVarCount : Nat
-  /- Local context variables defined in -/
-  lctx : LocalContext
-  /- Local instances for variables -/
-  linst : LocalInstances
-  /-- Maps type indices to variables for that type. -/
-  vars : Array (Array val)
-
-namespace GenCtx
-
-/-- `var ctx tp idx` returns a term denoting `i`th variable with type `tp`. -/
-def var (ctx : GenCtx val) (tp : Nat) (idx : Nat) : Option val :=
-  if g : tp < ctx.vars.size then
-    let a := ctx.vars[tp]'g
-    if h : idx < a.size then
-      some (a[idx]'h)
-    else
-      none
-  else
-    none
-
-end GenCtx
-
-/-- An operator together with a set of terms to apply to it. -/
-structure PartialApp (term : Type) where
-  /-- Operator to generate -/
-  op : Op Nat term
-  /-- Terms constructed so far -/
-  terms : Array term
-
-namespace PartialApp
-
-def fromOp (op : Op Nat term) : PartialApp term :=
-  { op, terms := .mkEmpty op.args.size }
-
-end PartialApp
-
-/--
-A partial term contains the initial part of a term as constructed from a
-left-to-right preorder traversal.
-
-It stores additional information needed to ensure the ultimate term satisfies
-the generation constraints on term size and number of variables.
-
-The operations for constructing this ensures the term is well-formed
-with respect to the signature and is not a complete term.
--/
-structure PartialTerm (term : Type) where
-  /-- Stack of partially built term (must be non-empty) -/
-  termStack : Array (PartialApp term)
-  /-- Maximum number of additional operations that may be added. -/
-  remTermSize : Nat
-  /-- Variables used with type index. -/
-  usedVars : Array Nat
-  deriving Inhabited
-
-namespace PartialTerm
-
-/--
-Create an initial partial term from an operator.
-
-If the operator is a constant, then this just returns a complete terms.
--/
-def init (maxTermSize : Nat) (maxDepth : Nat) (op : Op Nat term) : term ⊕ PartialTerm term :=
-  if op.args.isEmpty then
-    .inl (op.apply #[])
-  else
-    .inr {
-      termStack := #[PartialApp.fromOp op],
-      remTermSize := maxTermSize - (1 + op.args.size),
-      usedVars := #[]
-    }
-
-partial def push (p : PartialTerm term) (t : term) : term ⊕ PartialTerm term :=
-  match p.termStack.back? with
-  | none => .inl t
-  | some { op, terms } =>
-    let p := { p with termStack := p.termStack.pop }
-    let terms := terms.push t
-    if terms.size = op.args.size then
-      let v := op.apply terms
-      push p v
-    else
-      .inr { p with termStack := p.termStack.push { op, terms } }
-
-/-- Push an operator to the stack -/
-def pushOp (p : PartialTerm term) (op : Op Nat term) : PartialTerm term :=
-  { termStack   := p.termStack.push (.fromOp op)
-    remTermSize := p.remTermSize - op.args.size,
-    usedVars := p.usedVars
-  }
-
-end PartialTerm
-
-/--
-Term generator
--/
-structure Gen (term : Type) where
-  sofar : Array term := #[]
-  pending : Array (PartialTerm term) := #[]
-  deriving Inhabited
-
-namespace Gen
-
-/-- Return true if generator will return no more terms. -/
-def isEmpty (s: Gen term) : Bool := s.sofar.isEmpty && s.pending.isEmpty
-
-def pop (s : Gen term) : Option (Nat × PartialTerm term × Gen term) :=
-  if s.pending.isEmpty then
-    .none
-  else
-    let { sofar, pending } := s
-    let next := pending.back
-    let pending := pending.pop
-    match next.termStack.back? with
-    | none =>
-      panic! "Term stack empty"
-    | some app =>
-      let tp := app.op.args[app.terms.size]!
-      some (tp, next, { sofar, pending })
-
-/- `push s next v` adds the result of `next.push v` to the state. -/
-def push (s : Gen term) (next : PartialTerm term) (v : term) : Gen term :=
-  let { sofar, pending } := s
-  match next.push v with
-  | .inl v => { sofar := sofar.push v, pending }
-  | .inr next => { sofar, pending := pending.push next }
-
-def pushOp (s : Gen term) (ctx : GenCtx term) (next : PartialTerm term) (op : Op Nat term) :=
-  if op.args.isEmpty then
-    s.push next (op.apply #[])
-  else if op.args.size ≤ next.remTermSize ∧ next.termStack.size + 1 < ctx.maxDepth then
-    { s with pending := s.pending.push (next.pushOp op) }
-  else
-    s
-
-def add (s : Gen term) (val : term ⊕ PartialTerm term) : Gen term :=
-  let { sofar, pending } := s
-  match val with
-  | .inl v => { sofar := sofar.push v, pending }
-  | .inr p => { sofar, pending := pending.push p }
-
-/-- Create state that will explore all terms in context -/
-def addOpInstances (s : Gen term) (ctx : GenCtx term) (op : Op Nat term) : Gen term :=
-  s.add (PartialTerm.init ctx.maxTermSize ctx.maxDepth op)
-
-/-- Create state that will explore all terms in context -/
-def init (ctx : GenCtx term) : Gen term :=
-  ctx.topOps.foldl (init := {}) (·.addOpInstances ctx ·)
-
-end Gen
-
-/--
-Generate terms until we reach the limit.
--/
-partial
-def generateTerms
-    (ctx : GenCtx term)
-    (s : Gen term)
-    (limit : Nat := 0) :
-    Array term × Gen term :=
-  if limit > 0 ∧ s.sofar.size ≥ limit then
-    (s.sofar, { s with sofar := #[] })
-  else
-    match s.pop with
-    | none => (s.sofar, { s with sofar := #[] })
-    | some (tp, next, s) =>
-      let addVar (next : PartialTerm term) (i : Nat) (s : Gen term) : Gen term :=
-            if next.usedVars[i]! = tp then
-              match ctx.var tp i with
-              | some v => s.push next v
-              | none => s
-            else
-              s
-      let s := next.usedVars.size.fold (init := s) (addVar next)
-      let s :=
-        let var := next.usedVars.size
-        if var < ctx.maxVarCount then
-          let next := { next with usedVars := next.usedVars.push tp }
-          addVar next var s
-        else
-          s
-      generateTerms ctx (ctx.ops[tp]!.foldl (init := s) (·.pushOp ctx next ·))
+open Lean
+open Lean.Elab.Command (CommandElab)
+open Lean.Test.NormalForms
 
 /-
-`addScopeVariables` extends the local context and instances with a copy of the
-variables in the scope (which must be non-empty).
--/
-def addScopeVariables (lctx : LocalContext) (linst : LocalInstances) (scope : Scope) (idx : Nat) :
-    CoreM (LocalContext × LocalInstances × Ident) := do
-  let act := Term.elabBindersEx scope.varDecls fun vars => do pure (vars, ← (read : MetaM Meta.Context))
-  let mctx := { lctx := lctx, localInstances := linst }
-  let (((vars, mctx), _tstate), _mstate) ← act |>.run |>.run mctx
-  if vars.isEmpty then
-    throwError "No variables declared"
-  let fv := vars[0]!.snd |>.fvarId!
-  let rec drop (nm : Name) :=
-        match nm with
-        | .str .anonymous s => pure (.str .anonymous s!"{s}{idx}")
-        | .str nm _ => drop nm
-        | .num nm _ => drop nm
-        | .anonymous => throwError "Anonymous variable declared."
-  let nm ← drop (mctx.lctx.get! fv |>.userName)
-  let lctx := mctx.lctx.setUserName fv nm
-  pure (lctx, mctx.localInstances, mkIdent nm)
-
-def addVariables (cmdCtx : Command.Context) (cmdState : Command.State) (lctx : LocalContext) (linst : LocalInstances) (n : Nat) (cmd : Command) :
-    CoreM (LocalContext × LocalInstances × Array Ident) := do
-  let (_, s) ←  elabCommand cmd.raw |>.run cmdCtx |>.run cmdState
-  let scope := s.scopes.head!
-  Nat.foldM (n := n) (init := (lctx, linst, .mkEmpty n)) fun i (lctx, linst, a) => do
-    let (lctx, linst, ident) ← addScopeVariables lctx linst scope i
-    pure (lctx, linst, a.push ident)
-
-structure VarDecl (tp : Type) where
-  idx : Nat
-  ident : TSyntax `ident
-  type : tp
-  deriving Inhabited, Repr
-
-instance : BEq (VarDecl tp) where
-  beq x y := x.idx == y.idx
-
-instance : Hashable (VarDecl tp) where
-  hash v := hash v.idx
-
-structure GenStats where
-  maxTermSize : Nat := 9
-  maxDepth : Nat := 3
-  maxVarCount : Nat := 3
-
-def mkCtx [BEq tp] [Hashable tp]
-    (types : Array tp)
-    (ops : List (Op tp val))
-    (varGen : List (tp × CoreM Command))
-    (mkVar : VarDecl tp → val)
-    (stats : GenStats)
-    (topOps : List (Op tp val) := ops) : CommandElabM (GenCtx val) := do
-  let typeMap : HashMap tp Nat := Nat.fold (n := types.size) (init := {}) fun i s =>
-        if p : i < types.size then
-          s.insert types[i] i
-        else
-          s
-  let typeFn (t : tp) := typeMap.findD t 0
-  let addOp (a : Array (Array (Op Nat val))) (op : Op tp val) :=
-        let op := op.map typeFn
-        a.modify op.result (·.push op)
-  let init := Array.ofFn (n := types.size) (fun _ => #[])
-  let ops := ops.foldl (init := init) addOp
-  let ops := ops.map (·.reverse)
-  let topOps := topOps.toArray.map (·.map typeFn)
-  let (lctx, linst, vars) ← liftCoreM do
-    let coreCtx ← read
-    let coreState ← get
-    let fileName := coreCtx.fileName
-    let fileMap  := coreCtx.fileMap
-    let env := coreState.env
-    let maxRecDepth := coreCtx.maxRecDepth
-    let cmdCtx : Command.Context := { fileName, fileMap, tacticCache? := none }
-    let cmdState : Command.State := { env, maxRecDepth }
-    let addVars (p : LocalContext × LocalInstances × Array (Array val))
-                (q : tp × CoreM Command) :
-                CoreM (LocalContext × LocalInstances × _) := do
-          let (lctx, linst, a) := p
-          let (type, gen) := q
-          let cmd ← gen
-          let (lctx, linst, vars) ← addVariables cmdCtx cmdState lctx linst stats.maxVarCount cmd
-          let vars := Array.ofFn (n := vars.size) fun j => mkVar { idx := j.val, ident := vars[j], type }
-          let type := typeFn type
-          pure (lctx, linst, a.modify type (fun _ => vars))
-    let vars := Array.ofFn (n := types.size) fun _ => #[]
-    varGen.foldlM (init := ({}, {}, vars)) addVars
-  let maxTermSize : Nat := stats.maxTermSize
-  let maxDepth : Nat := stats.maxDepth
-  let maxVarCount : Nat := stats.maxVarCount
-  pure { ops, topOps, maxTermSize, maxDepth, maxVarCount, lctx, linst, vars }
-
-def runTests [BEq tp] [HasType val tp] [Value val] (stx : Syntax) (simp : val → val)(tac : Syntax.Tactic) (terms : Array val)
-      : TermElabM Unit := do
-  for tm in terms do
-    if ← IO.checkCanceled then
-      -- should never be visible to users!
-      throw <| Exception.error .missing "Testing interrupted"
-    let res := simp tm
-    let t ← Value.render tm
-    if HasType.typeOf tm != HasType.typeOf res then
-      throwErrorAt stx m!"simp spec for {t} did not preserve type."
-    withoutModifyingEnv $ do
-      let exp ← Value.render res
-      let u ← Lean.Elab.Term.elabTerm t none
-      let type ← inferType u
-      let checkGoalType ← mkCheckGoalType u type
-      let expTerm ← Lean.Elab.Term.elabTerm exp (some type)
-      let mvar ← mkFreshExprMVar (.some checkGoalType)
-      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
-      match goals with
-      | [next] => do
-        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
-        if !(← Meta.withReducible <| isDefEq val expTerm) then
-          logErrorAt stx
-            m!"{indentExpr u} reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
-      | [] =>
-        logErrorAt stx
-          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
-      | _ => do
-        logErrorAt stx
-          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
-
-private def mkCoreContext (ctx : Command.Context) (options : Options) (maxRecDepth : Nat) (initHeartbeats : Nat) : Core.Context :=
-  { fileName       := ctx.fileName
-    fileMap        := ctx.fileMap
-    options,
-    currRecDepth   := ctx.currRecDepth
-    maxRecDepth,
-    ref            := ctx.ref
-    initHeartbeats,
-    currMacroScope := ctx.currMacroScope }
-
-/-- Runs term elaborator in base context. -/
-def runTermElabM (cctx : Core.Context) (cstate : Core.State) (mctx : Meta.Context) (act : TermElabM Unit)
-    : BaseIO (Except Exception MessageLog) := do
-  let r ← act.run |>.run mctx |>.run cctx cstate |>.toBaseIO
-  match r with
-  | .error e =>
-    pure (.error e)
-  | .ok ((((), _termS), _metaS), coreS) =>
-    pure (.ok coreS.messages)
-
-partial
-def runGen [BEq tp] [Hashable tp] [HasType term tp] [Value term]
-
-      (stx : Syntax) (simp : term → term)
-      (varGen : List (tp × CoreM Command))
-      (mkVar : VarDecl tp → term)
-      (stats : GenStats)
-      (types : Array tp)
-      (ops : List (Op tp term))
-      (tac : Syntax.Tactic)
-      (topOps : List (Op tp term) := ops)
-      (concurrent : Bool := true) : CommandElabM Unit := do
-
-  let ctx ← mkCtx (types := types) (ops := ops) (topOps := topOps) (varGen := varGen) (mkVar := mkVar) (stats := stats)
-
-  let lctx := ctx.lctx
-  let linst := ctx.linst
-
-  let cmdCtx : Command.Context ← read
-  let s ← get
-  let ngen := s.ngen
-  let env := s.env
-  let maxRecDepth := s.maxRecDepth
-  let heartbeats ← IO.getNumHeartbeats
-  let options ← getOptions
-  let cctx := mkCoreContext cmdCtx options maxRecDepth heartbeats
-  let cstate : Core.State := { env := env, ngen := ngen, infoState.enabled := false }
-  let mctx : Meta.Context := { lctx := lctx, localInstances := linst }
-  let gen := Gen.init ctx
-  if concurrent then
-    let limit := 400
-    let rec loop (gen : Gen term) (tasks : Array (Task (Except Exception MessageLog))) := do
-      if gen.isEmpty then
-        return tasks
-      else
-        IO.println s!"Writing task"
-        let (terms, gen) := generateTerms ctx gen (limit := limit)
-        let t ← runTests stx simp tac terms |> runTermElabM cctx cstate mctx |>.asTask
-        loop gen (tasks.push t)
-    let tasks ←
-      profileitM Exception "simptest.launch" ({} : Options) (decl := .anonymous) do
-        loop gen #[]
-
-    profileitM Exception "simptest.execute" {} do
-      for i in [0:tasks.size] do
-        if ← IO.checkCanceled then
-          break
-        let act := tasks[i]!
-        match act.get with
-        | .error e =>
-          -- Cancel all tasks after this one
-          (tasks |>.toSubarray (start := i+1) |>.forM IO.cancel : BaseIO Unit)
-          throw e
-        | .ok m =>
-          modify fun s => { s with messages := s.messages ++ m }
-  else
-    let r ← runTermElabM cctx cstate mctx <|
-      let (terms, _) := generateTerms ctx gen
-      runTests stx simp tac terms
-    match r with
-    | .error e => throw e
-    | .ok m => modify fun s => { s with messages := s.messages ++ m }
-
-/-
-
 This file runs many tests on simp and other operations on Boolean/Prop
 values.
 
@@ -596,7 +167,6 @@ def map (f : BoolVal -> BoolVal) (v : BoolVal) : BoolVal :=
   | .ne x y op => .ne (f x) (f y) op
   | .ite c x y op => .ite (f c) (f x) (f y) op
 
-
 def trueProp  : BoolVal := .trueVal .prop
 def falseProp : BoolVal := .falseVal .prop
 def trueBool  : BoolVal := .trueVal .bool
@@ -639,7 +209,6 @@ def coerceType (v : BoolVal) (type : BoolType) : BoolVal :=
   | .bool, .prop => eq_true v
   | _, _ => v
 
-
 /--
 Returns true if we should consider `x` a complement of `y`.
 
@@ -655,7 +224,6 @@ def isComplement (x y : BoolVal) : Bool :=
   | eq_false x, eq_true y => x == y
   | _, _ => false
 
-
 def resolveEq (thunks : List (term → term → Option term)) (x y : term) : Option term :=
   match thunks with
   | [] => none
@@ -679,6 +247,14 @@ def isOrComplement (x y : BoolVal) (tp : BoolType) : Bool :=
   | eq_false x, eq_true y, _ => x == y
   | _, _, _ => false
 
+namespace BoolVal
+
+open BoolType
+
+variable (tp : BoolType)
+
+end BoolVal
+
 partial def simp (v : BoolVal) : BoolVal :=
   let v := map simp v
   match v with
@@ -687,8 +263,6 @@ partial def simp (v : BoolVal) : BoolVal :=
       match p with
       | .trueVal  _ => .trueVal  .bool
       | .falseVal _ => .falseVal .bool
-      | .var _ => v
-      | .boolToProp _ => panic! "Expected boolToProp to simplify away"
       | .not x _   => simp <| ~(.decide x)
       | .and x y _ => simp <| (.decide x) &&& (.decide y)
       | .or x y _  => simp <| (.decide x) ||| (.decide y)
@@ -708,6 +282,8 @@ partial def simp (v : BoolVal) : BoolVal :=
         match op with
         | .iteProp => simp <| .ite c (.decide t) (.decide f) .iteBool
         | _ => v
+      | .var _ => v
+      | .boolToProp _ => panic! "Expected boolToProp to simplify away"
       | .decide _ | .eq _ _ _ =>
         panic! s!"Unexpected prop {repr p} when bool expected."
   | .not t _ =>
@@ -780,7 +356,6 @@ partial def simp (v : BoolVal) : BoolVal :=
     | .falseVal _, _ => .trueVal .prop
     | _, .trueVal _ => y
     | _, .falseVal _ => simp <| .not x .prop
-    | .and a b _, y => simp <| .implies a (.implies b y)
     | x, y => Id.run <| do
       if x == y then
         return (.trueVal .prop)
@@ -798,7 +373,8 @@ partial def simp (v : BoolVal) : BoolVal :=
       if let .not yn _ := y then
         if x == yn then
           return y
-
+      if let .and a b _ := x then
+        return simp <| .implies a <| .implies b y
       return v
   | .eq (.trueVal _) y op =>
     match y with
@@ -1035,11 +611,10 @@ set_option profiler false
 
 end BoolVal
 
-instance : HasType BoolVal BoolType where
-  typeOf val := val.typeOf
-
-instance : Value BoolVal where
-  render val := val.render
+def vars : List (BoolType × CoreM Command) := [
+    (.bool, `(variable (b : Bool))),
+    (.prop, `(variable (p : Prop) [Decidable p]))
+  ]
 
 section
 open BoolVal BoolType
@@ -1047,29 +622,27 @@ open BoolVal BoolType
 def trueOp  (tp : BoolType) := mkOp [] tp fun _ => trueVal  tp
 def falseOp (tp : BoolType) := mkOp [] tp fun _ => falseVal tp
 def boolToPropOp := mkOp [.bool] prop fun a => boolToProp (a[0]!)
-def propToBoolOp := mkOp [prop] bool fun a => BoolVal.decide (a[0]!)
-
+def propToBoolOp := mkOp [prop] .bool fun a => BoolVal.decide (a[0]!)
 def notOp (tp : BoolType) := mkOp [tp] tp fun a => not (a[0]!) tp
 def andOp (tp : BoolType) := mkOp [tp, tp] tp fun a => and (a[0]!) (a[1]!) tp
 def orOp  (tp : BoolType) := mkOp [tp, tp] tp fun a => or  (a[0]!) (a[1]!) tp
 def impliesOp := mkOp [.prop, .prop] prop fun a => implies  (a[0]!) (a[1]!)
-def eqOp  (op : EqOp)  :=
-  mkOp [op.argType, op.argType] op.resultType fun a => eq (a[0]!) (a[1]!) op
-def neOp  (op : NeOp)  :=
-  mkOp [op.argType, op.argType] op.resultType fun a => ne (a[0]!) (a[1]!) op
+def eqOp (op : EqOp) := mkOp [op.argType, op.argType] op.resultType fun a => eq (a[0]!) (a[1]!) op
+def neOp (op : NeOp) := mkOp [op.argType, op.argType] op.resultType fun a => ne (a[0]!) (a[1]!) op
 def iteOp (op : IteOp) :=
   let rtp := op.resultType
   mkOp [op.condType, rtp, rtp] rtp fun a => ite (a[0]!) (a[1]!) (a[2]!) op
 
 end
 
-def mkBoolDecl : CoreM Command := `(variable (b : Bool))
-def mkDecidablePropDecl : CoreM Command := `(variable (p : Prop) [Decidable p])
+instance : GenTerm BoolVal BoolType where
+  mkVar := BoolVal.var
+  render := BoolVal.render
 
 syntax:lead (name := boolTestElab) "#boolTest" : command
 
 @[command_elab boolTestElab]
-def elabGenTest : CommandElab := fun stx => do
+def elabBoolTest : CommandElab := fun _stx => do
   let baseOps := [
       trueOp  .bool,  trueOp .prop,
       falseOp .bool, falseOp .prop,
@@ -1086,15 +659,13 @@ def elabGenTest : CommandElab := fun stx => do
     --iteOp .diteProp,  iteOp .diteBool,
     iteOp .condBool
   ]
-  let types := #[.prop, .bool]
+  let types := [.prop, .bool]
   let ops := baseOps ++ eqOps ++ neOps ++ iteOps
-  let varGen : List (BoolType × CoreM Command) := [
-      (.bool, mkBoolDecl),
-      (.prop, mkDecidablePropDecl)
-  ]
   let stats : GenStats := { maxTermSize := 7, maxDepth := 3, maxVarCount := 2 }
-  let tac : Syntax.Tactic ← `(tactic|try simp)
-  runGen stx BoolVal.simp varGen BoolVal.var stats types ops (topOps := ops) tac
+  testNormalForms types ops vars BoolVal.simp stats
 
 set_option maxHeartbeats 10000000
+--set_option profiler true
+--set_option profiler.threshold 1
+set_option trace.Test.normalforms true
 #boolTest

tests/playground/int_exhaust_test.lean

@@ -0,0 +1,657 @@
+import Lean.Util.TestNormalForms
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs
+import Lean.Meta.LitValues
+
+open Lean
+open Lean.Elab.Command (CommandElab)
+open Lean.Test.NormalForms
+
+namespace Nat
+
+attribute [simp] mod_one
+attribute [simp] Nat.mul_div_cancel
+attribute [simp] Nat.mul_div_cancel_left
+
+theorem succ_mod (a b : Nat) : (a + 1) % b = if a % b + 1 = b then 0 else (a % b) + 1 := by
+  match b with
+  | 0 =>
+    simp
+  | 1 =>
+    simp
+  | b + 2 =>
+    simp only [Nat.succ.injEq]
+    split <;> rename_i dp
+    · rw [Nat.add_mod a 1 _]
+      simp [dp]
+    · have one_lt : 1 < b + 2 := Nat.le_add_left ..
+      have q : a % (b + 2) ≤ b + 1 := Nat.le_of_succ_le_succ (Nat.mod_lt _ (by omega))
+      have a_lt : a % (b + 2) + 1 < b + 2 := Nat.succ_lt_succ (Nat.lt_of_le_of_ne q dp)
+      rw [Nat.add_mod a 1 _, Nat.mod_eq_of_lt one_lt, Nat.mod_eq_of_lt a_lt]
+
+theorem le_div_iff_mul_le' (hb : 0 < b) : a ≤ c / b ↔ a * b ≤ c := le_div_iff_mul_le hb
+
+protected theorem div_le_div_right {a b : Nat} (h : a ≤ b) (c : Nat) : a / c ≤ b / c :=
+  (c.eq_zero_or_pos.elim fun hc => by simp [hc]) fun hc ↦
+    (le_div_iff_mul_le' hc).2 <| Nat.le_trans (Nat.div_mul_le_self _ _) h
+
+theorem sub_div_dvd (a : Nat) {b c : Nat} (h : c ∣ b) : (a - b) / c = a / c - b / c := by
+  let ⟨d, p⟩ := h
+  match c with
+  | 0 =>
+    simp
+  | c + 1 =>
+    have sd := Nat.sub_mul_div a (c+1) d
+    if le : (c + 1) * d ≤ a then
+      simp [p, sd le, Nat.mul_comm c d, Nat.mul_div_cancel]
+    else
+      have q := Nat.le_of_not_le le
+      have r := Nat.div_le_of_le_mul q
+      simp [p, Nat.sub_eq_zero_of_le, q, r]
+
+@[simp] theorem sub_div_self (a b : Nat) : (a - b) / b = a / b - 1 := by
+  match b with
+  | 0 => simp
+  | b + 1 => simp [sub_div_dvd, Nat.zero_lt_succ, Nat.div_self]
+
+theorem div_eq_to_mul (a b c : Nat) (h : b > 0) : a / b = c ↔ a = b * c + a % b := by
+  apply Iff.intro
+  · intro p
+    simp [←p]
+    exact (div_add_mod a b).symm
+  · intro p
+    conv at p => lhs; rw [← div_add_mod a b]
+    replace p := Nat.add_right_cancel p
+    replace p := Nat.mul_left_cancel h p
+    exact p
+
+theorem eq_sub_iff (a : Nat) {b c : Nat} (p : b ≥ c) : (a = b - c) ↔ (a + c = b) := by
+  rw [@Eq.comm _ a, Nat.sub_eq_iff_eq_add p, @Eq.comm _ b]
+
+theorem mul_div_self (a b : Nat) : b * (a / b) = a - a % b := by
+  conv => rhs; lhs; rw [← Nat.div_add_mod a b]
+  simp
+
+end Nat
+
+namespace Int
+
+section
+open Lean.Meta Simp
+
+def reduceBinIntNatOp (name : Name) (op : Int → Nat → Int) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity name 2 do return .continue
+  let some v₁ ← getIntValue? e.appFn!.appArg! | return .continue
+  let some v₂ ← getNatValue? e.appArg! | return .continue
+  return .done <| toExpr (op v₁ v₂)
+
+dsimproc [simp, seval] reduceTDiv (Int.div _ _) := reduceBin ``Int.div 2 Int.div
+dsimproc [simp, seval] reduceTMod (Int.mod _ _) := reduceBin ``Int.mod 2 Int.mod
+dsimproc [simp, seval] reduceFDiv (Int.fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
+dsimproc [simp, seval] reduceFMod (Int.fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
+dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv
+dsimproc [simp, seval] reduceBmod (bmod _ _) := reduceBinIntNatOp ``bmod bmod
+
+end
+
+protected theorem sub_lt_iff (a b c : Int) : a - b < c ↔ a < b + c :=
+  Iff.intro Int.lt_add_of_sub_left_lt Int.sub_left_lt_of_lt_add
+
+protected theorem add_lt_iff (a b c : Int) : a + b < c ↔ a < -b + c := by
+  apply Iff.intro
+  · intro p
+    apply @Int.lt_of_add_lt_add_left b
+    simp [Int.add_comm b a, Int.add_neg_cancel_left, p]
+  · intro p
+    apply @Int.lt_of_add_lt_add_left (-b)
+    simp [Int.add_comm (-b) (a + b), Int.add_neg_cancel_right, Int.add_comm c (-b), p]
+
+attribute [simp] Int.dvd_neg
+attribute [simp] Int.dvd_refl
+attribute [simp] Int.dvd_natAbs
+
+@[simp]theorem dvd_mod_self (a b : Int) : (a ∣ b % a) ↔ a ∣ b := by
+  have p : a ∣ -(a * (b / a)) := by
+    simp [Int.dvd_neg, Int.dvd_mul_right]
+  simp [Int.emod_def, Int.sub_eq_add_neg, Int.dvd_add_left p]
+
+attribute [simp] emod_self
+
+theorem add_ofNat_ofNat (m n : Nat) : (m : Int) + (n : Int) = (m + n : Nat) := rfl
+theorem add_ofNat_negSucc (m n : Nat) : m + -[n+1] = subNatNat m (n + 1) := rfl
+theorem add_negSucc_ofNat (m n : Nat) : -[m+1] + n = subNatNat n (m + 1) := rfl
+theorem add_negSucc_negSucc (m n : Nat) : -[m+1] + -[n+1] = -[m + n + 1 +1] := rfl
+
+theorem ediv_ofNat_ofNat (m n : Nat) : (m : Int) / (n : Int) = (m / n : Nat) := rfl
+
+--set_option trace.Meta.Tactic.simp.rewrite true
+
+/-
+@[simp] theorem add_ediv_right (a : Int) {b : Int} (h : b ≠ 0) : (a + b) / b = (a / b) + 1 := by
+  match a, b with
+  | .ofNat a, .ofNat b => admit
+  | .ofNat a, -[b +1] => admit
+  | _, 0 => simp at h
+  | -[a+1], .ofNat (b + 1) =>
+    simp [-Int.natCast_add, add_negSucc_ofNat, subNatNat, ediv_negSucc_succ,
+          Int.neg_add_cancel_right]
+    split;
+    · simp only [Int.ediv_ofNat_ofNat]
+      --natCast_add] -- [ediv_ofNat_ofNat];
+      admit
+    · admit
+  | -[a+1], -[b+1] => simp [ediv_negSucc_negSucc]; admit
+-/
+
+/-
+  | ofNat m, ofNat n => ofNat (m / n)
+  | ofNat m, -[n+1]  => -ofNat (m / succ n)
+  | -[_+1],  0       => 0
+  | -[m+1],  ofNat (succ n) => -[m / succ n +1]
+  | -[m+1],  -[n+1]  => ofNat (succ (m / succ n))
+-/
+
+
+
+/-
+@[simp] theorem add_ediv_left (a : Int) {b : Int} (h : b ≠ 0) : (b + a) / b = (a / b) + 1 := by
+  rw [Int.add_comm, add_ediv_right a h]
+-/
+
+theorem emod_neg_iff (m n : Int) : m % n < 0 ↔ (m < 0 ∧ n = 0) := by
+  change Int.emod m n < 0 ↔ (m < 0 ∧ n = 0)
+  match m with
+  | ofNat m =>
+    have not_lt_zero (n : Nat) : ¬((n : Int) < 0) := by
+      apply (Int.ofNat_not_neg _).mp
+      -- (Int.ofNat_zero_le _)
+    simp [-ofNat_emod, Int.emod, not_lt_zero]
+  | -[m+1] =>
+    simp [-ofNat_emod, -Int.natCast_add, Int.emod, Int.subNatNat_eq_coe, negSucc_lt_zero,
+          Int.sub_lt_iff]
+    apply Iff.intro
+    · intro p
+      replace p := Nat.le_of_succ_le_succ p
+      if nz : n = 0 then
+        exact nz
+      else
+        have q : n.natAbs > 0 := Int.natAbs_pos.mpr nz
+        have r : m % n.natAbs < n.natAbs := Nat.mod_lt _ q
+        exact False.elim (Nat.not_le_of_gt r p)
+    · intro p
+      simp [p]
+
+theorem emod_sub_natAbs_self (m n : Int) : (m - n.natAbs) % n = m % n := by
+  simp [Int.sub_eq_add_neg, add_emod_of_dvd]
+
+theorem emod_lt (a b : Int) (h : b ≠ 0) : a % b < Int.natAbs b := by
+  rw [emod_as_nat_mod]
+  if p : a ≥ 0 then
+    simp [p, -Int.ofNat_emod]
+    exact Nat.mod_lt _ (by omega)
+  else
+    simp [p, -Int.ofNat_emod]
+    apply Int.sub_lt_self
+    apply Int.succ_ofNat_pos
+
+@[simp] theorem sub_emod_self_left (n y : Int) : (n - y) % n = (-y) % n := by
+  simp [Int.sub_eq_add_neg]
+
+theorem div_eq_ediv' (a b : Int) : Int.div a b = a / b + ite (a < 0 ∧ ¬(b ∣ a)) (sign b) 0  :=
+  match a, b with
+  | (a : Nat), ofNat b => rfl
+  | (a : Nat), -[b +1] => by
+    simp [Int.div, ediv_ofNat_negSucc, ofNat_not_neg]
+  | -[a +1], 0 => by
+    simp [Int.div, ediv_negSucc_zero]
+  | -[a +1], (b+1 : Nat) => by
+    have q : ¬(Nat.cast ((b + 1) : Nat) = (0 : Int)) := by
+      norm_cast
+    simp [-Int.natCast_add] at q
+    simp [Int.div, ediv_negSucc_succ, Nat.succ_div,
+          Int.negSucc_lt_zero, q, true_and,
+          -Int.natCast_add]
+    split <;> rename_i pg
+    · simp [Int.neg_add]
+    · simp [Int.neg_add, Int.neg_add_cancel_right]
+  | -[m +1], -[n +1] => by
+    simp [Int.div, ediv_negSucc_negSucc,
+      Int.negSucc_lt_zero,
+      -ofNat_ediv, -natCast_add,
+      Nat.succ_div]
+    split <;> rename_i h
+    . simp
+    · simp [Int.add_neg_cancel_right]
+
+theorem mod_eq_emod' (a b : Int) : Int.mod a b = a % b - b * ite (a < 0 ∧ ¬(b ∣ a)) (sign b) 0 := by
+  simp [emod_def, mod_def, div_eq_ediv',
+        Int.mul_add, Int.sub_eq_add_neg, Int.neg_add, Int.add_assoc]
+
+
+@[simp] theorem emod_mod (a b : Int) : (mod a b) % b = a % b := by
+  simp [Int.mod_eq_emod', Int.sub_eq_add_neg, Int.neg_mul_eq_mul_neg]
+
+@[simp] theorem mod_emod (m n : Int) : Int.mod (m % n) n = m % n := by
+  simp_all [mod_eq_emod', emod_neg_iff]
+
+@[simp] theorem mod_mod (m n : Int) : Int.mod (Int.mod m n) n = Int.mod m n := by
+  simp only [mod_eq_emod' m n]
+  split
+  · rename_i mnn
+    rw [mod_eq_emod']
+    by_cases q : OfNat.ofNat 0 < natAbs n <;>
+    simp_all [Int.sub_eq_add_neg, Int.mul_sign, add_emod_of_dvd, Int.add_lt_iff,
+              Int.natAbs_pos, Int.emod_lt, Int.dvd_add_left]
+  · simp [mod_emod]
+
+@[simp] theorem emod_fmod (a b : Int) : (fmod a b) % b = a % b := by
+  simp [Int.fmod_eq_emod', Int.sub_eq_add_neg, Int.neg_mul_eq_mul_neg]
+
+@[simp] theorem fmod_emod (m n : Int) : Int.fmod (m % n) n = Int.fmod m n := by
+  simp_all [fmod_eq_emod', emod_neg_iff]
+
+@[simp]
+theorem fmod_fmod (m n : Int) : Int.fmod (Int.fmod m n) n = Int.fmod m n := by
+  simp [fmod_eq_emod', Int.sub_eq_add_neg, Int.neg_mul_eq_mul_neg,
+        Int.dvd_add_left, Int.dvd_mul_right]
+
+--@[simp] theorem zero_bdiv : bdiv 0 n = 0 := by sorry
+
+--@[simp] theorem bdiv_one : bdiv m 1 = 0 := by sorry
+
+@[simp] theorem zero_bdiv (n : Nat) : bdiv 0 n = 0 := by
+  unfold bdiv; simp; omega
+@[simp] theorem bdiv_zero  (n : Int) : bdiv n 0 = 0 := by rfl
+
+@[simp] theorem bdiv_one   (n : Int) : bdiv n 1 = n := by unfold bdiv; simp
+
+@[simp] theorem bmod_zero (n : Int) : bmod n 0 = n := by unfold bmod; simp
+
+end Int
+
+inductive NumType where
+| nat
+| int
+deriving DecidableEq, Hashable, Inhabited, Repr
+
+protected def NumType.render [Monad M] [MonadQuotation M] (v : NumType) : M Term := do
+  match v with
+  | nat => `(Nat)
+  | int => `(Int)
+
+inductive  DivMode where
+  | divNat
+  | edivInt
+  | tdivInt
+  | fdivInt
+  | bdivInt
+  deriving DecidableEq, Repr
+
+def DivMode.typeOf (m : DivMode) : NumType :=
+  match m with
+  | divNat => .nat
+  | edivInt => .int
+  | fdivInt => .int
+  | tdivInt => .int
+  | bdivInt => .int
+
+inductive NumTerm where
+  | var (d : VarDecl NumType)
+  | lit (n : Nat) (tp : NumType)
+  | natToInt (x : NumTerm)
+  | intToNat (x : NumTerm)
+  | add (x y : NumTerm) (tp : NumType)
+  | sub (x y : NumTerm) (tp : NumType)
+  | neg (x : NumTerm)
+  | mul (x y : NumTerm) (tp : NumType)
+  | div (x y : NumTerm) (m : DivMode)
+  | mod (x y : NumTerm) (m : DivMode)
+  deriving BEq, Inhabited, Repr
+
+namespace NumTerm
+
+open NumType
+
+partial def map (f : NumTerm → NumTerm) (v : NumTerm) : NumTerm :=
+  match v with
+  | var _ | lit _ _ => v
+  | natToInt x => natToInt (f x)
+  | intToNat x => intToNat (f x)
+  | add x y tp => add (f x) (f y) tp
+  | sub x y tp => sub (f x) (f y) tp
+  | neg x => neg (f x)
+  | mul x y tp => mul (f x) (f y) tp
+  | div x y op => div (f x) (f y) op
+  | mod x y op => mod (f x) (f y) op
+
+protected def typeOf (v : NumTerm) : NumType :=
+  match v with
+  | var d => d.type
+  | lit _ tp => tp
+  | natToInt _ => .int
+  | intToNat _ => .nat
+  | add _ _ tp => tp
+  | sub _ _ tp => tp
+  | neg _ => .int
+  | mul _ _ tp => tp
+  | div _ _ op => op.typeOf
+  | mod _ _ op => op.typeOf
+
+protected def render [Monad M] [MonadQuotation M] (v : NumTerm) : M Term := do
+  match v with
+  | var d => pure d.ident
+  | lit n tp => `(($(Syntax.mkNumLit (toString n)) : $(←tp.render)))
+  | natToInt x => `((($(←x.render) : Nat) : Int))
+  | intToNat x => `((($(←x.render) : Int) : Nat))
+  | add x y tp => `((($(←x.render) + $(←y.render)) : $(←tp.render)))
+  | sub x y _ => `($(←x.render) - $(←y.render))
+  | neg x => `(- $(←x.render))
+  | mul x y _ => `($(←x.render) * $(←y.render))
+  | div x y op =>
+    match op with
+    | .divNat  => `($(←x.render) / $(←y.render))
+    | .edivInt => `($(←x.render) / $(←y.render))
+    | .fdivInt => `(Int.fdiv $(←x.render) $(←y.render))
+    | .tdivInt => `(Int.div  $(←x.render) $(←y.render))
+    | .bdivInt => `(Int.bdiv $(←x.render) $(←y.render))
+  | mod x y op =>
+    match op with
+    | .divNat  => `($(←x.render) % $(←y.render))
+    | .edivInt => `($(←x.render) % $(←y.render))
+    | .fdivInt => `(Int.fmod $(←x.render) $(←y.render))
+    | .tdivInt => `(Int.mod  $(←x.render) $(←y.render))
+    | .bdivInt => `(Int.bmod $(←x.render) $(←y.render))
+
+instance : GenTerm NumTerm NumType where
+  render := NumTerm.render
+  mkVar := NumTerm.var
+
+def intLit (i : Int) : NumTerm :=
+  if i < 0 then
+    neg (lit ((- i).toNat) .int)
+  else
+    lit i.toNat .int
+
+def mkLit (i : Int) (tp : NumType) : NumTerm :=
+  if i < 0 then
+    match tp with
+    | .nat => panic! "Negative number passed into nat"
+    | .int => neg (lit ((- i).toNat) .int)
+  else
+    lit i.toNat tp
+
+def asIntLit (i : NumTerm) : Option Int :=
+  match i with
+  | .lit n _ => some (n : Int)
+  | .neg (.lit n .int) => some (- (n : Int))
+  | _ => none
+
+
+/-
+
+  1 + i0 - i0 reduces to
+  1
+but is expected to reduce to
+  1 + i0 - i0
+
+
+  i0 - i1 + i1 reduces to
+  i0
+but is expected to reduce to
+  i0 - i1 + i1
+  -/
+partial def simp (v : NumTerm) : NumTerm :=
+  let v := map simp v
+  match v with
+  | natToInt x =>
+    (match x with
+    | lit n _ => lit n .int
+    | add x y _ => add (natToInt x) (natToInt y) .int
+    | mul x y _ => mul (natToInt x) (natToInt y) .int
+    | div x y _ => div (natToInt x) (natToInt y) .edivInt
+    | mod x y _ => mod (natToInt x) (natToInt y) .edivInt
+    | var _ | sub _ _ _ | neg _ | intToNat _ | natToInt _ => v)
+  | add x y tp =>
+    match x, y with
+    | x, lit 0 _ => x
+    | lit 0 _, y => y
+    | _, _ => Id.run <| do
+      if let .sub xa xb _ := x then
+        if tp = .int ∧ xb == y then
+          return xa
+      if let (some i, some j) := (asIntLit x, asIntLit y) then
+        return (mkLit (i+j) tp)
+      pure v
+  | sub x y tp =>
+    match x, y, tp with
+    | x, lit 0 _, _ => x
+    | lit 0 _, _, .nat => lit 0 .nat
+    | lit 0 _, y, .int => simp (neg y)
+    | x, y, _ => Id.run <| do
+      match tp with
+      | .nat =>
+        if let (lit i _, lit j _) := (x, y) then
+          return lit (i-j) .nat
+      | .int =>
+        if let (some i, some j) := (asIntLit x, asIntLit y) then
+          return mkLit (i - j) .int
+      if let .add xa xb _ := x then
+        if xb == y then
+          return xa
+      if x == y then
+        return .lit 0 tp
+      pure v
+  | neg x =>
+    match x with
+    | lit n _ => intLit (- (Int.ofNat n))
+    | neg x => x
+    | _ => v
+  | mul x y tp =>
+    match x, y with
+    | _, lit 0 _ => y
+    | lit 0 _, _ => x
+    | _, lit 1 _ => x
+    | lit 1 _, _ => y
+    | lit i _, lit j _ => lit (i*j) tp
+    | _, _ => Id.run <| do
+      if let (some i, some j) := (asIntLit x, asIntLit y) then
+        return (mkLit (i * j) tp)
+      pure v
+  | div x y op =>
+    if let (some x, some y) := (asIntLit x, asIntLit y) then
+      match op with
+      | .divNat => lit (Nat.div x.toNat y.toNat) .nat
+      | .edivInt => intLit (Int.ediv x y)
+      | .fdivInt => intLit (Int.fdiv x y)
+      | .tdivInt => intLit (Int.div  x y)
+      | .bdivInt => intLit (Int.bdiv x y.toNat)
+    else if let lit 0 _ := x then
+      x
+    else if let lit 0 _ := y then
+      lit 0 op.typeOf
+    else if let lit 1 _ := y then
+      x
+    else Id.run <| do
+      if let add xa xb _tp := x then
+        if let .lit i _ := y then
+          if op ∈ [.divNat] ∧ i ≠ 0 then
+            if xa == y then
+              return simp (.add (.div xb y op) (.lit 1 op.typeOf) op.typeOf)
+            else if xb == y then
+              return simp (.add (.div xa y op) (.lit 1 op.typeOf) op.typeOf)
+      if let sub xa xb _tp := x then
+          if op = .divNat ∧ xb == y then
+            return simp (.sub (.div xa y op) (.lit 1 op.typeOf) op.typeOf)
+      if let mod _ n mOp := x then
+        if op = .divNat ∧ mOp = .divNat ∧ n == y then
+          return .lit 0 .nat
+      if let neg xn := x then
+        match op with
+        | .tdivInt =>
+          return simp (neg (div xn y op))
+        | _ =>
+          pure ()
+      if let neg yn := y then
+        match op with
+        | .edivInt | .tdivInt =>
+          return simp (neg (div x yn op))
+        | _ =>
+          pure ()
+      if let mul xa xb _ := x then
+       if let .lit i _ := y then
+          if i ≠ 0 then
+            if xa == y then
+              return xb
+            if xb == y then
+              return xa
+      pure v
+  | mod x n op =>
+    if let (some x, some n) := (asIntLit x, asIntLit n) then
+      match op with
+      | .divNat => lit (Nat.mod x.toNat n.toNat) .nat
+      | .edivInt => intLit (Int.emod x n)
+      | .fdivInt => intLit (Int.fmod x n)
+      | .tdivInt => intLit (Int.mod  x n)
+      | .bdivInt => intLit (Int.bmod x n.toNat)
+    else if let lit 0 _ := x then
+      x
+    else if let lit 0 _ := n then
+      x
+    else if let lit 1 _ := n then
+      lit 0 op.typeOf
+    else if x == n then
+      lit 0 op.typeOf
+    else Id.run do
+      if let add xa xb _tp := x then
+        if op ∈ [.divNat, .edivInt] then
+          if xa == n then
+            return simp (.mod xb n op)
+          else if xb == n then
+            return simp (.mod xa n op)
+          if let mul xba xbb _tp := xb then
+            if xba == n || xbb == n then
+              return simp (.mod xa n op)
+      if let sub xa xb _tp := x then
+        if op ∈ [.edivInt] then
+          if xa == n then
+            return simp (.mod (.neg xb) n op)
+          else if xb == n then
+            return simp (.mod xa n op)
+          if let mul xba xbb _tp := xb then
+            if xba == n || xbb == n then
+              return simp (.mod xa n op)
+      if let mul xa xb tp := x then
+        if xa == n || xb == n then
+          return lit 0 tp
+      if let mod xn xd xop := x then
+        if xd == n then
+          let rop :=
+            match op, xop with
+            | .divNat, .divNat => some .divNat
+            | .edivInt, _ => some .edivInt
+            | .tdivInt, .edivInt => some .edivInt
+            | .tdivInt, .tdivInt => some .tdivInt
+            | .fdivInt, .edivInt => some .fdivInt
+            | .fdivInt, .fdivInt => some .fdivInt
+            | .bdivInt, _ => some .bdivInt
+            | _, _ => none
+          if let some rop := rop then
+            return simp (mod xn n rop)
+      if let neg yn := n then
+        match op with
+        | .edivInt | .tdivInt | .bdivInt =>
+          return simp (mod x yn op)
+        | _ =>
+          pure ()
+      return v
+  | _ => v
+
+partial def simpv (u : NumTerm) : NumTerm :=
+  let v := simp u
+  if v.typeOf == u.typeOf then
+    v
+  else
+    panic! s!"simp result changed types:\n  Input: {repr u}\n  Out:   {repr v}"
+
+def litOp (n : Nat) (tp : NumType) := mkOp [] tp fun _ => lit n tp
+def addOp (tp : NumType) := mkOp [tp, tp] tp fun a => add (a[0]!) (a[1]!) tp
+def subOp (tp : NumType) := mkOp [tp, tp] tp fun a => sub (a[0]!) (a[1]!) tp
+def negOp : Op NumType NumTerm := mkOp [.int] .int fun a => neg (a[0]!)
+def mulOp (tp : NumType) := mkOp [tp, tp] tp fun a => mul (a[0]!) (a[1]!) tp
+def divOp (op : DivMode) (dtp := op.typeOf) := let tp := op.typeOf; mkOp [tp, dtp] tp fun a => div (a[0]!) (a[1]!) op
+def modOp (op : DivMode) (dtp := op.typeOf) := let tp := op.typeOf; mkOp [tp, dtp] tp fun a => mod (a[0]!) (a[1]!) op
+
+end NumTerm
+
+open NumTerm
+
+syntax:lead (name := intTestElab) "#intTest" : command
+
+@[command_elab intTestElab]
+def elabIntTest : CommandElab := fun _stx => do
+  let types : List NumType := [.nat, .int]
+  let ops := [
+      litOp 0 .nat,
+      litOp 1 .nat,
+      litOp 2 .nat,
+      litOp 0 .int,
+      litOp 1 .int,
+      litOp 2 .int,
+      addOp .nat, addOp .int,
+      subOp .nat, subOp .int,
+      negOp,
+      mulOp .nat, mulOp .int,
+      divOp .divNat, divOp .edivInt, divOp .fdivInt, divOp .tdivInt, divOp .bdivInt .nat,
+      modOp .divNat, modOp .edivInt, modOp .fdivInt, modOp .tdivInt, modOp .bdivInt .nat,
+  ]
+  let vars : List (NumType × CoreM Command) := [
+      (.nat, `(variable (n : Nat))),
+      (.int, `(variable (i : Int)))
+  ]
+  let stats : GenStats := { maxTermSize := 6, maxDepth := 3, maxVarCount := 2 }
+  testNormalForms types ops vars NumTerm.simpv stats
+
+set_option maxHeartbeats 100000000
+--set_option pp.coercions false
+--set_option pp.notation false
+--set_option pp.explicit true
+#intTest
+
+section
+variable (i0 : Int)
+
+set_option trace.Meta.Tactic.simp true
+
+
+end
+namespace Nat
+
+end Nat
+
+namespace Int
+
+open Lean.Meta.CheckTactic (CheckGoalType)
+
+example (b : Int) : div (2 * b) 2 = b := by
+  simp
+  --admit
+
+theorem div_as_nat (x y : Int) : Int.div x y =
+  ite (x ≥ 0) 1 (-1) * ite (y ≥ 0) 1 (-1) * ((x.natAbs) / (y.natAbs)) := by
+  cases x <;> cases y <;>  simp [Int.div, ofNat_nonneg, ←Int.neg_eq_neg_one_mul]
+
+/-
+def emod : (@& Int) → (@& Int) → Int
+  | ofNat m, n => ofNat (m % natAbs n)
+  | -[m+1],  n => subNatNat (natAbs n) (succ (m % natAbs n))
+-/
+
+set_option trace.Meta.Tactic.simp.rewrite true
+
+
+--@[simp] theorem add_mod_self {a b : Int} : Int.mod(a + b)  b = a % b := by
+--  have := add_mul_emod_self_left a b 1; rwa [Int.mul_one] at this
+
+theorem negSucc_in_add (a b : Nat) : -[a + b +1] = -[a+1] - b := by
+  cases b <;> rfl
+
+end Int