[Merged by Bors] - feat: recognize scientific notation in norm_num

Mathlib/Algebra/Field/Defs.lean

@@ -174,6 +174,23 @@ end Rat
 
 end DivisionRing
 
+section OfScientific
+
+instance DivisionRing.toOfScientific [DivisionRing K] : OfScientific K where
+  ofScientific (m : ℕ) (b : Bool) (d : ℕ) := Rat.ofScientific m b d
+
+/-- A class which states that an `OfScientific α` instance is propositionally equal to the cast of
+the canonical `OfScientific Rat` instance, assuming we have `RatCast α`. -/
+class LawfulOfScientific (α) [OfScientific α] [RatCast α] : Prop where
+  /-- However `ofScientific` is defined, it's pointwise equal to the cast of `Rat.ofScientific`. -/
+  ofScientific_eq (m : ℕ) (b : Bool) (d : ℕ) :
+      OfScientific.ofScientific m b d = (Rat.ofScientific m b d : α)
+
+instance [DivisionRing α] : LawfulOfScientific α  where
+  ofScientific_eq _ _ _ := rfl
+
+end OfScientific
+
 section Field
 
 variable [Field K]

Mathlib/Algebra/Invertible.lean

@@ -81,31 +81,49 @@ prefix:max
   Invertible.invOf
 
 @[simp]
+theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟ a * a = 1 :=
+  Invertible.invOf_mul_self
+
 theorem invOf_mul_self [Mul α] [One α] (a : α) [Invertible a] : ⅟ a * a = 1 :=
   Invertible.invOf_mul_self
 #align inv_of_mul_self invOf_mul_self
 
 @[simp]
+theorem mul_invOf_self' [Mul α] [One α] (a : α) {_ : Invertible a} : a * ⅟ a = 1 :=
+  Invertible.mul_invOf_self
+
 theorem mul_invOf_self [Mul α] [One α] (a : α) [Invertible a] : a * ⅟ a = 1 :=
   Invertible.mul_invOf_self
 #align mul_inv_of_self mul_invOf_self
 
 @[simp]
+theorem invOf_mul_self_assoc' [Monoid α] (a b : α) {_ : Invertible a} : ⅟ a * (a * b) = b := by
+  rw [← mul_assoc, invOf_mul_self, one_mul]
+
 theorem invOf_mul_self_assoc [Monoid α] (a b : α) [Invertible a] : ⅟ a * (a * b) = b := by
   rw [← mul_assoc, invOf_mul_self, one_mul]
 #align inv_of_mul_self_assoc invOf_mul_self_assoc
 
 @[simp]
+theorem mul_invOf_self_assoc' [Monoid α] (a b : α) {_ : Invertible a} : a * (⅟ a * b) = b := by
+  rw [← mul_assoc, mul_invOf_self, one_mul]
+
 theorem mul_invOf_self_assoc [Monoid α] (a b : α) [Invertible a] : a * (⅟ a * b) = b := by
   rw [← mul_assoc, mul_invOf_self, one_mul]
 #align mul_inv_of_self_assoc mul_invOf_self_assoc
 
 @[simp]
+theorem mul_invOf_mul_self_cancel' [Monoid α] (a b : α) {_ : Invertible b} : a * ⅟ b * b = a := by
+  simp [mul_assoc]
+
 theorem mul_invOf_mul_self_cancel [Monoid α] (a b : α) [Invertible b] : a * ⅟ b * b = a := by
   simp [mul_assoc]
 #align mul_inv_of_mul_self_cancel mul_invOf_mul_self_cancel
 
 @[simp]
+theorem mul_mul_invOf_self_cancel' [Monoid α] (a b : α) {_ : Invertible b} : a * b * ⅟ b = a := by
+  simp [mul_assoc]
+
 theorem mul_mul_invOf_self_cancel [Monoid α] (a b : α) [Invertible b] : a * b * ⅟ b = a := by
   simp [mul_assoc]
 #align mul_mul_inv_of_self_cancel mul_mul_invOf_self_cancel

Mathlib/Data/Rat/Cast.lean

@@ -536,3 +536,10 @@ instance isScalarTower_right : IsScalarTower ℚ K K :=
 end Rat
 
 end SMul
+
+section OfScientific
+
+instance : LawfulOfScientific Rat where
+  ofScientific_eq _ _ _ := rfl
+
+end OfScientific

Mathlib/Data/Rat/Defs.lean

@@ -251,6 +251,15 @@ theorem divInt_neg_one_one : -1 /. 1 = -1 :=
     rfl
 #align rat.mk_neg_one_one Rat.divInt_neg_one_one
 
+theorem divInt_one (n : ℤ) : n /. 1 = n :=
+  show divInt _ _ = _ by
+    rw [divInt]
+    simp [mkRat, normalize]
+    rfl
+
+theorem mkRat_one {n : ℤ} : mkRat n 1 = n := by
+  simp [Rat.mkRat_eq, Rat.divInt_one]
+
 #align rat.mul_one Rat.mul_one
 #align rat.one_mul Rat.one_mul
 #align rat.mul_comm Rat.mul_comm
@@ -541,6 +550,17 @@ theorem coe_int_inj (m n : ℤ) : (m : ℚ) = n ↔ m = n :=
 
 end Casts
 
+theorem mkRat_eq_div {n : ℤ} {d : ℕ} : mkRat n d = n / d := by
+  simp [mkRat]
+  by_cases d = 0
+  · simp [h]
+  · simp [h, HDiv.hDiv, Rat.div, Div.div]
+    unfold Rat.inv
+    have h₁ : 0 < d := Nat.pos_iff_ne_zero.2 h
+    have h₂ : ¬ (d : ℤ) < 0 := by simp
+    simp [h, h₁, h₂, ←Rat.normalize_eq_mk', Rat.normalize_eq_mkRat, ← mkRat_one,
+      Rat.mkRat_mul_mkRat]
+
 end Rat
 
 -- Porting note: `assert_not_exists` is not implemented yet.

Mathlib/Tactic/NormNum/Basic.lean

@@ -15,12 +15,14 @@ This file adds `norm_num` plugins for `+`, `*` and `^` along with other basic op
 -/
 
 namespace Mathlib
-open Lean hiding Rat
+open Lean hiding Rat mkRat
 open Meta
 
 namespace Meta.NormNum
 open Qq
 
+/-! # Constructors and constants -/
+
 theorem isNat_zero (α) [AddMonoidWithOne α] : IsNat (Zero.zero : α) (nat_lit 0) :=
   ⟨Nat.cast_zero.symm⟩
 
@@ -52,6 +54,21 @@ theorem isNat_ofNat (α : Type u_1) [AddMonoidWithOne α] {a : α} {n : ℕ}
     guard <|← isDefEq a e
     return .isNat sα n (q(isNat_ofNat $α $pa) : Expr)
 
+theorem isNat_intOfNat : {n n' : ℕ} → IsNat n n' → IsNat (Int.ofNat n) n'
+  | _, _, ⟨rfl⟩ => ⟨rfl⟩
+
+/-- The `norm_num` extension which identifies the constructor application `Int.ofNat n` such that
+`norm_num` successfully recognizes `n`, returning `n`. -/
+@[norm_num Int.ofNat _] def evalIntOfNat : NormNumExt where eval {u α} e := do
+  let .app _ (n : Q(ℕ)) ← whnfR e | failure
+  guard <| α.isConstOf ``Int
+  let sℕ : Q(AddMonoidWithOne ℕ) := q(AddCommMonoidWithOne.toAddMonoidWithOne)
+  let sℤ : Q(AddMonoidWithOne ℤ) := q(AddGroupWithOne.toAddMonoidWithOne)
+  let ⟨n', p⟩ ← deriveNat n sℕ
+  return (.isNat sℤ n' q(isNat_intOfNat $p) : Result q(Int.ofNat $n))
+
+/-! # Casts -/
+
 theorem isNat_cast {R} [AddMonoidWithOne R] (n m : ℕ) :
     IsNat n m → IsNat (n : R) m := by rintro ⟨⟨⟩⟩; exact ⟨rfl⟩
 
@@ -85,6 +102,43 @@ theorem isInt_cast {R} [Ring R] (n m : ℤ) :
       return (.isNegNat rα na q(isInt_cast $a (.negOfNat $na) $pa) : Result q(Int.cast $a : $α))
     | _ => failure
 
+theorem isNat_ratCast [DivisionRing R] : {q : ℚ} → {n : ℕ} →
+    IsNat q n → IsNat (q : R) n
+  | _, _, ⟨rfl⟩ => ⟨by simp⟩
+
+theorem isInt_ratCast [DivisionRing R] : {q : ℚ} → {n : ℤ} →
+    IsInt q n → IsInt (q : R) n
+  | _, _, ⟨rfl⟩ => ⟨by simp⟩
+
+theorem isRat_ratCast [DivisionRing R] [CharZero R] : {q : ℚ} → {n : ℤ} → {d : ℕ} →
+    IsRat q n d → IsRat (q : R) n d
+  | _, _, _, ⟨⟨qi,_,_⟩, rfl⟩ => ⟨⟨qi, by norm_cast, by norm_cast⟩, by simp only []; norm_cast⟩
+
+/-- The `norm_num` extension which identifies an expression `RatCast.ratCast q` where `norm_num`
+recognizes `q`, returning the cast of `q`. -/
+@[norm_num RatCast.ratCast _] def evalRatCast : NormNumExt where eval {u α} e := do
+  let dα ← inferDivisionRing α
+  match e with
+  | ~q(RatCast.ratCast $a) =>
+    let r ← derive (α := q(ℚ)) a
+    match r with
+    | .isNat _ na pa =>
+      let sα : Q(AddMonoidWithOne $α) := q(instAddMonoidWithOne')
+      let pa : Q(@IsNat _ instAddMonoidWithOne' $a $na) := pa
+      return (.isNat sα na q(@isNat_ratCast $α _ $a $na $pa) : Result q(RatCast.ratCast $a : $α))
+    | .isNegNat _ na pa =>
+      let rα : Q(Ring $α) := q(instRing)
+      let pa : Q(@IsInt _ instRing $a (.negOfNat $na)) := pa
+      return (.isNegNat rα na q(@isInt_ratCast $α _ $a (.negOfNat $na) $pa) :
+          Result q(RatCast.ratCast $a : $α))
+    | .isRat _ qa na da pa =>
+      let i ← inferCharZeroOfDivisionRing dα
+      let pa : Q(@IsRat _ instRingRat $a $na $da) := pa
+      return (.isRat dα qa na da q(isRat_ratCast $pa) : Result q(RatCast.ratCast $a : $α))
+    | _ => failure
+
+/-! # Arithmetic -/
+
 theorem isNat_add {α} [AddMonoidWithOne α] : {a b : α} → {a' b' c : ℕ} →
     IsNat a a' → IsNat b b' → Nat.add a' b' = c → IsNat (a + b) c
   | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨(Nat.cast_add _ _).symm⟩
@@ -424,33 +478,33 @@ such that `norm_num` successfully recognises `a`. -/
     let ⟨qa, na, da, pa⟩ ← ra.toRat'
     let qb := qa⁻¹
     if qa > 0 then
-      if let .some _i := _i then
+      if let some _i := _i then
         have lit : Q(ℕ) := na.appArg!
         have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
-        let pa : Q(IsRat «$a» (Int.ofNat (Nat.succ $lit2)) $da) := pa
+        let pa : Q(IsRat $a (Int.ofNat (Nat.succ $lit2)) $da) := pa
         return (.isRat' dα qb q(.ofNat $da) lit
           (q(isRat_inv_pos (α := $α) $pa) : Expr) : Result q($a⁻¹))
       else
         guard (qa = 1)
-        let .isNat inst _z
+        let .isNat inst n
           (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 1))) := ra | failure
-        return (.isNat inst _z (q(isRat_inv_one $pa) : Expr) : Result q($a⁻¹))
+        return (.isNat inst n (q(isRat_inv_one $pa) : Expr) : Result q($a⁻¹))
     else if qa < 0 then
-      if let .some _i := _i then
+      if let some _i := _i then
         have lit : Q(ℕ) := na.appArg!
         have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
-        let pa : Q(IsRat «$a» (Int.negOfNat (Nat.succ $lit2)) $da) := pa
+        let pa : Q(IsRat $a (Int.negOfNat (Nat.succ $lit2)) $da) := pa
         return (.isRat' dα qb q(.negOfNat $da) lit
           (q(isRat_inv_neg (α := $α) $pa) : Expr) : Result q($a⁻¹))
       else
         guard (qa = -1)
-        let .isNegNat inst _z
+        let .isNegNat inst n
           (pa : Q(@IsInt _ DivisionRing.toRing $a (.negOfNat 1))) := ra | failure
-        return (.isNegNat inst _z (q(isRat_inv_neg_one $pa) : Expr) : Result q($a⁻¹))
+        return (.isNegNat inst n (q(isRat_inv_neg_one $pa) : Expr) : Result q($a⁻¹))
     else
-      let .isNat inst _z (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 0))) := ra
+      let .isNat inst n (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 0))) := ra
         | failure
-      return (.isNat inst _z (q(isRat_inv_zero $pa) : Expr) : Result q($a⁻¹))
+      return (.isNat inst n (q(isRat_inv_zero $pa) : Expr) : Result q($a⁻¹))
   core
 
 theorem isRat_div [DivisionRing α] : {a b : α} → {cn : ℤ} → {cd : ℕ} → IsRat (a * b⁻¹) cn cd →
@@ -468,6 +522,73 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
   let pa : Q(IsRat ($a * $b⁻¹) $na $da) := pa
   return (.isRat' dα qa na da q(isRat_div $pa) : Result q($a / $b))
 
+/-! # Constructor-like operations -/
+
+theorem isRat_mkRat : {a na n : ℤ} → {b nb d : ℕ} → IsInt a na → IsNat b nb →
+    IsRat (na / nb : ℚ) n d → IsRat (mkRat a b) n d
+  | _, _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, ⟨_, h⟩ => by rw [Rat.mkRat_eq_div]; exact ⟨_, h⟩
+
+/-- The `norm_num` extension which identifies expressions of the form `mkRat a b`,
+such that `norm_num` successfully recognises both `a` and `b`, and returns `a / b`. -/
+@[norm_num mkRat _ _] def evalMkRat : NormNumExt where eval {u α} e := do
+  let .app (.app _ (a : Q(ℤ))) (b : Q(ℕ)) ← whnfR e | failure
+  guard <| α.isConstOf ``Rat
+  let ra ← derive a
+  let rℤ : Q(Ring ℤ) := q(Int.instRingInt)
+  let some ⟨_, na, pa⟩ := ra.toInt | failure
+  let sℕ : Q(AddMonoidWithOne ℕ) := q(AddCommMonoidWithOne.toAddMonoidWithOne)
+  let ⟨nb, pb⟩ ← deriveNat b sℕ
+  let rab ← derive (q($na / $nb) : Q(Rat))
+  let dℚ : Q(DivisionRing ℚ) := q(Rat.divisionRing)
+  let ⟨q, n, d, p⟩ ← rab.toRat' dℚ
+  let p : Q(IsRat ($na / $nb : ℚ) $n $d) := p
+  return (.isRat' (inst := dℚ) q n d q(isRat_mkRat $pa $pb $p) : Result q(mkRat $a $b))
+
+theorem isRat_ofScientific_of_true [DivisionRing α] [OfScientific α] [LawfulOfScientific α] :
+    {m e : ℕ} → {n : ℤ} → {d : ℕ} → IsRat (mkRat m (10 ^ e) : α) n d →
+    IsRat (OfScientific.ofScientific (α := α) m true e) n d
+  | _, _, _, _, ⟨_, eq⟩ => ⟨_, by
+    simp only [LawfulOfScientific.ofScientific_eq, if_true, Rat.ofScientific,
+      Rat.normalize_eq_mkRat]
+    exact eq⟩
+
+theorem isNat_ofScientific_of_false [dα : DivisionRing α] [OfScientific α] [LawfulOfScientific α] :
+    {m e nm ne n : ℕ} → IsNat m nm → IsNat e ne → n = Nat.mul nm ((10 : ℕ) ^ ne) →
+    IsNat (OfScientific.ofScientific (α := α) m false e) n
+  | _, _, _, _, _, ⟨rfl⟩, ⟨rfl⟩, h =>
+    ⟨by simp [LawfulOfScientific.ofScientific_eq, Rat.ofScientific, h]; norm_cast⟩
+
+/-- The `norm_num` extension which identifies expressions in scientific notation, normalizing them
+to rat casts if the scientific notation is inherited from the one for rationals. -/
+@[norm_num OfScientific.ofScientific _ _ _] def evalOfScientific :
+    NormNumExt where eval {u α} e := do
+  let .app (.app (.app f (m : Q(ℕ))) (b : Q(Bool))) (exp : Q(ℕ)) ← whnfR e | failure
+  let σα ← inferOfScientific α
+  guard <|← withNewMCtxDepth <| isDefEq f q(OfScientific.ofScientific (α := $α))
+  let dα ← inferDivisionRing α
+  let lσα ← inferLawfulOfScientific dα σα
+  match b with
+  | ~q(true)  =>
+    let rme ← derive (q(mkRat $m (10 ^ $exp)) : Q($α))
+    let some ⟨q, n, d, p⟩ := rme.toRat' | failure
+    let p : Q(IsRat (mkRat $m (10 ^ $exp) : $α) $n $d) := p
+    return (.isRat' dα q n d q(isRat_ofScientific_of_true $p) :
+        Result q(@OfScientific.ofScientific $α $σα $m true $exp))
+  | ~q(false) =>
+    let ⟨nm, pm⟩ ← deriveNat m q(AddCommMonoidWithOne.toAddMonoidWithOne)
+    let ⟨ne, pe⟩ ← deriveNat exp q(AddCommMonoidWithOne.toAddMonoidWithOne)
+    have pm : Q(IsNat $m $nm) := pm
+    have pe : Q(IsNat $exp $ne) := pe
+    let m' := m.natLit!
+    let exp' := exp.natLit!
+    let n' := Nat.mul m' (Nat.pow (10 : ℕ) exp')
+    have n : Q(ℕ) := mkRawNatLit n'
+    have r : Q($n = Nat.mul $nm ((10 : ℕ) ^ $ne)) := (q(Eq.refl $n) : Expr)
+    return ((.isNat _ n
+        (q(isNat_ofScientific_of_false (α := $α) (n := $n) $pm $pe $r) :
+            Q(IsNat (OfScientific.ofScientific (α := $α) $m false $exp) $n))) :
+          Result q(@OfScientific.ofScientific $α $σα $m false $exp))
+
 /-! # Logic -/
 
 /-- The `norm_num` extension which identifies `True`. -/
@@ -607,7 +728,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
     if za = zb then
       let pb : Q(IsInt $b $na) := pb
       return (.isTrue q(isInt_eq_true $pa $pb) : Result q($a = $b))
-    else if let .some _i ← inferCharZeroOfRing? rα then
+    else if let some _i ← inferCharZeroOfRing? rα then
       let r : Q(decide ($na = $nb) = false) := (q(Eq.refl false) : Expr)
       return (.isFalse q(isInt_eq_false $pa $pb $r) : Result q($a = $b))
     else
@@ -617,7 +738,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
     if qa = qb then
       let pb : Q(IsRat $b $na $da) := pb
       return (.isTrue q(isRat_eq_true $pa $pb) : Result q($a = $b))
-    else if let .some _i ← inferCharZeroOfDivisionRing? dα then
+    else if let some _i ← inferCharZeroOfDivisionRing? dα then
       let r : Q(decide (Int.mul $na (.ofNat $db) = Int.mul $nb (.ofNat $da)) = false) :=
         (q(Eq.refl false) : Expr)
       return (.isFalse q(isRat_eq_false $pa $pb $r) : Result q($a = $b))
@@ -643,7 +764,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
     if na.natLit!.beq nb.natLit! then
       let r : Q(Nat.beq $na $nb = true) := (q(Eq.refl true) : Expr)
       return (.isTrue q(isNat_eq_true $pa $pb $r) : Result q($a = $b))
-    else if let .some _i ← inferCharZeroOfAddMonoidWithOne? mα then
+    else if let some _i ← inferCharZeroOfAddMonoidWithOne? mα then
       let r : Q(Nat.beq $na $nb = false) := (q(Eq.refl false) : Expr)
       return (.isFalse q(isNat_eq_false $pa $pb $r) : Result q($a = $b))
     else

Mathlib/Tactic/NormNum/Core.lean

@@ -214,6 +214,13 @@ and `q` is the value of `n / d`. -/
 /-- A shortcut (non)instance for `AddMonoidWithOne α` from `Ring α` to shrink generated proofs. -/
 def instAddMonoidWithOne [Ring α] : AddMonoidWithOne α := inferInstance
 
+/-- A shortcut (non)instance for `AddMonoidWithOne α` from `DivisionRing α` to shrink generated
+proofs. -/
+def instAddMonoidWithOne' [DivisionRing α] : AddMonoidWithOne α := inferInstance
+
+/-- A shortcut (non)instance for `Ring α` from `DivisionRing α` to shrink generated proofs. -/
+def instRing [DivisionRing α] : Ring α := inferInstance
+
 /-- The result is `z : ℤ` and `proof : isNat x z`. -/
 -- Note the independent arguments `z : Q(ℤ)` and `n : ℤ`.
 -- We ensure these are "the same" when calling.
@@ -306,6 +313,23 @@ exists. -/
 def inferCharZeroOfDivisionRing? {α : Q(Type u)}
     (_i : Q(DivisionRing $α) := by with_reducible assumption) : MetaM (Option Q(CharZero $α)) :=
   return (← trySynthInstanceQ (q(CharZero $α) : Q(Prop))).toOption
+
+/-- Helper function to synthesize a typed `OfScientific α` expression. -/
+def inferOfScientific (α : Q(Type u)) : MetaM Q(OfScientific $α) :=
+  return ← synthInstanceQ (q(OfScientific $α) : Q(Type u)) <|>
+    throwError "does not support scientific notation"
+
+/-- Helper function to synthesize a typed `LawfulOfScientific α` expression. -/
+def inferLawfulOfScientific {α : Q(Type u)}
+    (_dα : Q(DivisionRing $α) := by with_reducible assumption)
+    (_sα : Q(OfScientific $α) := by with_reducible assumption) : MetaM Q(LawfulOfScientific $α) :=
+  return ← synthInstanceQ (q(LawfulOfScientific $α) : Q(Prop)) <|>
+    throwError "does not support lawful scientific notation"
+
+/-- Helper function to synthesize a typed `RatCast α` expression. -/
+def inferRatCast (α : Q(Type u)) : MetaM Q(RatCast $α) :=
+  return ← synthInstanceQ (q(RatCast $α) : Q(Type u)) <|> throwError "does not support a rat cast"
+
 /--
 Extract from a `Result` the integer value (as both a term and an expression),
 and the proof that the original expression is equal to this integer.