feat: characterize OfScientific.ofScientific on Rat (#990)

leanprover-community · Oct 15, 2024 · 0ccda64 · 0ccda64
1 parent ad3ba5f
commit 0ccda64
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/Batteries/Data/Rat/Basic.lean b/Batteries/Data/Rat/Basic.lean
@@ -112,7 +112,8 @@ def divInt : Int → Int → Rat
   else
     (m * 10 ^ e : Nat)
 
-instance : OfScientific Rat where ofScientific := Rat.ofScientific
+instance : OfScientific Rat where
+  ofScientific m s e := Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e)
 
 /-- Rational number strictly less than relation, as a `Bool`. -/
 protected def blt (a b : Rat) : Bool :=

diff --git a/Batteries/Data/Rat/Lemmas.lean b/Batteries/Data/Rat/Lemmas.lean
@@ -332,6 +332,12 @@ theorem ofScientific_def : Rat.ofScientific m s e =
     if s then mkRat m (10 ^ e) else (m * 10 ^ e : Nat) := by
   cases s; exact ofScientific_false_def; exact ofScientific_true_def
 
+/-- `Rat.ofScientific` applied to numeric literals is the same as a scientific literal. -/
+@[simp]
+theorem ofScientific_ofNat_ofNat :
+    Rat.ofScientific (no_index (OfNat.ofNat m)) s (no_index (OfNat.ofNat e))
+      = OfScientific.ofScientific m s e := rfl
+
 @[simp] theorem intCast_den (a : Int) : (a : Rat).den = 1 := rfl
 
 @[simp] theorem intCast_num (a : Int) : (a : Rat).num = a := rfl