|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Leonardo de Moura |
| 5 | +-/ |
| 6 | +prelude |
| 7 | +import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof |
| 8 | +import Lean.Meta.Tactic.Grind.Arith.Linear.Util |
| 9 | +import Lean.Meta.Tactic.Grind.Arith.Linear.ToExpr |
| 10 | + |
| 11 | +namespace Lean.Meta.Grind.Arith.Linear |
| 12 | + |
| 13 | +open CommRing (RingExpr) |
| 14 | + |
| 15 | +/-- |
| 16 | +Returns a context of type `RArray α` containing the variables of the given structure, where |
| 17 | +`α` is `(← getStruct).type`. |
| 18 | +-/ |
| 19 | +def toContextExpr : LinearM Expr := do |
| 20 | + let struct ← getStruct |
| 21 | + if h : 0 < struct.vars.size then |
| 22 | + RArray.toExpr struct.type id (RArray.ofFn (struct.vars[·]) h) |
| 23 | + else |
| 24 | + RArray.toExpr struct.type id (RArray.leaf struct.zero) |
| 25 | + |
| 26 | +/-- |
| 27 | +Similar to `toContextExpr`, but for the `CommRing` module. |
| 28 | +Recall that this module interfaces with the `CommRing` module and their variable contexts |
| 29 | +may not be necessarily identical. For example, for this module, the term `x*y` does not have an interpretation |
| 30 | +and we have a "variable" representing it, but it is interpreted in the `CommRing` module, and such |
| 31 | +variable does not exist there. On the other direction, suppose we have the inequality `z < 0`, and |
| 32 | +`z` does not occur in any equality or disequality. Then, the `CommRing` does not even "see" `z`, and |
| 33 | +`z` does not occur in its context, but it occurs in the variable context created by this module. |
| 34 | +-/ |
| 35 | +def toRingContextExpr : LinearM Expr := do |
| 36 | + if (← isCommRing) then |
| 37 | + withRingM do CommRing.toContextExpr |
| 38 | + else |
| 39 | + let struct ← getStruct |
| 40 | + RArray.toExpr struct.type id (RArray.leaf struct.zero) |
| 41 | + |
| 42 | +structure ProofM.State where |
| 43 | + cache : Std.HashMap UInt64 Expr := {} |
| 44 | + polyMap : Std.HashMap Poly Expr := {} |
| 45 | + exprMap : Std.HashMap LinExpr Expr := {} |
| 46 | + ringExprMap : Std.HashMap RingExpr Expr := {} |
| 47 | + |
| 48 | +structure ProofM.Context where |
| 49 | + ctx : Expr |
| 50 | + ringCtx : Expr |
| 51 | + |
| 52 | +/-- Auxiliary monad for constructing linarith proofs. -/ |
| 53 | +abbrev ProofM := ReaderT ProofM.Context (StateRefT ProofM.State LinearM) |
| 54 | + |
| 55 | +/-- Returns a Lean expression representing the variable context used to construct linarith proofs. -/ |
| 56 | +private abbrev getContext : ProofM Expr := do |
| 57 | + return (← read).ctx |
| 58 | + |
| 59 | +/-- |
| 60 | +Returns a Lean expression representing the auxiliary `CommRing` variable context |
| 61 | +used to construct linarith proofs. |
| 62 | +-/ |
| 63 | +private abbrev getRingContext : ProofM Expr := do |
| 64 | + return (← read).ringCtx |
| 65 | + |
| 66 | +private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do |
| 67 | + let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2 |
| 68 | + if let some h := (← get).cache[addr]? then |
| 69 | + return h |
| 70 | + else |
| 71 | + let h ← k |
| 72 | + modify fun s => { s with cache := s.cache.insert addr h } |
| 73 | + return h |
| 74 | + |
| 75 | +def mkPolyDecl (p : Poly) : ProofM Expr := do |
| 76 | + if let some x := (← get).polyMap[p]? then |
| 77 | + return x |
| 78 | + let x := mkFVar (← mkFreshFVarId) |
| 79 | + modify fun s => { s with polyMap := s.polyMap.insert p x } |
| 80 | + return x |
| 81 | + |
| 82 | +def mkExprDecl (e : LinExpr) : ProofM Expr := do |
| 83 | + if let some x := (← get).exprMap[e]? then |
| 84 | + return x |
| 85 | + let x := mkFVar (← mkFreshFVarId) |
| 86 | + modify fun s => { s with exprMap := s.exprMap.insert e x } |
| 87 | + return x |
| 88 | + |
| 89 | +def mkRingExprDecl (e : RingExpr) : ProofM Expr := do |
| 90 | + if let some x := (← get).ringExprMap[e]? then |
| 91 | + return x |
| 92 | + let x := mkFVar (← mkFreshFVarId) |
| 93 | + modify fun s => { s with ringExprMap := s.ringExprMap.insert e x } |
| 94 | + return x |
| 95 | + |
| 96 | +private abbrev withProofContext (x : ProofM Expr) : LinearM Expr := do |
| 97 | + let struct ← getStruct |
| 98 | + withLetDecl `ctx (mkApp (mkConst ``RArray [struct.u]) struct.type) (← toContextExpr) fun ctx => do |
| 99 | + withLetDecl `rctx (mkApp (mkConst ``RArray [struct.u]) struct.type) (← toRingContextExpr) fun ringCtx => |
| 100 | + go { ctx, ringCtx } |>.run' {} |
| 101 | +where |
| 102 | + go : ProofM Expr := do |
| 103 | + let h ← x |
| 104 | + let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr |
| 105 | + let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr |
| 106 | + let h ← mkLetOfMap (← get).ringExprMap h `r (mkConst ``Grind.CommRing.Expr) toExpr |
| 107 | + mkLetFVars #[(← getContext), (← getRingContext)] h |
| 108 | + |
| 109 | +/-- |
| 110 | +Returns the prefix of a theorem with name `declName` where the first three arguments are |
| 111 | +`{α} [IntModule α] (ctx : Context α)` |
| 112 | +-/ |
| 113 | +private def mkIntModThmPrefix (declName : Name) : ProofM Expr := do |
| 114 | + let s ← getStruct |
| 115 | + return mkApp3 (mkConst declName [s.u]) s.type s.intModuleInst (← getContext) |
| 116 | + |
| 117 | +/-- |
| 118 | +Returns the prefix of a theorem with name `declName` where the first four arguments are |
| 119 | +`{α} [IntModule α] [Preorder α] (ctx : Context α)` |
| 120 | +-/ |
| 121 | +private def mkIntModPreThmPrefix (declName : Name) : ProofM Expr := do |
| 122 | + let s ← getStruct |
| 123 | + return mkApp4 (mkConst declName [s.u]) s.type s.intModuleInst s.preorderInst (← getContext) |
| 124 | + |
| 125 | +/-- |
| 126 | +Returns the prefix of a theorem with name `declName` where the first five arguments are |
| 127 | +`{α} [IntModule α] [Preorder α] [IntModule.IsOrdered α] (ctx : Context α)` |
| 128 | +This is the most common theorem prefix at `Linarith.lean` |
| 129 | +-/ |
| 130 | +private def mkIntModPreOrdThmPrefix (declName : Name) : ProofM Expr := do |
| 131 | + let s ← getStruct |
| 132 | + return mkApp5 (mkConst declName [s.u]) s.type s.intModuleInst s.preorderInst s.isOrdInst (← getContext) |
| 133 | + |
| 134 | +mutual |
| 135 | +partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do |
| 136 | + throwError "NIY" |
| 137 | + |
| 138 | +partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do |
| 139 | + match c'.h with |
| 140 | + | .core e lhs rhs => |
| 141 | + let h ← mkIntModPreOrdThmPrefix (if c'.strict then ``Grind.Linarith.lt_norm else ``Grind.Linarith.le_norm) |
| 142 | + return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) reflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e)) |
| 143 | + | _ => throwError "NIY" |
| 144 | + |
| 145 | +partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do |
| 146 | + throwError "NIY" |
| 147 | + |
| 148 | +partial def NotIneqCnstr.toExprProof (c' : NotIneqCnstr) : ProofM Expr := caching c' do |
| 149 | + throwError "NIY" |
| 150 | + |
| 151 | +partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do |
| 152 | + match h with |
| 153 | + | .lt c => return mkApp (← mkIntModPreThmPrefix ``Grind.Linarith.lt_unsat) (← c.toExprProof) |
| 154 | + | .diseq _ => throwError "NIY" |
| 155 | + |
| 156 | +end |
| 157 | + |
| 158 | +def UnsatProof.toExprProof (h : UnsatProof) : LinearM Expr := do |
| 159 | + withProofContext do h.toExprProofCore |
| 160 | + |
| 161 | +def setInconsistent (h : UnsatProof) : LinearM Unit := do |
| 162 | + if (← getStruct).caseSplits then |
| 163 | + -- Let the search procedure in `SearchM` resolve the conflict. |
| 164 | + modifyStruct fun s => { s with conflict? := some h } |
| 165 | + else |
| 166 | + let h ← h.toExprProof |
| 167 | + closeGoal h |
| 168 | + |
| 169 | +end Lean.Meta.Grind.Arith.Linear |
0 commit comments