From 2f3211028bbff5576518c52259dcfaf82fe99cb5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Oct 2025 19:05:26 -0700 Subject: [PATCH] feat: support for `Rat` scientific literals (#10961) This PR adds support for scientific literals for `Rat` in `grind`. `grind` does not yet add support for this kind of literal in arbitrary fields. closes #10489 --- src/Init/Data/Rat/Lemmas.lean | 8 ++++- src/Init/Grind/Norm.lean | 7 +++-- src/Lean/Meta/LitValues.lean | 24 +++++++++++--- src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean | 13 ++++++++ src/Lean/ToExpr.lean | 24 ++++++++++++-- tests/lean/run/grind_10489.lean | 10 ++++++ tests/lean/run/toExpr.lean | 31 ++++++++++++++++++- 7 files changed, 105 insertions(+), 12 deletions(-) create mode 100644 tests/lean/run/grind_10489.lean diff --git a/src/Init/Data/Rat/Lemmas.lean b/src/Init/Data/Rat/Lemmas.lean index 6daa36d63e..bd9ce08841 100644 --- a/src/Init/Data/Rat/Lemmas.lean +++ b/src/Init/Data/Rat/Lemmas.lean @@ -1011,7 +1011,6 @@ theorem intCast_neg_iff {a : Int} : /-- Alternative statement of `ofScientific_def`. -/ -@[grind =] theorem ofScientific_def' : (OfScientific.ofScientific m s e : Rat) = m * (10 ^ (if s then -e else e : Int)) := by change Rat.ofScientific _ _ _ = _ @@ -1023,6 +1022,13 @@ theorem ofScientific_def' : · push_cast rfl +theorem ofScientific_def_eq_if : + (OfScientific.ofScientific m s e : Rat) = if s then (m : Rat) / (10 : Rat) ^ e else (m : Rat) * (10 : Rat) ^ e := by + simp [ofScientific_def'] + split + next => rw [Rat.zpow_neg, ← Rat.div_def, Rat.zpow_natCast] + next => rw [Rat.zpow_natCast] + /-! # min and max -/ diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index ac42f8eed3..f91175db42 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Init.Data.Int.Linear public import Init.Grind.Ring.Field - +public import Init.Data.Rat.Lemmas public section namespace Lean.Grind @@ -153,7 +152,7 @@ init_grind_norm /- Pre theorems -/ | /- Post theorems -/ - iff_eq heq_eq_eq + iff_eq heq_eq_eq eq_self -- And and_true true_and and_false false_and and_assoc -- ite @@ -208,5 +207,7 @@ init_grind_norm Ring.intCast_mul Ring.intCast_pow Ring.intCast_sub + -- Rationals + Rat.ofScientific_def_eq_if Rat.zpow_neg end Lean.Grind diff --git a/src/Lean/Meta/LitValues.lean b/src/Lean/Meta/LitValues.lean index ce712422f7..33f2167d58 100644 --- a/src/Lean/Meta/LitValues.lean +++ b/src/Lean/Meta/LitValues.lean @@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.Meta.Basic - +public import Init.Data.Rat.Basic public section - namespace Lean.Meta - /-! Helper functions for recognizing builtin literal values. This module focus on recognizing the standard representation used in Lean for these literals. @@ -53,6 +50,25 @@ def getIntValue? (e : Expr) : MetaM (Option Int) := do let some (n, _) ← getOfNatValue? a ``Int | return none return some (-↑n) +/-- +Return `some i` if `e` `OfNat.ofNat`-application encoding a rational, or `Neg.neg`-application of one, +or a division. +-/ +def getRatValue? (e : Expr) : MetaM (Option Rat) := do + match_expr e with + | HDiv.hDiv _ _ _ _ a b => + let some n ← getRatValueNum? a | return none + let some (d, _) ← getOfNatValue? b ``Rat | return none + return some (n / (d : Rat)) + | _ => getRatValueNum? e +where + getRatValueNum? (e : Expr) : MetaM (Option Rat) := do + if let some (n, _) ← getOfNatValue? e ``Rat then + return some (n : Rat) + let_expr Neg.neg _ _ a ← e | return none + let some (n, _) ← getOfNatValue? a ``Rat | return none + return some (- (n : Rat)) + /-- Return `some c` if `e` is a `Char.ofNat`-application that encodes the character `c`. -/ def getCharValue? (e : Expr) : MetaM (Option Char) := do let_expr Char.ofNat n ← e | return none diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean index 3547bf11f9..01ccb24212 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean @@ -168,6 +168,18 @@ builtin_simproc_decl normIntCastNum (IntCast.intCast _) := fun e => do let h := mkApp4 (mkConst ``Grind.Ring.intCast_eq_ofNat_of_nonneg us) α ringInst a eagerReflBoolTrue return .done { expr := n, proof? := some h } +builtin_dsimproc [simp, seval] normPowRatInt ((_ : Rat) ^ (_ : Int)) := fun e => do + let_expr HPow.hPow _ _ _ _ a b ← e | return .continue + let some v₁ ← getRatValue? a | return .continue + let some v₂ ← getIntValue? b | return .continue + let warning := (← Simp.getConfig).warnExponents + unless (← checkExponent v₂.natAbs (warning := warning)) do return .continue + if v₂ < 0 then + -- **Note**: we use `Rat.zpow_neg` as a normalization rule + return .continue + else + return .done <| toExpr (v₁ ^ v₂) + /-! Add additional arithmetic simprocs -/ @@ -193,6 +205,7 @@ def addSimproc (s : Simprocs) : CoreM Simprocs := do let s ← s.add ``normIntOfNatInst (post := false) let s ← s.add ``normNatCastNum (post := false) let s ← s.add ``normIntCastNum (post := false) + let s ← s.add ``normPowRatInt (post := false) return s end Lean.Meta.Grind.Arith diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean index 7b1df26aa9..6c461d4e84 100644 --- a/src/Lean/ToExpr.lean +++ b/src/Lean/ToExpr.lean @@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ module - prelude public import Lean.ToLevel - +public import Init.Data.Rat.Basic public section universe u - namespace Lean /-- @@ -51,6 +49,26 @@ where mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r (.app (.const ``instOfNat []) r) +instance : ToExpr Rat where + toTypeExpr := .const ``Rat [] + toExpr i := if i.den == 1 then + mkInt i.num + else + mkApp6 (.const ``HDiv.hDiv [0, 0, 0]) (.const ``Rat []) (.const ``Rat []) (.const ``Rat []) + (mkApp2 (.const ``instHDiv [0]) (.const ``Rat []) (.const ``Rat.instDiv [])) + (mkInt i.num) (mkInt i.den) +where + mkInt (i : Int) : Expr := + if 0 ≤ i then + mkNat i.toNat + else + mkApp3 (.const ``Neg.neg [0]) (.const ``Rat []) (.const ``Rat.instNeg []) + (mkNat (-i).toNat) + mkNat (n : Nat) : Expr := + let r := mkRawNatLit n + mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Rat []) r + (.app (.const ``Rat.instOfNat []) r) + instance : ToExpr (Fin n) where toTypeExpr := .app (mkConst ``Fin) (toExpr n) toExpr a := diff --git a/tests/lean/run/grind_10489.lean b/tests/lean/run/grind_10489.lean new file mode 100644 index 0000000000..3fb404135c --- /dev/null +++ b/tests/lean/run/grind_10489.lean @@ -0,0 +1,10 @@ +example : (2 / 3 : Rat) ≤ (0.67 : Rat) := by grind +example : (1.2 : Rat) ≤ (1.21 : Rat) := by grind +example : (2 / 3 : Rat) ≤ (67 / 100 : Rat) := by grind +example : (2 / 3 : Rat) ≤ (67 * 10 ^ (-2) : Rat) := by grind +example : (2 / 3 : Rat) ≤ (67 / 10 ^ 2 : Rat) := by grind +example : (2 / 3 : Rat) ≤ (67 / 10 ^ (2:Int) : Rat) := by grind +example : (1.2345 : Rat) ≤ (1.2346 : Rat) := by grind +example : (1.2345 : Rat) ≤ (1.234501 : Rat) := by grind +example : (2.3 : Rat) ≤ (4.5 : Rat) := by grind +example : (2.3 : Rat) ≤ (5/2 : Rat) := by grind diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean index 6131320902..1bfad22afd 100644 --- a/tests/lean/run/toExpr.lean +++ b/tests/lean/run/toExpr.lean @@ -3,7 +3,6 @@ import Lean open Lean unsafe def test {α : Type} [ToString α] [ToExpr α] [BEq α] (a : α) : CoreM Unit := do -let env ← getEnv; let auxName := `_toExpr._test; let decl := Declaration.defnDecl { name := auxName, @@ -30,3 +29,33 @@ match newEnv.evalConst α {} auxName with #eval test ['a', 'b', 'c'] #eval test ("hello", true) #eval test ((), 10) +#eval test (1:Rat) +#eval test (-1:Rat) +#eval test (2:Rat) +#eval test (-2:Rat) +#eval test (1/(-2):Rat) +#eval test (-2/3:Rat) +#eval test (-2/1:Rat) +#eval test (-20/3:Rat) +#eval test (-1.234:Rat) +#eval test (0.67:Rat) + +open Lean Meta +def testRat (n : Rat) : MetaM Unit := do + let e := toExpr n + IO.println e + let some n' ← getRatValue? e | throwError "`Rat` expected{indentExpr e}" + IO.println n' + assert! n == n' + +#eval testRat 0 +#eval testRat 1 +#eval testRat (1/2) +#eval testRat (1/(-2)) +#eval testRat (2/3) +#eval testRat (0.67) +#eval testRat (1.67) +#eval testRat (1.68) +#eval testRat (-1.67) +#eval testRat (-2) +#eval testRat (-0.67)