wip: progress

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,204 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Mario Carneiro, Joe Hendrix
+-/
+prelude
+import Init.Data.Int.DivModLemmas
+import Init.Data.Nat.Lemmas
+
+/-
+Int div and mod lemmas that omega does not depend on
+-/
+namespace Int
+
+/-! ediv -/
+
+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
+
+/-! emod -/
+
+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
+
+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 =>
+    simp [-ofNat_emod, Int.emod, ofNat_not_neg]
+  | -[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
+      by_cases nz : n = 0
+      · exact nz
+      · 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_lt (a b : Int) (h : b ≠ 0) : a % b < Int.natAbs b := by
+  rw [emod_as_nat_mod]
+  by_cases p : a ≥ 0
+  · simp [p, -Int.ofNat_emod]
+    exact Nat.mod_lt _ (by omega)
+  · 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]
+
+/-! dvd -/
+
+@[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]
+
+/-! div -/
+
+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]
+
+/-! mod -/
+
+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]
+
+
+/-! fdiv -/
+
+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
+
+/-! fmod -/
+
+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]
+
+@[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]
+
+/-! bdiv -/
+
+@[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
+
+/-! bmod -/
+
+@[simp] theorem bmod_zero (n : Int) : bmod n 0 = n := by unfold bmod; simp
+
+
+end Int

src/Init/Data/Int/DivModLemmas.lean

@@ -25,22 +25,25 @@ protected theorem dvd_def (a b : Int) : (a ∣ b) = Exists (fun c => b = a * c)
 
 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⟩
+@[simp] 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])
+  | 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⟩
+
+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
 
 @[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⟩
+  simp [←natAbs_dvd_natAbs]
 
 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]
@@ -51,27 +54,14 @@ theorem dvd_antisymm {a b : Int} (H1 : 0 ≤ a) (H2 : 0 ≤ b) : a ∣ b → b
   Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
             (fun h => h.symm ▸ Int.dvd_refl _)
 
-protected theorem dvd_mul_right (a b : Int) : a ∣ a * b := ⟨_, rfl⟩
+@[simp] protected theorem neg_dvd {a b : Int} : -a ∣ b ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
 
-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
-  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
+@[simp] protected theorem dvd_neg {a b : Int} : a ∣ -b ↔ a ∣ b := 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]⟩
@@ -79,15 +69,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]
@@ -97,26 +91,17 @@ 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]
+@[simp] theorem dvd_natAbs {a b : Int} : a ∣ b.natAbs ↔ a ∣ b := by
+  simp [←natAbs_dvd_natAbs]
 
-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]
+@[simp] theorem natAbs_dvd {a b : Int} : (a.natAbs : Int) ∣ b ↔ 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 dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by
-  rw [Int.dvd_natAbs]
-  exact Int.dvd_refl a
+theorem dvd_natAbs_self {a : Int} : a ∣ (a.natAbs : Int) := by simp
+theorem natAbs_dvd_self {a : Int} : (a.natAbs : Int) ∣ a := by simp
 
 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
@@ -128,6 +113,9 @@ 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
@@ -153,19 +141,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
@@ -194,6 +169,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
@@ -220,67 +208,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)
@@ -305,6 +232,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
@@ -333,21 +264,26 @@ theorem add_mul_ediv_right (a b : Int) {c : Int} (H : c ≠ 0) : (a + b * c) / c
       show ediv (↑(n * succ k) + -((m : Int) + 1)) (succ k) = n + -(↑(m / succ k) + 1 : Int)
       rw [H h, H ((Nat.le_div_iff_mul_le k.succ_pos).2 h)]
       apply congrArg negSucc
-      rw [Nat.mul_comm, Nat.sub_mul_div]; rwa [Nat.mul_comm]
+      rw [Nat.mul_comm, Nat.sub_mul_div]
 
-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
 
@@ -362,10 +298,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
@@ -414,11 +346,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
@@ -440,11 +368,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
 
@@ -489,7 +421,7 @@ theorem mul_emod (a b n : Int) : (a * b) % n = (a % n) * (b % n) % n := by
     Int.mul_assoc, Int.mul_assoc, ← Int.mul_add n _ _, add_mul_emod_self_left,
     ← Int.mul_assoc, add_mul_emod_self]
 
-@[local simp] theorem emod_self {a : Int} : a % a = 0 := by
+@[simp] theorem emod_self {a : Int} : a % a = 0 := by
   have := mul_emod_left 1 a; rwa [Int.one_mul] at this
 
 @[simp] theorem emod_emod_of_dvd (n : Int) {m k : Int}
@@ -498,6 +430,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]
 
@@ -505,14 +442,16 @@ 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)
 
+
+@[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]
+
 /-! ### properties of `/` and `%` -/
 
 theorem mul_ediv_cancel_of_emod_eq_zero {a b : Int} (H : a % b = 0) : b * (a / b) = a := by
@@ -759,6 +698,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
@@ -845,6 +812,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
@@ -852,6 +823,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]
 
@@ -932,6 +908,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 _
@@ -969,8 +975,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]
@@ -999,7 +1010,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]
@@ -1075,7 +1086,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/Lemmas.lean

@@ -23,6 +23,10 @@ theorem subNatNat_of_sub_eq_succ {m n k : Nat} (h : n - m = succ k) : subNatNat
 @[simp] protected theorem neg_zero : -(0:Int) = 0 := rfl
 
 @[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := 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
+
 @[norm_cast] theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
 theorem ofNat_succ (n : Nat) : (succ n : Int) = n + 1 := rfl
 

src/Init/Data/Int/Order.lean

@@ -127,9 +127,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.mpr ⟨(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.mp h).right
+
 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]
@@ -507,9 +512,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
@@ -584,7 +586,10 @@ 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) :=
+  Int.not_lt.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)
@@ -799,6 +804,12 @@ protected theorem lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c
 protected theorem neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c :=
   Int.lt_sub_left_of_add_lt (Int.sub_right_lt_of_lt_add h)
 
+protected theorem add_lt_iff (a b c : Int) : a + b < c ↔ a < -b + c := by
+  rw [← Int.add_lt_add_iff_left (-b), Int.add_comm (-b), Int.add_neg_cancel_right]
+
+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 sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b :=
   Int.sub_left_lt_of_lt_add (Int.lt_add_of_sub_right_lt h)
 

src/Init/Data/Nat/Basic.lean

@@ -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, succ_sub_succ_eq_sub, 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/Div.lean

@@ -162,7 +162,7 @@ theorem mod_le (x y : Nat) : x % y ≤ x := by
 @[simp] theorem mod_self (n : Nat) : n % n = 0 := by
   rw [mod_eq_sub_mod (Nat.le_refl _), Nat.sub_self, zero_mod]
 
-theorem mod_one (x : Nat) : x % 1 = 0 := by
+@[simp] theorem mod_one (x : Nat) : x % 1 = 0 := by
   have h : x % 1 < 1 := mod_lt x (by decide)
   have : (y : Nat) → y < 1 → y = 0 := by
     intro y
@@ -239,10 +239,10 @@ theorem div_mul_le_self : ∀ (m n : Nat), m / n * n ≤ m
 theorem div_lt_iff_lt_mul (Hk : 0 < k) : x / k < y ↔ x < y * k := by
   rw [← Nat.not_le, ← Nat.not_le]; exact not_congr (le_div_iff_mul_le Hk)
 
-@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = succ (x / z) := by
+@[simp] theorem add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = (x / z) + 1 := by
   rw [div_eq_sub_div H (Nat.le_add_left _ _), Nat.add_sub_cancel]
 
-@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = succ (x / z) := by
+@[simp] theorem add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = (x / z) + 1 := by
   rw [Nat.add_comm, add_div_right x H]
 
 theorem add_mul_div_left (x z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z := by
@@ -280,20 +280,38 @@ Nat.le_antisymm
   (le_of_lt_succ ((Nat.div_lt_iff_lt_mul npos).2 hi))
   ((Nat.le_div_iff_mul_le npos).2 lo)
 
-theorem sub_mul_div (x n p : Nat) (h₁ : n*p ≤ x) : (x - n*p) / n = x / n - p := by
+protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
+  | 0, _ => by simp [Nat.div_zero, n.zero_le]
+  | succ k, h => by
+    suffices succ k * (m / succ k) ≤ succ k * n from
+      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
+    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
+    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
+    have h3 : m ≤ succ k * n := h
+    rw [← h2] at h3
+    exact Nat.le_trans h1 h3
+
+theorem sub_mul_div (x n p : Nat) : (x - n * p) / n = x / n - p :=
   match eq_zero_or_pos n with
-  | .inl h₀ => rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
-  | .inr h₀ => induction p with
-    | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
-    | succ p IH =>
-      have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
-      have h₃ : x - n * p ≥ n := by
-        apply Nat.le_of_add_le_add_right
-        rw [Nat.sub_add_cancel h₂, Nat.add_comm]
-        rw [mul_succ] at h₁
-        exact h₁
-      rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
-      simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
+  | .inl h₀ => by
+    rw [h₀, Nat.div_zero, Nat.div_zero, Nat.zero_sub]
+  | .inr h₀ =>
+    if h₁ : n * p ≤ x then by
+      induction p with
+      | zero => rw [Nat.mul_zero, Nat.sub_zero, Nat.sub_zero]
+      | succ p IH =>
+        have h₂ : n * p ≤ x := Nat.le_trans (Nat.mul_le_mul_left _ (le_succ _)) h₁
+        have h₃ : x - n * p ≥ n := by
+          apply Nat.le_of_add_le_add_right
+          rw [Nat.sub_add_cancel h₂, Nat.add_comm]
+          rw [mul_succ] at h₁
+          exact h₁
+        rw [sub_succ, ← IH h₂, div_eq_sub_div h₀ h₃]
+        simp [Nat.pred_succ, mul_succ, Nat.sub_sub]
+    else by
+      replace q := Nat.le_of_not_le h₁
+      have r := Nat.div_le_of_le_mul q
+      simp [Nat.sub_eq_zero_of_le, q, r]
 
 theorem mul_sub_div (x n p : Nat) (h₁ : x < n*p) : (n * p - succ x) / n = p - succ (x / n) := by
   have npos : 0 < n := (eq_zero_or_pos _).resolve_left fun n0 => by
@@ -334,29 +352,21 @@ theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
   intro h₁
   apply Nat.not_le_of_gt h₀ h₁.right
 
-protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
+@[simp] protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
   let t := add_mul_div_right 0 m H
   rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
 
-protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by
+@[simp] protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by
   rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
 
-protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
-  | 0, _ => by simp [Nat.div_zero, n.zero_le]
-  | succ k, h => by
-    suffices succ k * (m / succ k) ≤ succ k * n from
-      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
-    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
-    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
-    have h3 : m ≤ succ k * n := h
-    rw [← h2] at h3
-    exact Nat.le_trans h1 h3
 
-@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
-  induction n <;> simp_all [mul_succ]
+@[deprecated Nat.mul_div_cancel_left]
+theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n :=
+  Nat.mul_div_cancel_left n H
 
-@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
-  rw [Nat.mul_comm, mul_div_right _ H]
+@[deprecated  Nat.mul_div_cancel]
+theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m :=
+  Nat.mul_div_cancel m H
 
 protected theorem div_self (H : 0 < n) : n / n = 1 := by
   let t := add_div_right 0 H
@@ -379,5 +389,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,11 +9,11 @@ import Init.Meta
 
 namespace Nat
 
-protected theorem dvd_refl (a : Nat) : a ∣ a := ⟨1, by simp⟩
+@[simp] protected theorem dvd_refl (a : Nat) : a ∣ a := Exists.intro 1 (by simp)
 
-protected theorem dvd_zero (a : Nat) : a ∣ 0 := ⟨0, by simp⟩
+@[simp] protected theorem dvd_zero (a : Nat) : a ∣ 0 := Exists.intro 0 (by simp)
 
-protected theorem dvd_mul_left (a b : Nat) : a ∣ b * a := ⟨b, Nat.mul_comm b a⟩
+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_trans {a b c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c :=
@@ -25,23 +25,43 @@ 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⟩
+  Iff.intro Nat.eq_zero_of_zero_dvd
+            (fun h => h.symm ▸ Nat.dvd_refl 0)
 
 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
+protected theorem dvd_def (a b : Nat) : (a ∣ b) = Exists (fun c => b = a * c) := rfl
+
+@[simp] protected theorem one_dvd (n : Nat) : 1 ∣ n := ⟨n, n.one_mul.symm⟩
+
+-- 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]⟩
@@ -129,4 +148,13 @@ protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k
     have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
     rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
 
+theorem sub_div_dvd (a : Nat) {b c : Nat} (h : c ∣ b) : (a - b) / c = a / c - b / c := by
+  let ⟨d, p⟩ := h
+  cases c <;> simp [p, Nat.sub_mul_div]
+
+@[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]
+
 end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -787,7 +787,7 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
   | 0 => simp
   | x + 1 =>
     rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
-    simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
+    simp_arith [m_pos]
 
 theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   match x with
@@ -830,3 +830,60 @@ 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
+
+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]
+
+end Nat

src/Init/Data/Nat/Simproc.lean

@@ -89,6 +89,11 @@ theorem add_le_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b ≤ c + d)
 theorem add_le_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b ≤ c + d) = (a + (b - d) ≤ c) := by
   rw [← Nat.add_sub_assoc h, Nat.sub_le_iff_le_add]
 
+theorem add_le_eq (a b : Nat) : (a + b ≤ b) = (a = 0) := by
+  have r := add_le_add_le a 0 (Nat.le_refl b)
+  simp only [Nat.zero_add] at r
+  simp [r]
+
 theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c - b) := by
   have r := add_le_add_le a 0 h
   simp only [Nat.zero_add] at r
@@ -97,12 +102,34 @@ theorem add_le_le (a : Nat) {b c : Nat} (h : b ≤ c) : (a + b ≤ c) = (a ≤ c
 theorem add_le_gt (a : Nat) {b c : Nat} (h : b > c) : (a + b ≤ c) = False :=
   eq_false (Nat.not_le_of_gt (Nat.lt_of_lt_of_le h (le_add_left b a)))
 
+theorem add_lt_lt (a : Nat) {b c : Nat} (h : b < c) : (a + b < c) = (a < c - b) := by
+  have g := Nat.le_of_succ_le h
+  apply Eq.trans ?_ (add_le_le (a+1) g)
+  simp only [Nat.succ_add, Nat.add_assoc]
+  eq_refl
+
+theorem add_lt_ge (a : Nat) {b c : Nat} (h : b ≥ c) : (a + b < c) = False :=
+  eq_false (Nat.not_lt_of_ge (Nat.le_trans h (le_add_left b a)))
+
 theorem le_add_le (a : Nat) {b c : Nat} (h : a ≤ c) : (a ≤ b + c) = True :=
   eq_true (Nat.le_trans h (le_add_left c b))
 
-theorem le_add_ge (a : Nat) {b c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
+theorem le_add_ge {a : Nat} (b : Nat) {c : Nat} (h : a ≥ c) : (a ≤ b + c) = (a - c ≤ b) := by
   have r := add_le_add_ge 0 b h
   simp only [Nat.zero_add] at r
   exact r
 
+theorem lt_add_ge {a : Nat} (b : Nat) {c : Nat} (h : a ≥ c) : (a < b + c) = (a - c < b) := by
+  have r := le_add_ge b (@Nat.le.step _ _ h)
+  rw [Nat.succ_sub h] at r
+  exact r
+
+theorem add_lt_add_le (a c : Nat) {b d : Nat} (h : b ≤ d) : (a + b < c + d) = (a < c + (d - b)) := by
+  rw [← Nat.succ_le, ← Nat.succ_add, add_le_add_le _ _ h]
+  eq_refl
+
+theorem add_lt_add_ge (a c : Nat) {b d : Nat} (h : b ≥ d) : (a + b < c + d) = (a + (b - d) < c) := by
+  rw [← Nat.succ_le, ← Nat.succ_add, add_le_add_ge _ _ h, Nat.succ_add]
+  eq_refl
+
 end Nat.Simproc

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/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -25,6 +25,12 @@ def fromExpr? (e : Expr) : SimpM (Option Int) :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op v₁ v₂)
 
+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₂)
+
 @[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
@@ -65,6 +71,12 @@ builtin_dsimproc [simp, seval] reduceMul ((_ * _ : Int)) := reduceBin ``HMul.hMu
 builtin_dsimproc [simp, seval] reduceSub ((_ - _ : Int)) := reduceBin ``HSub.hSub 6 (· - ·)
 builtin_dsimproc [simp, seval] reduceDiv ((_ / _ : Int)) := reduceBin ``HDiv.hDiv 6 (· / ·)
 builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Int)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_dsimproc [simp, seval] reduceTDiv (div  _ _) := reduceBin ``Int.div 2 Int.div
+builtin_dsimproc [simp, seval] reduceTMod (mod  _ _) := reduceBin ``Int.mod 2 Int.mod
+builtin_dsimproc [simp, seval] reduceFDiv (fdiv _ _) := reduceBin ``Int.fdiv 2 Int.fdiv
+builtin_dsimproc [simp, seval] reduceFMod (fmod _ _) := reduceBin ``Int.fmod 2 Int.fmod
+builtin_dsimproc [simp, seval] reduceBdiv (bdiv _ _) := reduceBinIntNatOp ``bdiv bdiv
+builtin_dsimproc [simp, seval] reduceBmod (bmod _ _) := reduceBinIntNatOp ``bmod bmod
 
 builtin_dsimproc [simp, seval] reducePow ((_ : Int) ^ (_ : Nat)) := fun e => do
   let_expr HPow.hPow _ _ _ _ a b ← e | return .continue

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean

@@ -28,12 +28,6 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) :=
   let some m ← fromExpr? e.appArg! | return .continue
   return .done <| toExpr (op n m)
 
-@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
-  unless e.isAppOfArity declName arity do return .continue
-  let some n ← fromExpr? e.appFn!.appArg! | return .continue
-  let some m ← fromExpr? e.appArg! | return .continue
-  evalPropStep e (op n m)
-
 @[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
@@ -55,8 +49,6 @@ builtin_dsimproc [simp, seval] reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMo
 builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
-builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
-builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
 builtin_dsimproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
 
@@ -107,11 +99,11 @@ private partial def NatOffset.fromExprAux (e : Expr) (inc : Nat) : Meta.SimpM (O
     return if inc != 0 then some (e, inc) else none
 
 /- Attempt to parse a `NatOffset` from an expression-/
-private def NatOffset.fromExpr? (e : Expr) (inc : Nat := 0) : Meta.SimpM (Option NatOffset) := do
+private def NatOffset.fromExpr? (e : Expr) : Meta.SimpM (Option NatOffset) := do
   match ← Nat.fromExpr? e with
-  | some n => pure (some (const (n + inc)))
+  | some n => pure (some (const n))
   | none =>
-    match ← fromExprAux e inc with
+    match ← fromExprAux e 0 with
     | none => pure none
     | some (b, o) => pure (some (offset b (toExpr o) o))
 
@@ -251,18 +243,21 @@ builtin_simproc [simp, seval] reduceBneDiff ((_ : Nat) != _) := fun e => do
     let q := mkAppN (mkConst ``Nat.Simproc.bneEqOfEqEq) #[x, y, u, v, p]
     return .visit { expr := mkBneNat u v, proof? := some q, cache := true }
 
-def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step := do
+def reduceLE (nm : Name) (arity : Nat) (e : Expr) : SimpM Step := do
   unless e.isAppOfArity nm arity do
     return .continue
   let x := e.appFn!.appArg!
   let y := e.appArg!
-  let some xno ← NatOffset.fromExpr? x (inc := cond isLT 1 0) | return .continue
+  let some xno ← NatOffset.fromExpr? x | return .continue
   let some yno ← NatOffset.fromExpr? y | return .continue
   match xno, yno with
   | .const xn, .const yn =>
     Meta.Simp.evalPropStep e (xn ≤ yn)
   | .offset xb xo xn, .const yn => do
-    if xn ≤ yn then
+    if xn = yn then
+      let finExpr := mkEqNat xb (toExpr 0)
+      applySimprocConst finExpr ``Nat.Simproc.add_le_eq #[xb, xo]
+    else if xn < yn then
       let finExpr := mkLENat xb (toExpr (yn - xn))
       let leProof ← mkOfDecideEqTrue (mkLENat xo y)
       applySimprocConst finExpr ``Nat.Simproc.add_le_le #[xb, xo, y, leProof]
@@ -287,7 +282,45 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
       let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
       applySimprocConst finExpr ``Nat.Simproc.add_le_add_ge  #[xb, yb, xo, yo, geProof]
 
-builtin_simproc [simp, seval] reduceLeDiff ((_ : Nat) ≤ _) := reduceLTLE ``LE.le 4 false
+def reduceLT (nm : Name) (arity : Nat) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity nm arity do
+    return .continue
+  let x := e.appFn!.appArg!
+  let y := e.appArg!
+  let some xno ← NatOffset.fromExpr? x | return .continue
+  let some yno ← NatOffset.fromExpr? y | return .continue
+  match xno, yno with
+  | .const xn, .const yn =>
+    Meta.Simp.evalPropStep e (xn < yn)
+    -- xb < 1
+  | .offset xb xo xn, .const yn => do
+    if xn < yn then
+      let finExpr := mkLTNat xb (toExpr (yn - xn))
+      let ltProof ← mkOfDecideEqTrue (mkLTNat xo y)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_lt #[xb, xo, y, ltProof]
+    else
+      let geProof ← mkOfDecideEqTrue (mkGENat xo y)
+      applySimprocConst (mkConst ``False) ``Nat.Simproc.add_lt_ge #[xb, xo, y, geProof]
+  | .const xn, .offset yb yo yn => do
+    if xn < yn then
+      let ltProof ← mkOfDecideEqTrue (mkLTNat x yo)
+      applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, ltProof]
+    else
+      let finExpr := mkLTNat (toExpr (xn - yn)) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat x yo)
+      applySimprocConst finExpr ``Nat.Simproc.lt_add_ge #[x, yb, yo, geProof]
+  | .offset xb xo xn, .offset yb yo yn => do
+    if xn ≤ yn then
+      let finExpr := mkLTNat xb (if xn = yn then yb else mkAddNat yb (toExpr (yn - xn)))
+      let leProof ← mkOfDecideEqTrue (mkLENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_add_le  #[xb, yb, xo, yo, leProof]
+    else
+      let finExpr := mkLTNat (mkAddNat xb (toExpr (xn - yn))) yb
+      let geProof ← mkOfDecideEqTrue (mkGENat xo yo)
+      applySimprocConst finExpr ``Nat.Simproc.add_lt_add_ge  #[xb, yb, xo, yo, geProof]
+
+builtin_simproc [simp, seval] reduceLeDiff ((_ : Nat) ≤ _) := reduceLE ``LE.le 4
+builtin_simproc [simp, seval] reduceLtDiff ((_ : Nat) < _) := reduceLT ``LT.lt 4
 
 builtin_simproc [simp, seval] reduceSubDiff ((_ - _ : Nat)) := fun e => do
   unless e.isAppOfArity ``HSub.hSub 6 do

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,497 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Lean.Elab.Command
+import Lean.Elab.Tactic.Meta
+import Lean.Meta.CheckTactic
+
+open Lean Meta Elab Term CheckTactic Command
+
+/-
+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) (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 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/lean/librarySearch.lean

@@ -148,10 +148,22 @@ end synonym
 #guard_msgs in
 example : ∀ P : Prop, ¬(P ↔ ¬P) := by apply?
 
+-- Copy of P for testing purposes.
+inductive Q : Nat → Prop
+  | gt_in_head {n : Nat} : n < 0 → Q n
+
+theorem p_iff_q (i : Nat) : P i ↔ Q i :=
+  Iff.intro (fun ⟨i⟩ => Q.gt_in_head i) (fun ⟨i⟩ => P.gt_in_head i)
+
 -- We even find `iff` results:
-/-- info: Try this: exact (Nat.dvd_add_iff_left h₁).mpr h₂ -/
+
+/-- info: Try this: exact (p_iff_q a).mp h -/
 #guard_msgs in
-example {a b c : Nat} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b := by apply?
+example {a : Nat} (h : P a) : Q a := by apply?
+
+/-- info: Try this: exact (p_iff_q a).mpr h -/
+#guard_msgs in
+example {a : Nat} (h : Q a) : P a := by apply?
 
 -- Note: these examples no longer work after we turned off lemmas with discrimination key `#[*]`.
 -- example {α : Sort u} (h : Empty) : α := by apply? -- says `exact Empty.elim h`

tests/lean/run/simprocNat.lean

@@ -41,7 +41,7 @@ variable (a b : Nat)
 #check_simp (1234567 : Nat) ≠ 123456 ~> True
 #check_simp (a + 400) ≠ (b + 1000) ~> a ≠ b + 600
 
-/- leq -/
+/- le -/
 
 #check_simp (1234567 : Nat) ≤ 123456 ~> False
 #check_simp (1234567 : Nat) ≤ 1234567 ~> True
@@ -68,6 +68,36 @@ variable (a b : Nat)
 #check_simp 1000 ≥ (a + 1000) ~> a = 0
 #check_simp (a + 1000) ≥ (b +  400) ~> a + 600 ≥ b
 
+/- lt -/
+
+#check_simp (1234567 : Nat) < 123456 ~> False
+#check_simp (1234567 : Nat) < 1234567 ~> False
+#check_simp (1234567 : Nat) < 1234568 ~> True
+#check_simp (123456 : Nat) < 1234567 ~> True
+
+#check_simp (a +  999) < 1000 ~> a < 1
+#check_simp (a + 1000) < 1000 ~> False
+#check_simp (a + 1000) <  400 ~> False
+#check_simp (a +  400) < 1000 ~> a < 600
+
+#check_simp 1000 < (a + 1000) ~> 0 < a
+#check_simp 400  < (a + 1000) ~> True
+#check_simp 1000 < (a +  400) ~> 600 < a
+
+#check_simp (a +  999) < (b + 1000) ~> a < b + 1
+#check_simp (a + 1000) < (b + 1000) ~> a < b
+#check_simp (a + 1000) < (b +  400) ~> a + 600 < b
+#check_simp (a +  400) < (b + 1000) ~> a < b + 600
+#check_simp (Nat.add a 400) < (Add.add b 1000) ~> a < b + 600
+#check_simp (Nat.add a 400) < b.succ.succ ~> a + 398 < b
+
+/- gt (just make sure lt rules apply) -/
+
+#check_simp (123456 : Nat) > 1234567 ~> False
+#check_simp (a +  400) > 1000 ~> a > 600
+#check_simp 1000 > (a + 1000) ~> False
+#check_simp (a + 1000) > (b +  400) ~> a + 600 > b
+
 /- beq tests -/
 
 #check_simp (1234567 : Nat) == 123456 ~> false

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,522 @@
+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
+
+inductive NumType where
+  | prop
+  | nat
+  | int
+deriving DecidableEq, Hashable, Inhabited, Repr
+
+protected def NumType.render [Monad M] [MonadQuotation M] (v : NumType) : M Term := do
+  match v with
+  | prop => `(Prop)
+  | 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)
+  | natCast (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)
+  | eq (x y : NumTerm) (tp : NumType)
+  | le (x y : NumTerm) (tp : NumType)
+  | lt (x y : NumTerm) (tp : NumType)
+  | true | false
+  deriving BEq, Inhabited, Repr
+
+namespace NumTerm
+
+open NumType
+
+partial def map (f : NumTerm → NumTerm) (v : NumTerm) : NumTerm :=
+  match v with
+  | var _ | lit _ _ => v
+  | natCast x => natCast (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
+  | eq x y tp => eq (f x) (f y) tp
+  | le x y tp => le (f x) (f y) tp
+  | lt x y tp => lt (f x) (f y) tp
+  | true => true
+  | false => false
+
+protected def typeOf (v : NumTerm) : NumType :=
+  match v with
+  | var d => d.type
+  | lit _ tp => tp
+  | natCast _ => .int
+  | add _ _ tp | sub _ _ tp | mul _ _ tp => tp
+  | neg _ => .int
+  | div _ _ op | mod _ _ op => op.typeOf
+  | eq .. | le .. | lt .. | true | false => .prop
+
+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)))
+  | natCast x => `(($(←x.render).cast : Int))
+  | add x y tp => `((($(←x.render) + $(←y.render)) : $(← tp.render)))
+  | sub x y tp => `((($(←x.render) - $(←y.render)) : $(← tp.render)))
+  | mul x y tp => `((($(←x.render) * $(←y.render)) : $(← tp.render)))
+  | neg x => `(- $(←x.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))
+  | eq x y _ => `($(←x.render) = $(←y.render))
+  | le x y _ => `($(←x.render) ≤ $(←y.render))
+  | lt x y _ => `($(←x.render) < $(←y.render))
+  | true => `(True)
+  | false => `(False)
+
+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 mkConstProp (b : Bool) : NumTerm := cond b .true .false
+
+def mkLit (i : Int) (tp : NumType) : NumTerm :=
+  if i < 0 then
+    match tp with
+    | .prop => panic! "prop literal not allowed"
+    | .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
+
+/--
+Returns nat term or literal equal to input term if input
+term is a literal or has form `natToInt _`.
+-/
+def intAtNat (x : NumTerm) : Option NumTerm :=
+  match x with
+  | lit xn .int => some (lit xn .nat)
+  | natCast x => some x
+  | _ => none
+
+def isPos (x : NumTerm) : Bool :=
+  match x with
+  | lit xn .nat => xn > 0
+  | _ => Bool.false
+
+partial def simp (v : NumTerm) : NumTerm :=
+  let v := map simp v
+  match v with
+  | natCast x =>
+    (match x with
+    | lit n _ => lit n .int
+    | add x y _ => simp <| add (natCast x) (natCast y) .int
+    | mul x y _ => simp <| mul (natCast x) (natCast y) .int
+    | div x y _ => simp <| div (natCast x) (natCast y) .edivInt
+    | mod x y _ => simp <| mod (natCast x) (natCast y) .edivInt
+    | var _ | sub .. | neg _ | natCast _
+      | eq .. | le .. | lt .. | true | false => 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
+      | .prop =>
+        panic! "sub applied to prop"
+      | .nat =>
+        if let (lit xo _, lit yo _) := (x, y) then
+          return lit (xo - yo) .nat
+        if let (lit xo _, add yb (lit yo _) _) := (x, y) then
+          let r :=
+            if xo > yo then
+              sub (lit (xo - yo) nat) yb nat
+            else
+              lit 0 nat
+          return r
+        if let (add xb (lit xo _) _, lit yo _) := (x, y) then
+          let r :=
+            if xo > yo then
+              add xb (lit (xo - yo) nat) nat
+            else if xo < yo then
+              sub xb (lit (yo - xo) nat) nat
+            else
+              xb
+          return r
+        if let (add xb (lit xo _) _, add yb (lit yo _) _) := (x, y) then
+          let r :=
+            if xo > yo then
+              sub (add xb (lit (xo - yo) nat) nat) yb nat
+            else if xo < yo then
+              sub xb (add yb (lit (yo - xo) nat) nat) nat
+            else
+              sub xb yb nat
+          return r
+      | .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
+        let rop : Option NumTerm :=
+          match op, xop with
+          | .divNat,  .divNat  => do guard (n == xd); some (mod xn n .divNat)
+          | .edivInt, .bdivInt => do guard (n == natCast xd); some (mod xn n .edivInt)
+          | .edivInt, _        => do guard (n == xd); some (mod xn n .edivInt)
+          | .tdivInt, .edivInt => do guard (n == xd); some (mod xn n .edivInt)
+          | .tdivInt, .tdivInt => do guard (n == xd); some (mod xn n .tdivInt)
+          | .fdivInt, .edivInt => do guard (n == xd); some (mod xn n .fdivInt)
+          | .fdivInt, .fdivInt => do guard (n == xd); some (mod xn n .fdivInt)
+          | .bdivInt, .bdivInt => do guard (n == xd); some (mod xn n .bdivInt)
+          | .bdivInt, _        => do guard (natCast n == xd); some (mod xn n .bdivInt)
+          | _, _ => none
+        if let some r := rop then
+            return simp r
+      if let neg yn := n then
+        match op with
+        | .edivInt | .tdivInt =>
+          return simp (mod x yn op)
+        | _ =>
+          pure ()
+      return v
+  | eq x y _ => Id.run do
+      if let (some i, some j) := (asIntLit x, asIntLit y) then
+        return mkConstProp (i = j)
+      if x == y then
+        return NumTerm.true
+      pure v
+  | le x y _ => Id.run do
+      if let (some i, some j) := (asIntLit x, asIntLit y) then
+        return mkConstProp (i ≤ j)
+--      if let (some xn, some yn) := (intAtNat x, intAtNat y) then
+--        return (le xn yn .nat)
+      if x == y then
+        return NumTerm.true
+      pure v
+  | lt x y tp => Id.run do
+      if let (some i, some j) := (asIntLit x, asIntLit y) then
+        return mkConstProp (i < j)
+      if let (lit 0 .int, natCast yn) := (x, y) then
+        return simp (lt (lit 0 .nat) yn .nat)
+      if let (natCast xn, natCast yn) := (x, y) then
+        return simp (lt xn yn .nat)
+      if tp = .nat then
+        if x == y then
+          return NumTerm.false
+        if let add yb (lit yo _) _ := y then
+          if x == yb then
+            return mkConstProp (yo > 0)
+        if let (lit xo _, add yb (lit yo _) _) := (x, y) then
+          let r := if xo < yo then NumTerm.true else lt (lit (xo - yo) .nat) yb .nat
+          return r
+        if let (add xb (lit xo _) _, lit yo _) := (x, y) then
+          let r :=
+            if xo < yo then
+              lt xb (lit (yo - xo) .nat) .nat
+            else
+              NumTerm.false
+          return r
+        if let (add xb (lit xo _) _, add yb (lit yo _) _) := (x, y) then
+          let r :=
+            if xo < yo then
+              lt xb (add yb (lit (yo - xo) .nat) .nat) .nat
+            else if xo > yo then
+              lt (add xb (lit (xo - yo) .nat) .nat) yb .nat
+            else
+              lt xb yb .nat
+          return r
+        if let (lit 0 _, mul y1 y2 _) := (x, y) then
+          if isPos y1 then
+            return lt (lit 0 nat) y2 nat
+          if isPos y2 then
+            return lt (lit 0 nat) y1 nat
+      pure v
+  | true | false | lit _ _ | var _ => 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 binOp (op : NumTerm → NumTerm → NumType → NumTerm) (tp : NumType) :=
+  mkOp [tp, tp] tp fun a => op (a[0]!) (a[1]!) tp
+def binRel (op : NumTerm → NumTerm → NumType → NumTerm) (tp : NumType) :=
+  mkOp [tp, tp] .prop fun a => op (a[0]!) (a[1]!) tp
+def negOp : Op NumType NumTerm := mkOp [.int] .int fun a => neg (a[0]!)
+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
+def natToIntOp := mkOp [NumType.nat] .int fun x => natCast x[0]!
+
+end NumTerm
+
+open NumTerm
+
+syntax:lead (name := intTestElab) "#intTest" : command
+
+@[command_elab intTestElab]
+def elabIntTest : CommandElab := fun _stx => do
+  let types : List NumType := [.prop, .nat, .int]
+  let ops := [
+      litOp 0 .nat,
+      litOp 1 .nat,
+      litOp 2 .nat,
+      litOp 0 .int,
+      litOp 1 .int,
+      litOp 2 .int,
+      natToIntOp,
+      binOp add .nat, binOp add .int,
+      binOp sub .nat, binOp sub .int,
+      binOp mul .nat, binOp mul .int,
+      negOp,
+      divOp .divNat, divOp .edivInt, divOp .fdivInt, divOp .tdivInt, divOp .bdivInt .nat,
+      modOp .divNat, modOp .edivInt, modOp .fdivInt, modOp .tdivInt, modOp .bdivInt .nat,
+      binRel eq .nat, binRel eq .int,
+      binRel le .nat, binRel le .int,
+      binRel lt .nat, binRel lt .int,
+  ]
+  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 pp.coercions false
+set_option pp.explicit true
+set_option maxHeartbeats 100000000
+#intTest
+
+variable (m n : Nat)
+
+/-
+
+  @LT.lt Nat instLTNat (@OfNat.ofNat Nat 1 (instOfNatNat 1))
+    (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n0 (@OfNat.ofNat Nat 2 (instOfNatNat 2))) reduces to
+  @LT.lt Nat instLTNat (@OfNat.ofNat Nat 1 (instOfNatNat 1))
+    (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n0 (@OfNat.ofNat Nat 2 (instOfNatNat 2)))
+but is expected to reduce to
+  True
+
+-/
+
+set_option trace.Meta.Tactic.simp.rewrite true
+
+#check_tactic n < n + 1 ~> True by simp
+
+#check_tactic 0 < n + 2 ~> True by
+  simp
+
+#check_simp 1 < n + 2 !~>
+
+
+#print Nat.mul_pos_iff_of_pos_left
+#check_tactic 0 < n + 2 ~> True by simp
+
+#check_tactic 0 < 2 * n ~> 0 < n by simp
+
+
+
+#check_tactic (@OfNat.ofNat Int 0 (@instOfNat 0)) < (@Nat.cast Int _ n0) ~> m < n by
+  simp
+
+set_option trace.Meta.Tactic.simp.rewrite true
+
+#print Int.ofNat_pos
+
+#check_tactic ((0 : Int) < @Nat.cast Int _ n) ~> 0 < n by
+  simp
+
+
+#check_simp ((1 : Int) < @Nat.cast Int _ n) !~> 1 < n.cast
+
+#check_tactic ((0 : Int) < (n : Int)) ~> 0 < n by
+  simp
+
+
+--set_option pp.notation fals
+
+example : ((1 : Nat) < (n : Int)) := by
+  simp
+
+#check_tactic ((1 : Nat) < (n : Int)) ~> 1 < n by
+  simp
+
+#check_tactic (n < n + 2) ~> True by
+  simp
+
+
+
+--#check_tactic (1 < (n : Int)) ~> 1 < n by
+--  simp
+
+/-
+
+-/