From b76bf446546de558e77e6db2adfc4c1b5645ffd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2025 00:01:19 -0700 Subject: [PATCH] feat: infrastructure for cutsat generic `ToInt` (#9008) This PR implements the basic infrastructure for the generic `ToInt` support in `cutsat`. --- src/Init/Grind.lean | 1 + src/Init/Grind/ToInt.lean | 5 + src/Init/Grind/ToIntLemmas.lean | 96 ++++++++ src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean | 1 + .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 14 +- .../Tactic/Grind/Arith/Cutsat/Search.lean | 10 +- .../Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean | 210 ++++++++++++++++++ .../Tactic/Grind/Arith/Cutsat/ToIntInfo.lean | 39 ++++ .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 7 +- 9 files changed, 371 insertions(+), 12 deletions(-) create mode 100644 src/Init/Grind/ToIntLemmas.lean create mode 100644 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean create mode 100644 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean diff --git a/src/Init/Grind.lean b/src/Init/Grind.lean index 57974f516e..02dd3b87bc 100644 --- a/src/Init/Grind.lean +++ b/src/Init/Grind.lean @@ -19,4 +19,5 @@ import Init.Grind.Module import Init.Grind.Ordered import Init.Grind.Ext import Init.Grind.ToInt +import Init.Grind.ToIntLemmas import Init.Data.Int.OfNat -- This may not have otherwise been imported, breaking `grind` proofs. diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean index f83ef1d800..be64922da4 100644 --- a/src/Init/Grind/ToInt.lean +++ b/src/Init/Grind/ToInt.lean @@ -35,6 +35,11 @@ inductive IntInterval : Type where io (hi : Int) | /-- The infinite interval `(-∞, ∞)`. -/ ii + deriving BEq, DecidableEq + +instance : LawfulBEq IntInterval where + rfl := by intro a; cases a <;> simp_all! [BEq.beq] + eq_of_beq := by intro a b; cases a <;> cases b <;> simp_all! [BEq.beq] namespace IntInterval diff --git a/src/Init/Grind/ToIntLemmas.lean b/src/Init/Grind/ToIntLemmas.lean new file mode 100644 index 0000000000..fea63c6031 --- /dev/null +++ b/src/Init/Grind/ToIntLemmas.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +module + +prelude +import all Init.Grind.ToInt + +namespace Lean.Grind.ToInt + +/-! Wrap -/ + +theorem of_eq_wrap_co_0 (i : IntInterval) (hi : Int) (h : i == .co 0 hi) {a b : Int} : a = i.wrap b → a = b % hi := by + revert h + cases i <;> simp + intro h₁ h₂; subst h₁ h₂; simp + +/-! Asserted propositions -/ + +theorem of_eq {α i} [ToInt α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : a = b → a' = b' := by + intro h; replace h := congrArg toInt h + rw [h₁, h₂] at h; assumption + +theorem of_diseq {α i} [ToInt α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : a ≠ b → a' ≠ b' := by + intro hne h; rw [← h₁, ← h₂] at h + replace h := ToInt.toInt_inj _ _ h; contradiction + +theorem of_le {α i} [ToInt α i] [_root_.LE α] [ToInt.LE α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : a ≤ b → a' ≤ b' := by + intro h; replace h := ToInt.LE.le_iff _ _ |>.mp h + rw [h₁, h₂] at h; assumption + +theorem of_not_le {α i} [ToInt α i] [_root_.LE α] [ToInt.LE α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : ¬ (a ≤ b) → b' + 1 ≤ a' := by + intro h; have h' := ToInt.LE.le_iff a b + simp [h, h₁, h₂] at h'; exact h' + +theorem of_lt {α i} [ToInt α i] [_root_.LT α] [ToInt.LT α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : a < b → a' + 1 ≤ b' := by + intro h; replace h := ToInt.LT.lt_iff _ _ |>.mp h + rw [h₁, h₂] at h; assumption + +theorem of_not_lt {α i} [ToInt α i] [_root_.LT α] [ToInt.LT α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : ¬ (a < b) → b' ≤ a' := by + intro h; have h' := ToInt.LT.lt_iff a b + simp [h, h₁, h₂] at h'; assumption + +/-! Addition -/ + +theorem add_congr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : toInt (a + b) = i.wrap (a' + b') := by + rw [ToInt.Add.toInt_add, h₁, h₂] + +theorem add_congr.ww {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) {a b : α} {a' b' : Int} + (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by + rw [add_congr h₁ h₂, ← i.wrap_add h] + +theorem add_congr.wr {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a + b) = i.wrap (a' + b') := by + have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a) + rw [h₁] at this; rw [← this] at h₁; apply add_congr.ww h h₁ h₂ + +theorem add_congr.wl {α i} [ToInt α i] [_root_.Add α] [ToInt.Add α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int} + (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a + b) = i.wrap (a' + b') := by + have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b) + rw [h₂] at this; rw [← this] at h₂; apply add_congr.ww h h₁ h₂ + +/-! Multiplication -/ + +theorem mul_congr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = b') : toInt (a * b) = i.wrap (a' * b') := by + rw [ToInt.Mul.toInt_mul, h₁, h₂] + +theorem mul_congr.ww {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) {a b : α} {a' b' : Int} + (h₁ : toInt a = i.wrap a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by + rw [ToInt.Mul.toInt_mul, h₁, h₂, ← i.wrap_mul]; apply h + +theorem mul_congr.wr {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int} + (h₁ : toInt a = a') (h₂ : toInt b = i.wrap b') : toInt (a * b) = i.wrap (a' * b') := by + have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem a) + rw [h₁] at this; rw [← this] at h₁; apply mul_congr.ww h h₁ h₂ + +theorem mul_congr.wl {α i} [ToInt α i] [_root_.Mul α] [ToInt.Mul α i] (h : i.isFinite) (h' : i.nonEmpty) {a b : α} {a' b' : Int} + (h₁ : toInt a = i.wrap a') (h₂ : toInt b = b') : toInt (a * b) = i.wrap (a' * b') := by + have := i.wrap_eq_self_iff h' _ |>.mpr (ToInt.toInt_mem b) + rw [h₂] at this; rw [← this] at h₂; apply mul_congr.ww h h₁ h₂ + +-- TODO: add theorems for other operations + + + +end Lean.Grind.ToInt diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean index 67c9ce3702..458829082a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean @@ -35,5 +35,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.search.assign (inherit builtin_initialize registerTraceClass `grind.debug.cutsat.search.conflict (inherited := true) builtin_initialize registerTraceClass `grind.debug.cutsat.search.backtrack (inherited := true) builtin_initialize registerTraceClass `grind.debug.cutsat.internalize +builtin_initialize registerTraceClass `grind.debug.cutsat.toInt end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index 9f028e645c..0af8329eec 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -8,6 +8,7 @@ import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt namespace Lean.Meta.Grind.Arith.Cutsat @@ -274,7 +275,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do /-- Different kinds of terms internalized by this module. -/ private inductive SupportedTermKind where - | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast + | add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast | neg deriving BEq private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) := @@ -285,9 +286,9 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) := | HDiv.hDiv α _ _ _ _ _ => some (.div, α) | HMod.hMod α _ _ _ _ _ => some (.mod, α) | HPow.hPow α _ _ _ _ _ => some (.pow, α) - | OfNat.ofNat α _ _ => some (.num, α) + | OfNat.ofNat α _ _ => some (.num, α) | Neg.neg α _ a => - let_expr OfNat.ofNat _ _ _ := a | none + let_expr OfNat.ofNat _ _ _ := a | some (.neg, α) some (.num, α) | Int.natAbs _ => some (.natAbs, Nat.mkType) | Int.toNat _ => some (.toNat, Nat.mkType) @@ -300,7 +301,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) : -- TODO: document `NatCast.natCast` case. -- Remark: we added it to prevent natCast_sub from being expanded twice. if declName == ``NatCast.natCast then return true - if k matches .div | .mod | .sub | .pow | .natAbs | .toNat | .natCast then return false + if k matches .div | .mod | .sub | .pow | .neg | .natAbs | .toNat | .natCast then return false if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true match k with | .add => return false @@ -408,5 +409,10 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do | .natAbs => propagateNatAbs e | .toNat => propagateToNat e | _ => internalizeNat e + else if let some (e', h) ← toInt? e type then + -- TODO: save `(e', h)` + trace[grind.debug.cutsat.toInt] "{e} ==> {e'}" + trace[grind.debug.cutsat.toInt] "{h} : {← inferType h}" + check h end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index 1169d3d1e0..f6af41089a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean @@ -501,7 +501,7 @@ def resolveConflict (h : UnsatProof) : SearchM Unit := do s.assert /-- Search for an assignment/model for the linear constraints. -/ -private def searchAssigmentMain : SearchM Unit := do +private def searchAssignmentMain : SearchM Unit := do repeat trace[grind.debug.cutsat.search] "main loop" checkSystem "cutsat" @@ -527,7 +527,7 @@ private def resetDecisionStack : SearchM Unit := do private def searchQLiaAssignment : GoalM Bool := do let go : SearchM Bool := do - searchAssigmentMain + searchAssignmentMain let precise := (← get).precise resetDecisionStack return precise @@ -535,11 +535,11 @@ private def searchQLiaAssignment : GoalM Bool := do private def searchLiaAssignment : GoalM Unit := do let go : SearchM Unit := do - searchAssigmentMain + searchAssignmentMain resetDecisionStack go .int |>.run' {} -def searchAssigment : GoalM Unit := do +def searchAssignment : GoalM Unit := do let precise ← searchQLiaAssignment if (← isInconsistent) then return () if !(← getConfig).qlia && !precise then @@ -564,7 +564,7 @@ def check : GoalM Bool := do if (← hasAssignment) then return false else - searchAssigment + searchAssignment return true end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean new file mode 100644 index 0000000000..10b57a68b1 --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Grind.ToIntLemmas +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util + +namespace Lean.Meta.Grind.Arith.Cutsat + +private def reportMissingToIntAdapter (type : Expr) (instType : Expr) : MetaM Unit := do + trace[grind.debug.cutsat.debug] "`ToInt` initialization failure, failed to synthesize{indentExpr instType}\nfor type{indentExpr type}" + +private def throwMissingDecl (declName : Name) : MetaM Unit := + throwError "`grind cutsat`, unexpected missing declaration {declName}" + +private def checkDecl (declName : Name) : MetaM Unit := do + unless (← getEnv).contains declName do + throwMissingDecl declName + +private def mkOpCongr (type : Expr) (u : Level) (toIntInst : Expr) (rangeExpr : Expr) (range : Grind.IntInterval) (opBaseName : Name) (thmName : Name) : MetaM ToIntCongr := do + let op := mkApp (mkConst opBaseName [u]) type + let .some opInst ← trySynthInstance op | return {} + let toIntOpName := ``Grind.ToInt ++ opBaseName + checkDecl toIntOpName + let toIntOp := mkApp4 (mkConst toIntOpName [u]) type opInst rangeExpr toIntInst + let .some toIntOpInst ← trySynthInstance toIntOp + | reportMissingToIntAdapter type toIntOp; return {} + checkDecl thmName + let c := mkApp5 (mkConst thmName [u]) type rangeExpr toIntInst opInst toIntOpInst + let env ← getEnv + let cwwName := thmName ++ `ww + let cwlName := thmName ++ `wl + let cwrName := thmName ++ `wr + let c_ww? := if range.isFinite && env.contains cwwName then + some <| mkApp6 (mkConst cwwName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue + else + none + let c_wl? := if range.isFinite && range.nonEmpty && env.contains cwwName then + some <| mkApp7 (mkConst cwlName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue reflBoolTrue + else + none + let c_wr? := if range.isFinite && range.nonEmpty && env.contains cwwName then + some <| mkApp7 (mkConst cwrName [u]) type rangeExpr toIntInst opInst toIntOpInst reflBoolTrue reflBoolTrue + else + none + return { c? := some c, c_ww?, c_wl?, c_wr? } + +-- TODO: improve this function +private def evalInt? (e : Expr) : MetaM (Option Int) := do + let e ← whnfD e + match_expr e with + | Int.ofNat a => + let some a ← getNatValue? (← whnfD a) | return none + return some (a : Int) + | Int.negSucc a => + let some a ← getNatValue? (← whnfD a) | return none + return some (- (a : Int) - 1) + | _ => return none + +def getToIntInfo? (type : Expr) : GoalM (Option ToIntInfo) := do + if let some id? := (← get').toIntInfos.find? { expr := type } then + return id? + else + let info? ← go? + modify' fun s => { s with toIntInfos := s.toIntInfos.insert { expr := type } info? } + return info? +where + toIntInterval? (rangeExpr : Expr) : GoalM (Option Grind.IntInterval) := do + let rangeExpr ← whnfD rangeExpr + match_expr rangeExpr with + | Grind.IntInterval.co lo hi => + let some lo ← evalInt? lo + | trace[grind.debug.cutsat.toInt] "`ToInt` lower bound could not be reduced to an integer{indentExpr (← whnfD lo)}\nfor type{indentExpr type}" + return none + let some hi ← evalInt? hi + | trace[grind.debug.cutsat.toInt] "`ToInt` upper bound could not be reduced to an integer{indentExpr hi}\nfor type{indentExpr type}" + return none + return some (.co lo hi) + | _ => + trace[grind.debug.cutsat.toInt] "unsupported `ToInt` interval{indentExpr rangeExpr}\nfor type{indentExpr type}" + return none + + go? : GoalM (Option ToIntInfo) := withNewMCtxDepth do + let u' ← getLevel type + let u ← decLevel u' + let rangeExpr ← mkFreshExprMVar (mkConst ``Grind.IntInterval) + let toIntType := mkApp2 (mkConst ``Grind.ToInt [u]) type rangeExpr + let .some toIntInst ← trySynthInstance toIntType | + trace[grind.debug.cutsat.toInt] "failed to synthesize {indentExpr toIntType}" + return none + let rangeExpr ← instantiateMVars rangeExpr + let some range ← toIntInterval? rangeExpr | return none + let toInt := mkApp3 (mkConst ``Grind.ToInt.toInt [u]) type rangeExpr toIntInst + let wrap := mkApp (mkConst ``Grind.IntInterval.wrap) rangeExpr + let ofWrap0? := if let .co 0 hi := range then + some <| mkApp3 (mkConst ``Grind.ToInt.of_eq_wrap_co_0) rangeExpr (toExpr hi) reflBoolTrue + else + none + let ofEq := mkApp3 (mkConst ``Grind.ToInt.of_eq [u]) type rangeExpr toIntInst + let ofDiseq := mkApp3 (mkConst ``Grind.ToInt.of_diseq [u]) type rangeExpr toIntInst + let (ofLE?, ofNotLE?) ← do + let toLE := mkApp (mkConst ``LE [u]) type + let .some leInst ← LOption.toOption <$> trySynthInstance toLE | pure (none, none) + let toIntLE := mkApp4 (mkConst ``Grind.ToInt.LE [u]) type leInst rangeExpr toIntInst + let .some toIntLEInst ← LOption.toOption <$> trySynthInstance toIntLE + | reportMissingToIntAdapter type toIntLE; pure (none, none) + let ofLE := mkApp5 (mkConst ``Grind.ToInt.of_le [u]) type rangeExpr toIntInst leInst toIntLEInst + let ofNotLE := mkApp5 (mkConst ``Grind.ToInt.of_not_le [u]) type rangeExpr toIntInst leInst toIntLEInst + pure (some ofLE, some ofNotLE) + let (ofLT?, ofNotLT?) ← do + let toLT := mkApp (mkConst ``LT [u]) type + let .some ltInst ← LOption.toOption <$> trySynthInstance toLT | pure (none, none) + let toIntLT := mkApp4 (mkConst ``Grind.ToInt.LT [u]) type ltInst rangeExpr toIntInst + let .some toIntLTInst ← LOption.toOption <$> trySynthInstance toIntLT + | reportMissingToIntAdapter type toIntLT; pure (none, none) + let ofLT := mkApp5 (mkConst ``Grind.ToInt.of_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst + let ofNotLT := mkApp5 (mkConst ``Grind.ToInt.of_not_lt [u]) type rangeExpr toIntInst ltInst toIntLTInst + pure (some ofLT, some ofNotLT) + let mkOp (opBaseName : Name) (thmName : Name) := + mkOpCongr type u toIntInst rangeExpr range opBaseName thmName + let add ← mkOp ``Add ``Grind.ToInt.add_congr + let mul ← mkOp ``Mul ``Grind.ToInt.mul_congr + -- TODO: other operators + return some { + type, u, toIntInst, rangeExpr, range, toInt, wrap, ofWrap0?, ofEq, ofDiseq, ofLE?, ofNotLE?, ofLT?, ofNotLT?, add, mul + } + +structure ToIntM.Context where + info : ToIntInfo + +abbrev ToIntM := ReaderT ToIntM.Context GoalM + +def getInfo : ToIntM ToIntInfo := + return (← read).info + +def ToIntM.run? (type : Expr) (x : ToIntM α) : GoalM (Option α) := do + let some info ← getToIntInfo? type | return none + return some (← x { info }) + +private def isHomo (α β γ : Expr) : Bool := + isSameExpr α β && isSameExpr α γ + +private def intRfl := mkApp (mkConst ``Eq.refl [1]) Int.mkType + +private def toIntDef (e : Expr) : ToIntM (Expr × Expr) := do + let e' := mkApp (← getInfo).toInt e + let he := mkApp intRfl e' + return (e', he) + +private def isWrap (e : Expr) : Option Expr := + match_expr e with + | Grind.IntInterval.wrap _ a => some a + | _ => none + +/-- +Given `h : toInt a = i.wrap b`, return `(b', h)` where +`b'` is the expanded form of `i.wrap b`, and `h : toInt a = b'` +-/ +private def expandWrap (a b : Expr) (h : Expr) : ToIntM (Expr × Expr) := do + match (← getInfo).range with + | .ii => return (b, h) + | .co 0 hi => + let b' := mkIntMod b (toExpr hi) + let toA := mkApp (← getInfo).toInt a + let h := mkApp3 (← getInfo).ofWrap0?.get! toA b h + return (b', h) + | .co lo hi => + let b' := mkIntAdd (mkIntMod (mkIntSub b (toExpr lo)) (toExpr (hi - lo))) (toExpr lo) + return (b', h) + | _ => throwError "`grind cutsat`, `ToInt` interval not supported yet" + +private def mkToIntResult (toIntOp : ToIntCongr) (mkBinOp : Expr → Expr → Expr) (a b : Expr) (a' b' : Expr) (h₁ h₂ : Expr) : ToIntM (Expr × Expr) := do + let f := toIntOp.c?.get! + let mk (f : Expr) (a' b' : Expr) : ToIntM (Expr × Expr) := do + let h := mkApp6 f a b a' b' h₁ h₂ + let r := mkApp (← getInfo).wrap (mkBinOp a' b') + return (r, h) + match isWrap a', isWrap b' with + | none, none => mk f a' b' + | some a'', none => if let some f := toIntOp.c_wl? then mk f a'' b' else mk f a' b' + | none, some b'' => if let some f := toIntOp.c_wr? then mk f a' b'' else mk f a' b' + | some a'', some b'' => if let some f := toIntOp.c_ww? then mk f a'' b'' else mk f a' b' + +partial def toInt (e : Expr) : ToIntM (Expr × Expr) := do + match_expr e with + | HAdd.hAdd α β γ _ a b => + unless isHomo α β γ do return (← toIntDef e) + toIntBin (← getInfo).add mkIntAdd a b + | HMul.hMul α β γ _ a b => + unless isHomo α β γ do return (← toIntDef e) + toIntBin (← getInfo).mul mkIntMul a b + -- TODO: other operators + | _ => toIntDef e +where + toIntBin (toIntOp : ToIntCongr) (mkBinOp : Expr → Expr → Expr) (a b : Expr) : ToIntM (Expr × Expr) := do + unless toIntOp.c?.isSome do return (← toIntDef e) + let (a', h₁) ← toInt a + let (b', h₂) ← toInt b + mkToIntResult toIntOp mkBinOp a b a' b' h₁ h₂ + +def toInt? (a : Expr) (type : Expr) : GoalM (Option (Expr × Expr)) := do + ToIntM.run? type do + let (b, h) ← toInt a + match isWrap b with + | some b' => expandWrap a b' h + | _ => return (b, h) + +end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean new file mode 100644 index 0000000000..f3d6b83011 --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean @@ -0,0 +1,39 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Grind.ToInt +import Lean.Meta.Tactic.Grind.Arith.Util + +namespace Lean.Meta.Grind.Arith.Cutsat +open Lean Grind + +structure ToIntCongr where + c? : Option Expr := none + c_ww? : Option Expr := none + c_wl? : Option Expr := none + c_wr? : Option Expr := none + +structure ToIntInfo where + type : Expr + u : Level + toIntInst : Expr + rangeExpr : Expr + range : IntInterval + toInt : Expr + wrap : Expr + -- theorem `of_eq_wrap_co_0` if `range == .co 0 hi` + ofWrap0? : Option Expr + ofEq : Expr + ofDiseq : Expr + ofLE? : Option Expr + ofNotLE? : Option Expr + ofLT? : Option Expr + ofNotLT? : Option Expr + add : ToIntCongr + mul : ToIntCongr + -- TODO: other operators + +end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index e518df49d3..64e8a62e25 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -9,6 +9,7 @@ import Std.Internal.Rat import Lean.Data.PersistentArray import Lean.Meta.Tactic.Grind.ExprPtr import Lean.Meta.Tactic.Grind.Arith.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo namespace Lean.Meta.Grind.Arith.Cutsat @@ -153,7 +154,7 @@ inductive DvdCnstrProof where /-- `c.c₃?` must be `some` -/ | cooper₂ (c : CooperSplit) -/-- An inequalirty constraint and its justification/proof. -/ +/-- An inequality constraint and its justification/proof. -/ structure LeCnstr where p : Poly h : LeCnstrProof @@ -197,7 +198,7 @@ inductive DiseqCnstrProof where /-- A proof of `False`. -Remark: We will later add support for a backtraking search inside of cutsat. +Remark: We will later add support for a backtracking search inside of cutsat. -/ inductive UnsatProof where | dvd (c : DvdCnstr) @@ -306,7 +307,7 @@ structure State where - `Int.Linear.emod_le` -/ divMod : PHashSet (Expr × Int) := {} - /- TODO: Model-based theory combination. -/ + toIntInfos : PHashMap ExprPtr (Option ToIntInfo) := {} deriving Inhabited end Lean.Meta.Grind.Arith.Cutsat