feat: add norm_num extensions (#28836)

Add `norm_num` extensions for

- `Int.negOfNat`;
-  `Nat.floor`, `Nat.ceil`, and `Int.round`.

Author: yury-harmonic

Mathlib/Algebra/Order/Floor/Semifield.lean

@@ -101,3 +101,70 @@ lemma ceil_le_two_mul (ha : 2⁻¹ ≤ a) : ⌈a⌉₊ ≤ 2 * a :=
 end LinearOrderedField
 
 end Nat
+
+namespace Mathlib.Meta.NormNum
+
+open Qq
+
+/-!
+### `norm_num` extension for `Nat.floor`
+-/
+
+theorem IsNat.natFloor {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (m : ℕ) : IsNat r m → IsNat (⌊r⌋₊) m := by
+  rintro ⟨⟨⟩⟩
+  exact ⟨by simp⟩
+
+theorem IsInt.natFloor {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (m : ℕ) : IsInt r (.negOfNat m) → IsNat (⌊r⌋₊) 0 := by
+  rintro ⟨⟨⟩⟩
+  exact ⟨Nat.floor_of_nonpos <| by simp⟩
+
+theorem IsNNRat.natFloor {R : Type*} [Semifield R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (n d : ℕ) (h : IsNNRat r n d) (res : ℕ) (hres : n / d = res) :
+    IsNat ⌊r⌋₊ res := by
+  constructor
+  rw [← hres, h.to_eq rfl rfl, Nat.floor_div_eq_div, Nat.cast_id]
+
+theorem IsRat.natFloor {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (n d : ℕ) (h : IsRat r (Int.negOfNat n) d) : IsNat ⌊r⌋₊ 0 := by
+  rcases h with ⟨hd, rfl⟩
+  constructor
+  rw [Nat.cast_zero, Nat.floor_eq_zero]
+  exact lt_of_le_of_lt (by simp [mul_nonneg]) one_pos
+
+open Lean in
+/-- `norm_num` extension for `Nat.floor` -/
+@[norm_num ⌊_⌋₊]
+def evalNatFloor : NormNumExt where eval {u αZ} e := do
+  match u, αZ, e with
+  | 0, ~q(ℕ), ~q(@Nat.floor $α $instSemiring $instPartialOrder $instFloorSemiring $x) =>
+    match ← derive x with
+    | .isBool .. => failure
+    | .isNat sα nb pb => do
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) nb q(IsNat.natFloor $x _ $pb)
+    | .isNegNat sα nb pb => do
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) (mkRawNatLit 0) q(IsInt.natFloor _ _ $pb)
+    | .isNNRat dα q n d h => do
+      let instSemifield ← synthInstanceQ q(Semifield $α)
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      have z : Q(ℕ) := mkRawNatLit (q.num.toNat / q.den)
+      haveI : $z =Q $n / $d := ⟨⟩
+      return .isNat q(inferInstance) z q(IsNNRat.natFloor _ $n $d $h $z rfl)
+    | .isNegNNRat _ q n d h => do
+      let instField ← synthInstanceQ q(Field $α)
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) (mkRawNatLit 0) q(IsRat.natFloor $x $n $d $h)
+  | _, _, _ => failure
+
+end Mathlib.Meta.NormNum

Mathlib/Data/NNRat/Floor.lean

@@ -92,3 +92,69 @@ theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ≥0)⌋₊
   Rat.natFloor_natCast_div_natCast n d
 
 end NNRat
+
+namespace Mathlib.Meta.NormNum
+
+open Qq
+
+/-!
+### `norm_num` extension for `Nat.ceil`
+-/
+
+theorem IsNat.natCeil {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (m : ℕ) : IsNat r m → IsNat (⌈r⌉₊) m := by
+  rintro ⟨⟨⟩⟩
+  exact ⟨by simp⟩
+
+theorem IsInt.natCeil {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R]
+    (r : R) (m : ℕ) : IsInt r (.negOfNat m) → IsNat (⌈r⌉₊) 0 := by
+  rintro ⟨⟨⟩⟩
+  exact ⟨by simp⟩
+
+theorem IsNNRat.natCeil {R : Type*} [Semifield R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (n d : ℕ) (h : IsNNRat r n d) (res : ℕ)
+    (hres : ⌈(n / d : ℚ≥0)⌉₊ = res) : IsNat ⌈r⌉₊ res := by
+  constructor
+  rw [← hres, h.to_eq rfl rfl, ← @NNRat.ceil_cast R]
+  simp
+
+theorem IsRat.natCeil {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorSemiring R] (r : R) (n d : ℕ) (h : IsRat r (.negOfNat n) d) : IsNat ⌈r⌉₊ 0 := by
+  constructor
+  simp [h.neg_to_eq, div_nonneg]
+
+open Lean in
+/-- `norm_num` extension for `Nat.ceil` -/
+@[norm_num ⌈_⌉₊]
+def evalNatCeil : NormNumExt where eval {u αZ} e := do
+  match u, αZ, e with
+  | 0, ~q(ℕ), ~q(@Nat.ceil $α $instSemiring $instPartialOrder $instFloorSemiring $x) =>
+    match ← derive x with
+    | .isBool .. => failure
+    | .isNat sα nb pb => do
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) nb q(IsNat.natCeil $x _ $pb)
+    | .isNegNat sα nb pb => do
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) (mkRawNatLit 0) q(IsInt.natCeil _ _ $pb)
+    | .isNNRat _ q n d h => do
+      let instSemifield ← synthInstanceQ q(Semifield $α)
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      have z : Q(ℕ) := mkRawNatLit (⌈q⌉₊)
+      letI : $z =Q ⌈($n / $d : NNRat)⌉₊ := ⟨⟩
+      return .isNat q(inferInstance) z q(IsNNRat.natCeil _ $n $d $h $z rfl)
+    | .isNegNNRat _ q n d h => do
+      let instField ← synthInstanceQ q(Field $α)
+      let instLinearOrder ← synthInstanceQ q(LinearOrder $α)
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) (mkRawNatLit 0) q(IsRat.natCeil _ _ _ $h)
+  | _, _, _ => failure
+
+end Mathlib.Meta.NormNum

Mathlib/Data/Rat/Floor.lean

@@ -283,6 +283,59 @@ def evalIntFract : NormNumExt where eval {u α} e := do
       return .isRat _ (Int.fract q) n' d q(isRat_intFract_of_isRat_negOfNat _ $n $d $h)
   | _, _, _ => failure
 
+/-!
+### `norm_num` extension for `round`
+-/
+
+theorem isNat_round {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
+    (r : R) (m : ℕ) : IsNat r m → IsNat (round r) m := by
+  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩
+
+theorem isInt_round {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
+    (r : R) (m : ℤ) : IsInt r m → IsInt (round r) m := by
+  rintro ⟨⟨⟩⟩; exact ⟨by simp⟩
+
+theorem IsRat.isInt_round {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
+    [FloorRing R] (r : R) (n : ℤ) (d : ℕ) (res : ℤ) (hres : round (n / d : ℚ) = res) :
+    IsRat r n d → IsInt (round r) res := by
+  rintro ⟨inv, rfl⟩
+  subst res
+  constructor
+  rw [invOf_eq_inv, ← div_eq_mul_inv]
+  norm_cast
+
+/-- `norm_num` extension for `round` -/
+@[norm_num round _]
+def evalRound : NormNumExt where eval {u αZ} e := do
+  match u, αZ, e with
+  | 0, ~q(ℤ), ~q(@round $α $instRing $instLinearOrder $instFloorRing $x) =>
+    match ← derive x with
+    | .isBool .. => failure
+    | .isNat sα nb pb => do
+      let instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNat q(inferInstance) nb q(isNat_round $x _ $pb)
+    | .isNegNat sα nb pb => do
+      let _instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      return .isNegNat q(inferInstance) nb q(isInt_round _ _ $pb)
+    | .isNNRat _ q n d h => do
+      let _instField ← synthInstanceQ q(Field $α)
+      let _instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      have z : Q(ℤ) := mkRawIntLit (round q)
+      haveI : $z =Q round (Int.ofNat $n / $d : ℚ) := ⟨⟩
+      return .isInt q(inferInstance) z (round q)
+        q(IsRat.isInt_round $x $n $d $z rfl (IsNNRat.to_isRat $h))
+    | .isNegNNRat _ q n d h => do
+      let _instField ← synthInstanceQ q(Field $α)
+      let _instIsStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
+      assertInstancesCommute
+      have z : Q(ℤ) := mkRawIntLit (round q)
+      haveI : $z =Q round ((Int.negOfNat $n) / $d : ℚ) := ⟨⟩
+      return .isInt q(inferInstance) z (round q) q(IsRat.isInt_round $x (.negOfNat $n) $d $z rfl $h)
+  | _, _, _ => failure
+
 end NormNum
 
 end Rat

Mathlib/Tactic/NormNum/Basic.lean

@@ -81,6 +81,20 @@ theorem isNat_intOfNat : {n n' : ℕ} → IsNat n n' → IsNat (Int.ofNat n) n'
   haveI' x : $e =Q Int.ofNat $n := ⟨⟩
   return .isNat sℤ n' q(isNat_intOfNat $p)
 
+theorem isInt_negOfNat (m n : ℕ) (h : IsNat m n) : IsInt (Int.negOfNat m) (.negOfNat n) :=
+  ⟨congr_arg Int.negOfNat h.1⟩
+
+/-- `norm_num` extension for `Int.negOfNat`.
+
+It's useful for calling `derive` with the numerator of an `.isNegNNRat` branch. -/
+@[norm_num Int.negOfNat _]
+def evalNegOfNat : NormNumExt where eval {u αZ} e := do
+  match u, αZ, e with
+  | 0, ~q(ℤ), ~q(Int.negOfNat $a) =>
+    let ⟨n, pn⟩ ← deriveNat (u := 0) a q(inferInstance)
+    return .isNegNat q(inferInstance) n q(isInt_negOfNat $a $n $pn)
+  | _ => failure
+
 theorem isNat_natAbs_pos : {n : ℤ} → {a : ℕ} → IsNat n a → IsNat n.natAbs a
   | _, _, ⟨rfl⟩ => ⟨rfl⟩
 
@@ -718,5 +732,3 @@ end NormNum
 end Meta
 
 end Mathlib
-
-open Mathlib.Meta.NormNum

MathlibTest/norm_num_ext.lean

@@ -14,6 +14,8 @@ import Mathlib.Tactic.NormNum.NatLog
 import Mathlib.Tactic.NormNum.NatSqrt
 import Mathlib.Tactic.NormNum.Parity
 import Mathlib.Tactic.NormNum.Prime
+import Mathlib.Algebra.Order.Floor.Semifield
+import Mathlib.Data.NNRat.Floor
 import Mathlib.Data.Rat.Floor
 import Mathlib.Tactic.NormNum.LegendreSymbol
 import Mathlib.Tactic.NormNum.Pow
@@ -422,23 +424,59 @@ end big_operators
 
 section floor
 
+section Semiring
+
+variable (R : Type*) [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R]
+
+example : ⌊(2 : R)⌋₊ = 2 := by norm_num1
+example : ⌈(2 : R)⌉₊ = 2 := by norm_num1
+
+end Semiring
+
+section Ring
+
 variable (R : Type*) [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
-variable (K : Type*) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K]
 
-example : ⌊(-1 : R)⌋ = -1 := by norm_num
-example : ⌊(2 : R)⌋ = 2 := by norm_num
-example : ⌊(15 / 16 : K)⌋ + 1 = 1 := by norm_num
-example : ⌊(-15 / 16 : K)⌋ + 1 = 0 := by norm_num
+example : ⌊(-1 : R)⌋ = -1 := by norm_num1
+example : ⌊(2 : R)⌋ = 2 := by norm_num1
+example : ⌈(-1 : R)⌉ = -1 := by norm_num1
+example : ⌈(2 : R)⌉ = 2 := by norm_num1
+example : ⌊(-2 : R)⌋₊ = 0 := by norm_num1
+example : ⌈(-3 : R)⌉₊ = 0 := by norm_num1
+example : round (1 : R) = 1 := by norm_num1
+example : Int.fract (2 : R) = 0 := by norm_num1
+example : round (-3 : R) = -3 := by norm_num1
+example : Int.fract (-3 : R) = 0 := by norm_num1
+
 
-example : ⌈(-1 : R)⌉ = -1 := by norm_num
-example : ⌈(2 : R)⌉ = 2 := by norm_num
-example : ⌈(15 / 16 : K)⌉ + 1 = 2 := by norm_num
-example : ⌈(-15 / 16 : K)⌉ + 1 = 1 := by norm_num
+end Ring
+
+section Semifield
+
+variable (K : Type*) [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K]
+
+example : ⌊(35 / 16 : K)⌋₊ = 2 := by norm_num1
+example : ⌈(35 / 16 : K)⌉₊ = 3 := by norm_num1
+
+end Semifield
+
+section Field
+
+variable (K : Type*) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K]
 
-example : Int.fract (2 : R) = 0 := by norm_num
-example : Int.fract (16 / 15 : K) = 1 / 15 := by norm_num
-example : Int.fract (3.7 : ℚ) = 0.7 := by norm_num
-example : Int.fract (-3.7 : ℚ) = 0.3 := by norm_num
+example : ⌊(15 / 16 : K)⌋ + 1 = 1 := by norm_num1
+example : ⌊(-15 / 16 : K)⌋ + 1 = 0 := by norm_num1
+example : ⌈(15 / 16 : K)⌉ + 1 = 2 := by norm_num1
+example : ⌈(-15 / 16 : K)⌉ + 1 = 1 := by norm_num1
+example : ⌊(-35 / 16 : K)⌋₊ = 0 := by norm_num1
+example : ⌈(-35 / 16 : K)⌉₊ = 0 := by norm_num1
+example : round (-35 / 16 : K) = -2 := by norm_num1
+example : Int.fract (16 / 15 : K) = 1 / 15 := by norm_num1
+example : Int.fract (-35 / 16 : K) = 13 / 16 := by norm_num1
+example : Int.fract (3.7 : ℚ) = 0.7 := by norm_num1
+example : Int.fract (-3.7 : ℚ) = 0.3 := by norm_num1
+
+end Field
 
 end floor