From 0aca10b228974232cd2d77cd4575a8594458c6e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2025 23:29:31 -0700 Subject: [PATCH] feat: `Toint` inequalities in cutsat (#9026) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements support for (non strict) `ToInt` inequalities in `grind cutsat`. `grind cutsat` can solve simple problems such as: ```lean example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by grind example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b ≤ c → a ≤ c + 1 := by grind example (a b c : UInt8) : a ≤ b → b ≤ c → a ≤ c := by grind example (a b c d : UInt32) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by grind ``` Next step: strict inequalities, and equalities. --- .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 20 ++-- .../Tactic/Grind/Arith/Cutsat/LeCnstr.lean | 22 ++++- .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean | 6 +- .../Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean | 93 +++++++++++++------ .../Tactic/Grind/Arith/Cutsat/ToIntInfo.lean | 10 ++ .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 10 ++ .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean | 3 - .../Tactic/Grind/Arith/Linear/StructId.lean | 21 +++-- src/Lean/Meta/Tactic/Grind/Arith/Main.lean | 4 +- tests/lean/run/grind_cutsat_toint_1.lean | 11 +++ 10 files changed, 146 insertions(+), 54 deletions(-) create mode 100644 tests/lean/run/grind_cutsat_toint_1.lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index fe22dcd459..82df6c21db 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -382,7 +382,6 @@ private def internalizeNat (e : Expr) : GoalM Unit := do let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr } c.assert - private def isToIntForbiddenParent (parent? : Option Expr) : Bool := if let some parent := parent? then getKindAndType? parent |>.isSome @@ -410,20 +409,25 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do | _ => internalizeInt e else if type.isConstOf ``Nat then if isForbiddenParent parent? k then return () - trace[grind.debug.cutsat.internalize] "{e} : {type}" if (← isNatTerm e) then return () + trace[grind.debug.cutsat.internalize] "{e} : {type}" discard <| mkNatVar e match k with | .sub => propagateNatSub e | .natAbs => propagateNatAbs e | .toNat => propagateToNat e | _ => internalizeNat e - else if let some (e', h) ← toInt? e type then + else if isToIntForbiddenParent parent? then return () - trace[grind.debug.cutsat.internalize] "{e} : {type}" - -- TODO: save `(e', h)` - trace[grind.debug.cutsat.toInt] "{e} ==> {e'}" - trace[grind.debug.cutsat.toInt] "{h} : {← inferType h}" - check h + -- Term has already been internalized + if (← isToIntTerm e) then return () + if let some (eToInt, he) ← toInt? e type then + trace[grind.debug.cutsat.internalize] "{e} : {type}" + trace[grind.debug.cutsat.toInt] "{e} ==> {eToInt}" + let α := type + modify' fun s => { s with + toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α } + } + markAsCutsatTerm e end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean index 94d6bc3af6..ef8a178f81 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean @@ -11,6 +11,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt namespace Lean.Meta.Grind.Arith.Cutsat @@ -160,12 +161,29 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do trace[grind.cutsat.assert.le] "{← c.pp}" c.assert -def propagateIfSupportedLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do +def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do + let some thm ← if eqTrue then pure (← getInfo).ofLE? else pure (← getInfo).ofNotLE? | return () + let_expr LE.le _ _ a b := e | return () + let gen ← getGeneration e + let (a', h₁) ← toInt a + let (b', h₂) ← toInt b + let thm := mkApp6 thm a b a' b' h₁ h₂ + let (a', b') := if eqTrue then (a', b') else (mkIntAdd b' (mkIntLit 1), a') + let lhs ← toLinearExpr a' gen + let rhs ← toLinearExpr b' gen + let p := lhs.sub rhs |>.norm + let c := { p, h := .coreToInt e eqTrue thm lhs rhs : LeCnstr } + trace[grind.cutsat.assert.le] "{← c.pp}" + c.assert + +def propagateLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do unless (← getConfig).cutsat do return () let_expr LE.le α _ _ _ := e | return () if α.isConstOf ``Nat then propagateNatLe e eqTrue - else + else if α.isConstOf ``Int then propagateIntLe e eqTrue + else ToIntM.run α do + propagateToIntLe e eqTrue end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index cce8966022..335ea5fb13 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean @@ -200,6 +200,10 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do let ctx ← getNatContext let h := mkApp4 (mkConst ``Int.OfNat.of_le) ctx (← mkNatExprDecl lhs) (← mkNatExprDecl rhs) (mkOfEqTrueCore e (← mkEqTrueProof e)) return mkApp6 (mkConst ``Int.Linear.le_norm_expr) (← getContext) (← mkExprDecl lhs') (← mkExprDecl rhs') (← mkPolyDecl c'.p) reflBoolTrue h + | .coreToInt e pos toIntThm lhs rhs => + let h ← if pos then pure <| mkOfEqTrueCore e (← mkEqTrueProof e) else pure <| mkOfEqFalseCore e (← mkEqFalseProof e) + let h := mkApp toIntThm h + return mkApp6 (mkConst ``Int.Linear.le_norm_expr) (← getContext) (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue h | .denoteAsIntNonneg rhs rhs' => let ctx ← getNatContext let h := mkApp2 (mkConst ``Int.OfNat.Expr.denoteAsInt_nonneg) ctx (toExpr rhs) @@ -395,7 +399,7 @@ partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .denoteAsIntNonneg .. => return () + | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .coreToInt .. | .denoteAsIntNonneg .. => return () | .dec h => markAsFound h | .cooper c | .norm c | .divCoeffs c => c.collectDecVars | .dvdTight c₁ c₂ | .negDvdTight c₁ c₂ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean index 2095736cf1..3059aaa4bb 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToInt.lean @@ -5,6 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Init.Grind.ToIntLemmas +import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util namespace Lean.Meta.Grind.Arith.Cutsat @@ -156,6 +157,7 @@ where let powThm? ← mkPowThm? type u toIntInst rangeExpr let zeroThm? ← mkSimpleOpThm? ``Zero ``Grind.ToInt.zero_eq let ofNatThm? ← mkOfNatThm? type u toIntInst rangeExpr + trace[grind.debug.cutsat.toInt] "registered toInt: {type}" return some { type, u, toIntInst, rangeExpr, range, toInt, wrap, ofWrap0?, ofEq, ofDiseq, ofLE?, ofNotLE?, ofLT?, ofNotLT?, addThms, mulThms, subThm?, negThm?, divThm?, modThm?, powThm?, zeroThm?, ofNatThm? @@ -173,15 +175,33 @@ 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 α γ +def ToIntM.run (type : Expr) (x : ToIntM Unit) : GoalM Unit := do + let some info ← getToIntInfo? type | return () + x { info } 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) +def mkToIntVar (e : Expr) : ToIntM (Expr × Expr) := do + if let some info := (← get').toIntTermMap.find? { expr := e } then + return (info.eToInt, info.he) + let eToInt := mkApp (← getInfo).toInt e + let he := mkApp intRfl eToInt + let α := (← getInfo).type + modify' fun s => { s with + toIntTermMap := s.toIntTermMap.insert { expr := e } { eToInt, he, α } + } + markAsCutsatTerm e + return (eToInt, he) + +def getToIntTermType? (e : Expr) : GoalM (Option Expr) := do + let some info := (← get').toIntTermMap.find? { expr := e } | return none + return some info.α + +def isToIntTerm (e : Expr) : GoalM Bool := + return (← get').toIntTermMap.contains { expr := e } + +private def isHomo (α β γ : Expr) : Bool := + isSameExpr α β && isSameExpr α γ private def isWrap (e : Expr) : Option Expr := match_expr e with @@ -232,52 +252,52 @@ private def ToIntThms.mkResult (toIntThms : ToIntThms) (mkBinOp : Expr → Expr | none, some b'' => if let some f := toIntThms.c_wr? then mk f a' b'' else mk f a' b' | some a'', some b'' => if let some f := toIntThms.c_ww? then mk f a'' b'' else mk f a' b' -partial def toInt (e : Expr) : ToIntM (Expr × Expr) := do +private partial def toInt' (e : Expr) : ToIntM (Expr × Expr) := do match_expr e with | HAdd.hAdd α β γ _ a b => - unless isHomo α β γ do return (← toIntDef e) + unless isHomo α β γ do return (← mkToIntVar e) toIntBin (← getInfo).addThms mkIntAdd a b | HMul.hMul α β γ _ a b => - unless isHomo α β γ do return (← toIntDef e) + unless isHomo α β γ do return (← mkToIntVar e) toIntBin (← getInfo).mulThms mkIntMul a b | HDiv.hDiv α β γ _ a b => - unless isHomo α β γ do return (← toIntDef e) + unless isHomo α β γ do return (← mkToIntVar e) processDivMod (isDiv := true) a b | HMod.hMod α β γ _ a b => - unless isHomo α β γ do return (← toIntDef e) + unless isHomo α β γ do return (← mkToIntVar e) processDivMod (isDiv := false) a b | HSub.hSub α β γ _ a b => - unless isHomo α β γ do return (← toIntDef e) + unless isHomo α β γ do return (← mkToIntVar e) processSub a b | Neg.neg _ _ a => processNeg a | HPow.hPow α β γ _ a b => - unless isSameExpr α γ && β.isConstOf ``Nat do return (← toIntDef e) + unless isSameExpr α γ && β.isConstOf ``Nat do return (← mkToIntVar e) processPow a b | Zero.zero _ _ => - let some thm := (← getInfo).zeroThm? | toIntDef e + let some thm := (← getInfo).zeroThm? | mkToIntVar e return (mkIntLit 0, thm) | OfNat.ofNat _ n _ => - let some thm := (← getInfo).ofNatThm? | toIntDef e - let some n ← getNatValue? n | toIntDef e + let some thm := (← getInfo).ofNatThm? | mkToIntVar e + let some n ← getNatValue? n | mkToIntVar e let r := mkIntLit ((← getInfo).range.wrap n) let h := mkApp thm (toExpr n) return (r, h) - | _ => toIntDef e + | _ => mkToIntVar e where toIntBin (toIntOp : ToIntThms) (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 + unless toIntOp.c?.isSome do return (← mkToIntVar e) + let (a', h₁) ← toInt' a + let (b', h₂) ← toInt' b toIntOp.mkResult mkBinOp a b a' b' h₁ h₂ toIntAndExpandWrap (a : Expr) : ToIntM (Expr × Expr) := do - let (a', h₁) ← toInt a + let (a', h₁) ← toInt' a expandIfWrap a a' h₁ processDivMod (isDiv : Bool) (a b : Expr) : ToIntM (Expr × Expr) := do let some thm ← if isDiv then pure (← getInfo).divThm? else pure (← getInfo).modThm? - | return (← toIntDef e) + | return (← mkToIntVar e) let (a', h₁) ← toIntAndExpandWrap a let (b', h₂) ← toIntAndExpandWrap b let r := if isDiv then mkIntDiv a' b' else mkIntMod a' b' @@ -285,7 +305,7 @@ where return (r, h) processSub (a b : Expr) : ToIntM (Expr × Expr) := do - let some thm := (← getInfo).subThm? | return (← toIntDef e) + let some thm := (← getInfo).subThm? | return (← mkToIntVar e) let (a', h₁) ← toIntAndExpandWrap a let (b', h₂) ← toIntAndExpandWrap b let r ← mkWrap (mkIntSub a' b') @@ -293,24 +313,37 @@ where return (r, h) processNeg (a : Expr) : ToIntM (Expr × Expr) := do - let some thm := (← getInfo).negThm? | return (← toIntDef e) + let some thm := (← getInfo).negThm? | return (← mkToIntVar e) let (a', h₁) ← toIntAndExpandWrap a let r ← mkWrap (mkIntNeg a') let h := mkApp3 thm a a' h₁ return (r, h) processPow (a b : Expr) : ToIntM (Expr × Expr) := do - let some thm := (← getInfo).powThm? | return (← toIntDef e) + let some thm := (← getInfo).powThm? | return (← mkToIntVar e) let (a', h₁) ← toIntAndExpandWrap a let r ← mkWrap (mkIntPowNat a' b) let h := mkApp4 thm a b a' h₁ return (r, 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 +def toInt (a : Expr) : ToIntM (Expr × Expr) := do + let (b, h) ← toInt' a + let (b, h) ← match isWrap b with | some b' => expandWrap a b' h - | _ => return (b, h) + | _ => pure (b, h) + let r ← preprocess b + if let some proof := r.proof? then + return (r.expr, (← mkEqTrans h proof)) + else + return (r.expr, h) + +def toInt? (a : Expr) (type : Expr) : GoalM (Option (Expr × Expr)) := do + ToIntM.run? type do toInt a + +def isSupportedType (type : Expr) : GoalM Bool := do + if type == Nat.mkType || type == Int.mkType then + return true + else + return (← getToIntInfo? type).isSome 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 index 5b4b002807..5f2da87ef3 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/ToIntInfo.lean @@ -70,4 +70,14 @@ structure ToIntInfo where zeroThm? : Option Expr ofNatThm? : Option Expr +/-- +For each term `e` of type `α` which implements the `ToInt α i` class, +we store its corresponding `Int` term `eToInt`, a proof `he : toInt e = eToInt`, +and the type `α`. +-/ +structure ToIntTermInfo where + eToInt : Expr + α : Expr + he : Expr + 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 b421b5329c..3706d1bda4 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -164,6 +164,7 @@ inductive LeCnstrProof where | coreNeg (e : Expr) (p : Poly) | coreNat (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) | coreNatNeg (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) + | coreToInt (e : Expr) (pos : Bool) (toIntThm : Expr) (lhs rhs : Int.Linear.Expr) | denoteAsIntNonneg (rhs : Int.OfNat.Expr) (rhs' : Int.Linear.Expr) | dec (h : FVarId) | norm (c : LeCnstr) @@ -303,7 +304,16 @@ structure State where - `Int.Linear.emod_le` -/ divMod : PHashSet (Expr × Int) := {} + /-- + Mapping from a type `α` to its corresponding `ToIntInfo` object, which contains + the information needed to embed `α` terms into `Int` terms. + -/ toIntInfos : PHashMap ExprPtr (Option ToIntInfo) := {} + /-- + For each type `α` in `toIntInfos`, the mapping `toIntVarMap` contains a mapping + from a α-term `e` to the pair `(toInt e, α)`. + -/ + toIntTermMap : PHashMap ExprPtr ToIntTermInfo := {} deriving Inhabited end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean index 721e0f8378..593e9cbe32 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean @@ -28,9 +28,6 @@ end Int.Linear namespace Lean.Meta.Grind.Arith.Cutsat -def isSupportedType (type : Expr) : Bool := - type == Nat.mkType || type == Int.mkType - def get' : GoalM State := do return (← get).arith.cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index 6f453d1335..dfb588368a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Grind.Ordered.Module import Lean.Meta.Tactic.Grind.Simp -import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util +import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId import Lean.Meta.Tactic.Grind.Arith.Linear.Util import Lean.Meta.Tactic.Grind.Arith.Linear.Var @@ -55,11 +55,16 @@ private def isNonTrivialIsCharInst (isCharInst? : Option (Expr × Nat)) : Bool : | some (_, c) => c != 1 | none => false +private def isCutsatType (type : Expr) : GoalM Bool := do + if (← getConfig).cutsat then + if (← Cutsat.isSupportedType type) then + -- If `type` is supported by cutsat, let it handle + return true + return false + def getStructId? (type : Expr) : GoalM (Option Nat) := do unless (← getConfig).linarith do return none - if (← getConfig).cutsat && Cutsat.isSupportedType type then - -- If `type` is supported by cutsat, let it handle - return none + if (← isCutsatType type) then return none if let some id? := (← get').typeIdOf.find? { expr := type } then return id? else @@ -150,11 +155,11 @@ where pure (some leFn, some ltFn) else pure (none, none) - let getHSMulFn? : GoalM (Option Expr) := do + let rec getHSMulFn? : GoalM (Option Expr) := do let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type let .some smulInst ← trySynthInstance smulType | return none internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst - let getHSMulNatFn? : GoalM (Option Expr) := do + let rec getHSMulNatFn? : GoalM (Option Expr) := do let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type let .some smulInst ← trySynthInstance smulType | return none internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst @@ -164,7 +169,7 @@ where let semiringInst? ← getInst? ``Grind.Semiring let ringInst? ← getInst? ``Grind.Ring let fieldInst? ← getInst? ``Grind.Field - let getOne? : GoalM (Option Expr) := do + let rec getOne? : GoalM (Option Expr) := do let some oneInst ← getInst? ``One | return none let one ← internalizeConst <| mkApp2 (mkConst ``One.one [u]) type oneInst let one' ← mkNumeral type 1 @@ -182,7 +187,7 @@ where return some inst let orderedRingInst? ← getOrderedRingInst? let charInst? ← if let some semiringInst := semiringInst? then getIsCharInst? u type semiringInst else pure none - let getNoNatZeroDivInst? : GoalM (Option Expr) := do + let rec getNoNatZeroDivInst? : GoalM (Option Expr) := do let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type let .some hmulInst ← trySynthInstance hmulNat | return none let noNatZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type hmulInst diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Main.lean b/src/Lean/Meta/Tactic/Grind/Arith/Main.lean index 52d867ee2a..bafed5c4d6 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Main.lean @@ -32,12 +32,12 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do if (← isEqTrue e) then if let some c ← Offset.isCnstr? e then Offset.assertTrue c (← mkEqTrueProof e) - Cutsat.propagateIfSupportedLe e (eqTrue := true) + Cutsat.propagateLe e (eqTrue := true) Linear.propagateIneq e (eqTrue := true) else if (← isEqFalse e) then if let some c ← Offset.isCnstr? e then Offset.assertFalse c (← mkEqFalseProof e) - Cutsat.propagateIfSupportedLe e (eqTrue := false) + Cutsat.propagateLe e (eqTrue := false) Linear.propagateIneq e (eqTrue := false) builtin_grind_propagator propagateLT ↓LT.lt := fun e => do diff --git a/tests/lean/run/grind_cutsat_toint_1.lean b/tests/lean/run/grind_cutsat_toint_1.lean new file mode 100644 index 0000000000..e0bc773695 --- /dev/null +++ b/tests/lean/run/grind_cutsat_toint_1.lean @@ -0,0 +1,11 @@ +example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by + grind + +example (a b c : Fin 11) : c ≤ 9 → a ≤ b → b ≤ c → a ≤ c + 1 := by + grind + +example (a b c : UInt8) : a ≤ b → b ≤ c → a ≤ c := by + grind + +example (a b c d : UInt32) : a ≤ b → b ≤ c → c ≤ d → a ≤ d := by + grind