|
| 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 Init.Grind.Ordered.Module |
| 8 | +import Lean.Meta.Tactic.Grind.Simp |
| 9 | +import Lean.Meta.Tactic.Grind.Arith.Linear.Util |
| 10 | +import Lean.Meta.Tactic.Grind.Arith.Linear.Var |
| 11 | + |
| 12 | +namespace Lean.Meta.Grind.Arith.Linear |
| 13 | + |
| 14 | +private def internalizeFn (fn : Expr) : GoalM Expr := do |
| 15 | + shareCommon (← canon fn) |
| 16 | + |
| 17 | +open Grind.Linarith (Poly) |
| 18 | + |
| 19 | +def getStructId? (type : Expr) : GoalM (Option Nat) := do |
| 20 | + if let some id? := (← get').typeIdOf.find? { expr := type } then |
| 21 | + return id? |
| 22 | + else |
| 23 | + let id? ← go? |
| 24 | + modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? } |
| 25 | + return id? |
| 26 | +where |
| 27 | + go? : GoalM (Option Nat) := do |
| 28 | + let u ← getDecLevel type |
| 29 | + let getInst? (declName : Name) : GoalM (Option Expr) := do |
| 30 | + let instType := mkApp (mkConst declName [u]) type |
| 31 | + return LOption.toOption (← trySynthInstance instType) |
| 32 | + let getInst (declName : Name) : GoalM Expr := do |
| 33 | + let instType := mkApp (mkConst declName [u]) type |
| 34 | + let .some inst ← trySynthInstance instType |
| 35 | + | throwError "`grind linarith` failed to find instance{indentExpr instType}" |
| 36 | + return inst |
| 37 | + let getBinHomoInst (declName : Name) : GoalM Expr := do |
| 38 | + let instType := mkApp3 (mkConst declName [u, u, u]) type type type |
| 39 | + let .some inst ← trySynthInstance instType |
| 40 | + | throwError "`grind linarith` failed to find instance{indentExpr instType}" |
| 41 | + return inst |
| 42 | + let getHMulInst : GoalM Expr := do |
| 43 | + let instType := mkApp3 (mkConst ``HMul [0, u, u]) Int.mkType type type |
| 44 | + let .some inst ← trySynthInstance instType |
| 45 | + | throwError "`grind linarith` failed to find instance{indentExpr instType}" |
| 46 | + return inst |
| 47 | + let checkToFieldDefEq? (parentInst? : Option Expr) (inst? : Option Expr) (toFieldName : Name) : GoalM (Option Expr) := do |
| 48 | + let some parentInst := parentInst? | return none |
| 49 | + let some inst := inst? | return none |
| 50 | + let toField := mkApp2 (mkConst toFieldName [u]) type inst |
| 51 | + unless (← withDefault <| isDefEq parentInst toField) do |
| 52 | + reportIssue! "`grind linarith` expected{indentExpr parentInst}\nto be definitionally equal to{indentExpr toField}" |
| 53 | + return none |
| 54 | + return some inst |
| 55 | + let ensureToFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) : GoalM Unit := do |
| 56 | + let toField := mkApp2 (mkConst toFieldName [u]) type inst |
| 57 | + unless (← withDefault <| isDefEq parentInst toField) do |
| 58 | + throwError "`grind linarith` expected{indentExpr parentInst}\nto be definitionally equal to{indentExpr toField}" |
| 59 | + let ensureToHomoFieldDefEq (parentInst : Expr) (inst : Expr) (toFieldName : Name) (toHeteroName : Name) : GoalM Unit := do |
| 60 | + let toField := mkApp2 (mkConst toFieldName [u]) type inst |
| 61 | + let heteroToField := mkApp2 (mkConst toHeteroName [u]) type toField |
| 62 | + unless (← withDefault <| isDefEq parentInst heteroToField) do |
| 63 | + throwError "`grind linarith` expected{indentExpr parentInst}\nto be definitionally equal to{indentExpr heteroToField}" |
| 64 | + let some intModuleInst ← getInst? ``Grind.IntModule | return none |
| 65 | + let zeroInst ← getInst ``Zero |
| 66 | + let zero := mkApp2 (mkConst ``Zero.zero [u]) type zeroInst |
| 67 | + let addInst ← getBinHomoInst ``HAdd |
| 68 | + let addFn := mkApp4 (mkConst ``HAdd.hAdd [u, u, u]) type type type addInst |
| 69 | + let subInst ← getBinHomoInst ``HSub |
| 70 | + let subFn := mkApp4 (mkConst ``HSub.hSub [u, u, u]) type type type subInst |
| 71 | + let negInst ← getInst ``Neg |
| 72 | + let negFn := mkApp2 (mkConst ``Neg.neg [u]) type negInst |
| 73 | + let hmulInst ← getHMulInst |
| 74 | + let hmulFn := mkApp4 (mkConst ``HMul.hMul [0, u, u]) Int.mkType type type hmulInst |
| 75 | + ensureToFieldDefEq zeroInst intModuleInst ``Grind.IntModule.toZero |
| 76 | + ensureToHomoFieldDefEq addInst intModuleInst ``Grind.IntModule.toAdd ``instHAdd |
| 77 | + ensureToHomoFieldDefEq subInst intModuleInst ``Grind.IntModule.toSub ``instHSub |
| 78 | + ensureToFieldDefEq negInst intModuleInst ``Grind.IntModule.toNeg |
| 79 | + ensureToFieldDefEq hmulInst intModuleInst ``Grind.IntModule.toHMul |
| 80 | + let some preorderInst ← getInst? ``Grind.Preorder | return none |
| 81 | + let leInst ← getInst ``LE |
| 82 | + let ltInst ← getInst ``LT |
| 83 | + let leFn := mkApp2 (mkConst ``LE.le [u]) type leInst |
| 84 | + let ltFn := mkApp2 (mkConst ``LT.lt [u]) type ltInst |
| 85 | + ensureToFieldDefEq leInst preorderInst ``Grind.Preorder.toLE |
| 86 | + ensureToFieldDefEq ltInst preorderInst ``Grind.Preorder.toLT |
| 87 | + let partialInst? ← checkToFieldDefEq? (some preorderInst) (← getInst? ``Grind.PartialOrder) ``Grind.PartialOrder.toPreorder |
| 88 | + let linearInst? ← checkToFieldDefEq? partialInst? (← getInst? ``Grind.LinearOrder) ``Grind.LinearOrder.toPartialOrder |
| 89 | + let isOrderedType := mkApp3 (mkConst ``Grind.IntModule.IsOrdered [u]) type preorderInst intModuleInst |
| 90 | + let .some isOrdInst ← trySynthInstance isOrderedType | return none |
| 91 | + let getSMulFn? : GoalM (Option Expr) := do |
| 92 | + let smulType := mkApp2 (mkConst ``SMul [0, u]) Int.mkType type |
| 93 | + let .some smulInst ← trySynthInstance smulType | return none |
| 94 | + let smulFn := mkApp3 (mkConst ``SMul.smul [0, u]) Int.mkType type smulInst |
| 95 | + if (← withDefault <| isDefEq hmulFn smulFn) then |
| 96 | + return smulFn |
| 97 | + reportIssue! "`grind linarith` expected{indentExpr hmulFn}\nto be definitionally equal to{indentExpr smulFn}" |
| 98 | + return none |
| 99 | + let smulFn? ← getSMulFn? |
| 100 | + let ringInst? ← getInst? ``Grind.Ring |
| 101 | + let getOne? : GoalM (Option Expr) := do |
| 102 | + let some oneInst ← getInst? ``One | return none |
| 103 | + let one := mkApp2 (mkConst ``One.one [u]) type oneInst |
| 104 | + let one' ← mkNumeral type 1 |
| 105 | + unless (← withDefault <| isDefEq one one') do reportIssue! "`grind linarith` expected{indentExpr one}\nto be definitionally equal to{indentExpr one'}" |
| 106 | + return some one |
| 107 | + let one? ← getOne? |
| 108 | + let commRingInst? ← getInst? ``Grind.CommRing |
| 109 | + let getRingIsOrdInst? : GoalM (Option Expr) := do |
| 110 | + let some ringInst := ringInst? | return none |
| 111 | + let isOrdType := mkApp3 (mkConst ``Grind.Ring.IsOrdered [u]) type ringInst preorderInst |
| 112 | + return LOption.toOption (← trySynthInstance isOrdType) |
| 113 | + let ringIsOrdInst? ← getRingIsOrdInst? |
| 114 | + let getNoNatZeroDivInst? : GoalM (Option Expr) := do |
| 115 | + let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type |
| 116 | + let .some hmulInst ← trySynthInstance hmulNat | return none |
| 117 | + let noNatZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst |
| 118 | + return LOption.toOption (← trySynthInstance noNatZeroDivType) |
| 119 | + let noNatDivInst? ← getNoNatZeroDivInst? |
| 120 | + let id := (← get').structs.size |
| 121 | + let struct : Struct := { |
| 122 | + id, type, u, intModuleInst, preorderInst, isOrdInst, partialInst?, linearInst?, noNatDivInst? |
| 123 | + leFn, ltFn, addFn, subFn, negFn, hmulFn, smulFn?, zero, one? |
| 124 | + ringInst?, commRingInst?, ringIsOrdInst? |
| 125 | + } |
| 126 | + modify' fun s => { s with structs := s.structs.push struct } |
| 127 | + if let some one := one? then |
| 128 | + if ringInst?.isSome then LinearM.run id do |
| 129 | + -- Create `1` variable, and assert strict lower bound `0 < 1` |
| 130 | + let x ← mkVar one |
| 131 | + let p := Poly.add (-1) x .nil |
| 132 | + modifyStruct fun s => { s with |
| 133 | + lowers := s.lowers.modify x fun cs => cs.push { p, h := .oneGtZero, strict := true } |
| 134 | + } |
| 135 | + return some id |
| 136 | + |
| 137 | +end Lean.Meta.Grind.Arith.Linear |
0 commit comments