chore: add norm_cast_add_elim ne_eq

Recall that `add_elim` was a local command in Std

src/Init/Data/Int/DivModLemmas.lean

@@ -22,7 +22,7 @@ namespace Int
 
 /-! ### `/`  -/
 
-@[simp] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
+@[simp, norm_cast] theorem ofNat_ediv (m n : Nat) : (↑(m / n) : Int) = ↑m / ↑n := rfl
 
 @[simp] theorem zero_ediv : ∀ b : Int, 0 / b = 0
   | ofNat _ => show ofNat _ = _ by simp
@@ -102,7 +102,7 @@ theorem ofNat_mod (m n : Nat) : (↑(m % n) : Int) = mod m n := rfl
 
 theorem ofNat_mod_ofNat (m n : Nat) : (m % n : Int) = ↑(m % n) := rfl
 
-@[simp] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
+@[simp, norm_cast] theorem ofNat_emod (m n : Nat) : (↑(m % n) : Int) = m % n := rfl
 
 @[simp] theorem zero_emod (b : Int) : 0 % b = 0 := by simp [mod_def', emod]
 
@@ -260,7 +260,7 @@ protected theorem dvd_sub : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b -
   | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Int.mul_sub]⟩
 
 
-theorem ofNat_dvd {m n : Nat} : (↑m : Int) ∣ ↑n ↔ m ∣ n := by
+@[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 =>

src/Init/Data/Int/Lemmas.lean

@@ -22,8 +22,8 @@ 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
 
-theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := rfl
-theorem ofNat_mul (n m : Nat) : (↑(n * m) : Int) = n * m := rfl
+@[norm_cast] theorem ofNat_add (n m : Nat) : (↑(n + m) : Int) = n + m := 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
 
 @[local simp] theorem neg_ofNat_zero : -((0 : Nat) : Int) = 0 := rfl
@@ -53,7 +53,7 @@ theorem negOfNat_eq : negOfNat n = -ofNat n := rfl
 
 /- ## some basic functions and properties -/
 
-theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
+@[norm_cast] theorem ofNat_inj : ((m : Nat) : Int) = (n : Nat) ↔ m = n := ⟨ofNat.inj, congrArg _⟩
 
 theorem ofNat_eq_zero : ((n : Nat) : Int) = 0 ↔ n = 0 := ofNat_inj
 
@@ -67,7 +67,7 @@ theorem negSucc_eq (n : Nat) : -[n+1] = -((n : Int) + 1) := rfl
 
 @[simp] theorem zero_ne_negSucc (n : Nat) : 0 ≠ -[n+1] := nofun
 
-@[simp] theorem Nat.cast_ofNat_Int :
+@[simp, norm_cast] theorem Nat.cast_ofNat_Int :
   (Nat.cast (no_index (OfNat.ofNat n)) : Int) = OfNat.ofNat n := rfl
 
 /- ## neg -/
@@ -295,7 +295,7 @@ protected theorem sub_neg (a b : Int) : a - -b = a + b := by simp [Int.sub_eq_ad
 protected theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c) := by
   rw [Int.sub_eq_add_neg, Int.add_assoc, ← Int.sub_eq_add_neg]
 
-theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
+@[norm_cast] theorem ofNat_sub (h : m ≤ n) : ((n - m : Nat) : Int) = n - m := by
   match m with
   | 0 => rfl
   | succ m =>

src/Init/Data/Int/Order.lean

@@ -48,7 +48,7 @@ protected theorem le_total (a b : Int) : a ≤ b ∨ b ≤ a :=
   (nonneg_or_nonneg_neg (b - a)).imp_right fun H => by
     rwa [show -(b - a) = a - b by simp [Int.add_comm, Int.sub_eq_add_neg]] at H
 
-@[simp] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
+@[simp, norm_cast] theorem ofNat_le {m n : Nat} : (↑m : Int) ≤ ↑n ↔ m ≤ n :=
   ⟨fun h =>
     let ⟨k, hk⟩ := le.dest h
     Nat.le.intro <| Int.ofNat.inj <| (Int.ofNat_add m k).trans hk,
@@ -74,10 +74,10 @@ theorem lt.intro {a b : Int} {n : Nat} (h : a + Nat.succ n = b) : a < b :=
 theorem lt.dest {a b : Int} (h : a < b) : ∃ n : Nat, a + Nat.succ n = b :=
   let ⟨n, h⟩ := le.dest h; ⟨n, by rwa [Int.add_comm, Int.add_left_comm] at h⟩
 
-@[simp] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by
+@[simp, norm_cast] theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m := by
   rw [lt_iff_add_one_le, ← ofNat_succ, ofNat_le]; rfl
 
-@[simp] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
+@[simp, norm_cast] theorem ofNat_pos {n : Nat} : 0 < (↑n : Int) ↔ 0 < n := ofNat_lt
 
 theorem ofNat_nonneg (n : Nat) : 0 ≤ (n : Int) := ⟨_⟩
 

src/Init/SimpLemmas.lean

@@ -84,6 +84,7 @@ theorem dite_congr {_ : Decidable b} [Decidable c]
   | inr h => rw [dif_neg h]; subst b; rw [dif_neg h]; exact h₃ h
 
 @[simp] theorem ne_eq (a b : α) : (a ≠ b) = ¬(a = b) := rfl
+norm_cast_add_elim ne_eq
 @[simp] theorem ite_true (a b : α) : (if True then a else b) = a := rfl
 @[simp] theorem ite_false (a b : α) : (if False then a else b) = b := rfl
 @[simp] theorem dite_true {α : Sort u} {t : True → α} {e : ¬ True → α} : (dite True t e) = t True.intro := rfl

src/Init/Tactics.lean

@@ -1156,6 +1156,11 @@ end
 syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
   (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
 
+/--
+`norm_cast_add_elim foo` registers `foo` as an elim-lemma in `norm_cast`.
+-/
+syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Tactic/NormCast.lean

@@ -262,4 +262,12 @@ def evalPushCast : Tactic := fun stx => do
   dischargeWrapper.with fun discharge? =>
     discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
 
+open Command in
+@[builtin_command_elab Parser.Tactic.normCastAddElim] def elabAddElim : CommandElab := fun stx => do
+  match stx with
+  | `(norm_cast_add_elim $id:ident) =>
+    Elab.Command.liftCoreM do MetaM.run' do
+     addElim (← resolveGlobalConstNoOverload id)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.NormCast

src/Lean/Meta/Tactic/NormCast.lean

@@ -90,7 +90,7 @@ def classifyType (ty : Expr) : MetaM Label :=
         rhs must have fewer head coes than lhs{indentExpr ty}"
 
 /-- The `push_cast` simp attribute. -/
-initialize pushCastExt : SimpExtension ←
+builtin_initialize pushCastExt : SimpExtension ←
   registerSimpAttr `push_cast "\
     The `push_cast` simp attribute uses `norm_cast` lemmas \
     to move casts toward the leaf nodes of the expression."

tests/lean/run/norm_cast.lean

@@ -19,3 +19,66 @@ example (a b c : Bool) (n : Nat) (h : n = (a && b && c))
   norm_cast
   guard_target =ₛ ↑(a && b && c) = n
   rw [h]
+
+
+set_option linter.missingDocs false
+
+variable (an bn cn dn : Nat) (az bz cz dz : Int)
+
+example : (an : Int) = bn → an = bn := by intro h; exact_mod_cast h
+example : an = bn → (an : Int) = bn := by intro h; exact_mod_cast h
+
+example : (an : Int) < bn ↔ an < bn := by norm_cast
+example : (an : Int) ≠ (bn : Int) ↔ an ≠ bn := by norm_cast
+
+-- zero and one cause special problems
+example : az > (1 : Nat) ↔ az > 1 := by norm_cast
+example : az > (0 : Nat) ↔ az > 0 := by norm_cast
+
+example : (an : Int) ≠ 0 ↔ an ≠ 0 := by norm_cast
+
+example (a b : Nat) (h : False) : (a : Int) < ((2 * b : Nat) : Int) := by
+  push_cast
+  guard_target = (a : Int) < 2 * (b : Int)
+  cases h
+
+example : (an : Int) + bn = (an + bn : Nat) := by norm_cast
+
+example (h : ((an + bn : Nat) : Int) = (an : Int) + (bn : Int)) : True := by
+  push_cast at h
+  guard_hyp h : (an : Int) + (bn : Int) = (an : Int) + (bn : Int)
+  trivial
+
+example (h : ((an * bn : Nat) : Int) = (an : Int) * (bn : Int)) : True := by
+  push_cast at h
+  guard_hyp h : (an : Int) * (bn : Int) = (an : Int) * (bn : Int)
+  trivial
+
+--testing numerals
+example : ((42 : Nat) : Int) = 42 := by norm_cast
+
+structure p (n : Int)
+example : p 42 := by
+  norm_cast
+  guard_target = p 42
+  exact ⟨⟩
+
+example : an + bn = 1 ↔ (an + bn : Int) = 1 := by norm_cast
+
+example (h : bn ≤ an) : an - bn = 1 ↔ (an - bn : Int) = 1 := by norm_cast
+
+example (k : Nat) {x y : Nat} (h : ((x + y + k : Nat) : Int) = 0) : x + y + k = 0 := by
+  push_cast at h
+  guard_hyp h : (x : Int) + y + k = 0
+  assumption_mod_cast
+
+example (a b : Nat) (h2 : ((a + b + 0 : Nat) : Int) = 10) :
+    ((a + b : Nat) : Int) = 10 := by
+  push_cast
+  push_cast [Int.add_zero] at h2
+  exact h2
+
+theorem b (_h g : true) : true ∧ true := by
+  constructor
+  assumption_mod_cast
+  assumption_mod_cast