chore: remove leftovers (#9347)

after update stage0

src/Init/Data/Int/Linear.lean

@@ -1737,34 +1737,6 @@ theorem emod_le (x y : Int) (n : Int) : emod_le_cert y n → x % y + n ≤ 0 :=
     simp only [Int.add_comm, Int.sub_neg, Int.add_zero]
     exact Int.emod_lt_of_pos x h
 
--- TODO: delete
-theorem natCast_nonneg (x : Nat) : (-1:Int) * NatCast.natCast x ≤ 0 := by
-  simp
-
--- TODO: delete
-theorem natCast_sub (x y : Nat)
-    : (NatCast.natCast (x - y) : Int)
-      =
-      if (NatCast.natCast y : Int) + (-1)*NatCast.natCast x ≤ 0 then
-        (NatCast.natCast x : Int) + -1*NatCast.natCast y
-      else
-        (0 : Int) := by
-  change (↑(x - y) : Int) = if (↑y : Int) + (-1)*↑x ≤ 0 then (↑x : Int) + (-1)*↑y else 0
-  rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
-  rw [Int.neg_mul, ← Int.sub_eq_add_neg, Int.one_mul]
-  split
-  next h =>
-    replace h := Int.le_of_sub_nonpos h
-    rw [Int.ofNat_le] at h
-    rw [Int.ofNat_sub h]
-  next h =>
-    have : ¬ (↑y : Int) ≤ ↑x := by
-      intro h
-      replace h := Int.sub_nonpos_of_le h
-      contradiction
-    rw [Int.ofNat_le] at this
-    rw [Lean.Omega.Int.ofNat_sub_eq_zero this]
-
 private theorem dvd_le_tight' {d p b₁ b₂ : Int} (hd : d > 0) (h₁ : d ∣ p + b₁) (h₂ : p + b₂ ≤ 0)
     : p + (b₁ - d*((b₁-b₂) / d)) ≤ 0 := by
   have ⟨k, h⟩ := h₁

src/Init/Data/Int/OfNat.lean

@@ -13,108 +13,13 @@ public import Init.Data.RArray
 
 public section
 
--- TODO: this namespace will deleted after we move to the new encoding using `Nat.ToInt` namespace.
--- Bootstrapping sucks.
-namespace Int.OfNat
-/-!
-Helper definitions and theorems for converting `Nat` expressions into `Int` one.
-We use them to implement the arithmetic theories in `grind`
--/
-
-abbrev Var := Nat
-abbrev Context := Lean.RArray Nat
-@[expose]
-def Var.denote (ctx : Context) (v : Var) : Nat :=
-  ctx.get v
-
-inductive Expr where
-  | num  (v : Nat)
-  | var  (i : Var)
-  | add  (a b : Expr)
-  | mul  (a b : Expr)
-  | div  (a b : Expr)
-  | mod  (a b : Expr)
-  | pow  (a : Expr) (k : Nat)
-  deriving BEq
-
-@[expose]
-def Expr.denote (ctx : Context) : Expr → Nat
-  | .num k    => k
-  | .var v    => v.denote ctx
-  | .add a b  => Nat.add (denote ctx a) (denote ctx b)
-  | .mul a b  => Nat.mul (denote ctx a) (denote ctx b)
-  | .div a b  => Nat.div (denote ctx a) (denote ctx b)
-  | .mod a b  => Nat.mod (denote ctx a) (denote ctx b)
-  | .pow a k  => Nat.pow (denote ctx a) k
-
-@[expose]
-def Expr.denoteAsInt (ctx : Context) : Expr → Int
-  | .num k    => Int.ofNat k
-  | .var v    => Int.ofNat (v.denote ctx)
-  | .add a b  => Int.add (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .mul a b  => Int.mul (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .div a b  => Int.ediv (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .mod a b  => Int.emod (denoteAsInt ctx a) (denoteAsInt ctx b)
-  | .pow a k  => Int.pow (denoteAsInt ctx a) k
-
-theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by
-  induction e <;> simp [denote, denoteAsInt, *] <;> rfl
-
-theorem Expr.eq_denoteAsInt (ctx : Context) (e : Expr) : e.denote ctx = e.denoteAsInt ctx := by
-  apply Eq.symm; apply denoteAsInt_eq
-
-theorem Expr.eq (ctx : Context) (lhs rhs : Expr)
-    : (lhs.denote ctx = rhs.denote ctx) = (lhs.denoteAsInt ctx = rhs.denoteAsInt ctx) := by
-  simp [denoteAsInt_eq, Int.ofNat_inj]
-
-theorem Expr.le (ctx : Context) (lhs rhs : Expr)
-    : (lhs.denote ctx ≤ rhs.denote ctx) = (lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx) := by
-  simp [denoteAsInt_eq, Int.ofNat_le]
-
-theorem of_le (ctx : Context) (lhs rhs : Expr)
-    : lhs.denote ctx ≤ rhs.denote ctx → lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx := by
-  rw [Expr.le ctx lhs rhs]; simp
-
-theorem of_not_le (ctx : Context) (lhs rhs : Expr)
-    : ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ lhs.denoteAsInt ctx ≤ rhs.denoteAsInt ctx := by
-  rw [Expr.le ctx lhs rhs]; simp
-
-theorem of_dvd (ctx : Context) (d : Nat) (e : Expr)
-    : d ∣ e.denote ctx → Int.ofNat d ∣ e.denoteAsInt ctx := by
-  simp [Expr.denoteAsInt_eq, Int.ofNat_dvd]
-
-theorem of_eq (ctx : Context) (lhs rhs : Expr)
-    : lhs.denote ctx = rhs.denote ctx → lhs.denoteAsInt ctx = rhs.denoteAsInt ctx := by
-  rw [Expr.eq ctx lhs rhs]; simp
-
-theorem of_not_eq (ctx : Context) (lhs rhs : Expr)
-    : ¬ lhs.denote ctx = rhs.denote ctx → ¬ lhs.denoteAsInt ctx = rhs.denoteAsInt ctx := by
-  rw [Expr.eq ctx lhs rhs]; simp
-
-theorem ofNat_toNat (a : Int) : (NatCast.natCast a.toNat : Int) = if a ≤ 0 then 0 else a := by
-  split
-  next h =>
-    rw [Int.toNat_of_nonpos h]; rfl
-  next h =>
-    simp at h
-    have := Int.toNat_of_nonneg (Int.le_of_lt h)
-    assumption
-
-theorem Expr.denoteAsInt_nonneg (ctx : Context) (e : Expr) : 0 ≤ e.denoteAsInt ctx := by
-  simp [Expr.denoteAsInt_eq]
-
-end Int.OfNat
-
 namespace Nat.ToInt
 
-theorem ofNat_toNat (a : Int) : (NatCast.natCast a.toNat : Int) = if a ≤ 0 then 0 else a := by
-  simp [Int.max_def]
+theorem ofNat_toNat (a : Int) : (NatCast.natCast a.toNat : Int) = if a ≤ 0 then 0 else a := by simp [Int.max_def]
 
-theorem toNat_nonneg (x : Nat) : (-1:Int) * (NatCast.natCast x) ≤ 0 := by
-  simp
+theorem toNat_nonneg (x : Nat) : (-1:Int) * (NatCast.natCast x) ≤ 0 := by simp
 
-theorem natCast_ofNat (n : Nat) : (NatCast.natCast (OfNat.ofNat n : Nat) : Int) = OfNat.ofNat n := by
-  rfl
+theorem natCast_ofNat (n : Nat) : (NatCast.natCast (OfNat.ofNat n : Nat) : Int) = OfNat.ofNat n := by rfl
 
 theorem of_eq {a b : Nat} {a' b' : Int}
     (h₁ : NatCast.natCast a = a') (h₂ : NatCast.natCast b = b') : a = b → a' = b' := by
@@ -182,34 +87,17 @@ end Nat.ToInt
 
 namespace Int.Nonneg
 
-
-@[expose]
-def num_cert (a : Int) : Bool := a ≥ 0
-
-theorem num (a : Int) : num_cert a → a ≥ 0 := by
-  simp [num_cert]
-
-theorem add (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a + b ≥ 0 := by
-  exact Int.add_nonneg h₁ h₂
-
-theorem mul (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a * b ≥ 0 := by
-  exact Int.mul_nonneg h₁ h₂
-
-theorem div (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a / b ≥ 0 := by
-  exact Int.ediv_nonneg h₁ h₂
-
-theorem pow (a : Int) (k : Nat) (h₁ : a ≥ 0) : a ^ k ≥ 0 := by
-  exact Int.pow_nonneg h₁
-
+@[expose] def num_cert (a : Int) : Bool := a ≥ 0
+theorem num (a : Int) : num_cert a → a ≥ 0 := by simp [num_cert]
+theorem add (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a + b ≥ 0 := by exact Int.add_nonneg h₁ h₂
+theorem mul (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a * b ≥ 0 := by exact Int.mul_nonneg h₁ h₂
+theorem div (a b : Int) (h₁ : a ≥ 0) (h₂ : b ≥ 0) : a / b ≥ 0 := by exact Int.ediv_nonneg h₁ h₂
+theorem pow (a : Int) (k : Nat) (h₁ : a ≥ 0) : a ^ k ≥ 0 := by exact Int.pow_nonneg h₁
 theorem mod (a b : Int) (h₁ : a ≥ 0) : a % b ≥ 0 := by
   by_cases b = 0
   next => simp [*]
   next h => exact emod_nonneg a h
-
-theorem natCast (a : Nat) : (NatCast.natCast a : Int) ≥ 0 := by
-  simp
-
-theorem toPoly (e : Int) : e ≥ 0 → -1 * e ≤ 0 := by
-  omega
+theorem natCast (a : Nat) : (NatCast.natCast a : Int) ≥ 0 := by simp
+theorem toPoly (e : Int) : e ≥ 0 → -1 * e ≤ 0 := by omega
 
 end Int.Nonneg

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -419,7 +419,7 @@ private def propagateNatAbs (e : Expr) : GoalM Unit := do
 
 private def propagateToNat (e : Expr) : GoalM Unit := do
   let_expr Int.toNat a := e | return ()
-  pushNewFact <| mkApp (mkConst ``Int.OfNat.ofNat_toNat) a
+  pushNewFact <| mkApp (mkConst ``Nat.ToInt.ofNat_toNat) a
 
 private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -17,7 +17,6 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 namespace Lean.Meta.Grind.Arith.Cutsat
 
 deriving instance Hashable for Int.Linear.Expr
-deriving instance Hashable for Int.OfNat.Expr
 
 structure ProofM.State where
   cache       : Std.HashMap UInt64 Expr := {}

tests/lean/run/grind_cutsat_nat_le.lean

@@ -1,6 +1,5 @@
 
-open Int.Linear Int.OfNat
-
+open Int.Linear
 
 set_option trace.grind.debug.proof true in
 theorem ex1 (x y z : Nat) : x < y + z → y + 1 < z → z + x < 3*z := by
@@ -14,7 +13,7 @@ theorem ex3 (x y : Nat) :
     7*y ≤ 9*x + 10 → 9*x ≤ 4 + 7*y → False := by
   grind
 
-open Int.Linear Int.OfNat
+open Int.Linear
 #print ex1
 #print ex2
 #print ex3