|
| 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.Lemmas |
| 8 | +import Lean.Meta.Tactic.Assert |
| 9 | +import Lean.Meta.Tactic.Grind.Simp |
| 10 | +import Lean.Meta.Tactic.Grind.Types |
| 11 | +import Lean.Meta.Tactic.Grind.Cases |
| 12 | +import Lean.Meta.Tactic.Grind.Injection |
| 13 | +import Lean.Meta.Tactic.Grind.Core |
| 14 | + |
| 15 | +namespace Lean.Meta.Grind |
| 16 | + |
| 17 | +private inductive IntroResult where |
| 18 | + | done |
| 19 | + | newHyp (fvarId : FVarId) (goal : Goal) |
| 20 | + | newDepHyp (goal : Goal) |
| 21 | + | newLocal (fvarId : FVarId) (goal : Goal) |
| 22 | + deriving Inhabited |
| 23 | + |
| 24 | +private def introNext (goal : Goal) : GrindM IntroResult := do |
| 25 | + let target ← goal.mvarId.getType |
| 26 | + if target.isArrow then |
| 27 | + goal.mvarId.withContext do |
| 28 | + let p := target.bindingDomain! |
| 29 | + if !(← isProp p) then |
| 30 | + let (fvarId, mvarId) ← goal.mvarId.intro1P |
| 31 | + return .newLocal fvarId { goal with mvarId } |
| 32 | + else |
| 33 | + let tag ← goal.mvarId.getTag |
| 34 | + let q := target.bindingBody! |
| 35 | + -- TODO: keep applying simp/eraseIrrelevantMData/canon/shareCommon until no progress |
| 36 | + let r ← simp p |
| 37 | + let fvarId ← mkFreshFVarId |
| 38 | + let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! r.expr target.bindingInfo! |
| 39 | + let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag |
| 40 | + let mvarIdNew := mvarNew.mvarId! |
| 41 | + mvarIdNew.withContext do |
| 42 | + let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew |
| 43 | + match r.proof? with |
| 44 | + | some he => |
| 45 | + let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, r.expr, q, he, h] |
| 46 | + goal.mvarId.assign hNew |
| 47 | + return .newHyp fvarId { goal with mvarId := mvarIdNew } |
| 48 | + | none => |
| 49 | + -- `p` and `p'` are definitionally equal |
| 50 | + goal.mvarId.assign h |
| 51 | + return .newHyp fvarId { goal with mvarId := mvarIdNew } |
| 52 | + else if target.isLet || target.isForall then |
| 53 | + let (fvarId, mvarId) ← goal.mvarId.intro1P |
| 54 | + mvarId.withContext do |
| 55 | + let localDecl ← fvarId.getDecl |
| 56 | + if (← isProp localDecl.type) then |
| 57 | + -- Add a non-dependent copy |
| 58 | + let mvarId ← mvarId.assert (← mkFreshUserName localDecl.userName) localDecl.type (mkFVar fvarId) |
| 59 | + return .newDepHyp { goal with mvarId } |
| 60 | + else |
| 61 | + return .newLocal fvarId { goal with mvarId } |
| 62 | + else |
| 63 | + return .done |
| 64 | + |
| 65 | +private def isCasesCandidate (fvarId : FVarId) : MetaM Bool := do |
| 66 | + let .const declName _ := (← fvarId.getType).getAppFn | return false |
| 67 | + isGrindCasesTarget declName |
| 68 | + |
| 69 | +private def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do |
| 70 | + if (← isCasesCandidate fvarId) then |
| 71 | + let mvarIds ← cases goal.mvarId fvarId |
| 72 | + return mvarIds.map fun mvarId => { goal with mvarId } |
| 73 | + else |
| 74 | + return none |
| 75 | + |
| 76 | +private def applyInjection? (goal : Goal) (fvarId : FVarId) : MetaM (Option Goal) := do |
| 77 | + if let some mvarId ← injection? goal.mvarId fvarId then |
| 78 | + return some { goal with mvarId } |
| 79 | + else |
| 80 | + return none |
| 81 | + |
| 82 | +/-- Introduce new hypotheses (and apply `by_contra`) until goal is of the form `... ⊢ False` -/ |
| 83 | +partial def intros (goal : Goal) (generation : Nat) : GrindM (List Goal) := do |
| 84 | + let rec go (goal : Goal) : StateRefT (Array Goal) GrindM Unit := do |
| 85 | + if goal.inconsistent then |
| 86 | + return () |
| 87 | + match (← introNext goal) with |
| 88 | + | .done => |
| 89 | + if let some mvarId ← goal.mvarId.byContra? then |
| 90 | + go { goal with mvarId } |
| 91 | + else |
| 92 | + modify fun s => s.push goal |
| 93 | + | .newHyp fvarId goal => |
| 94 | + if let some goals ← applyCases? goal fvarId then |
| 95 | + goals.forM go |
| 96 | + else if let some goal ← applyInjection? goal fvarId then |
| 97 | + go goal |
| 98 | + else |
| 99 | + go (← GoalM.run' goal <| addHypothesis fvarId generation) |
| 100 | + | .newDepHyp goal => |
| 101 | + go goal |
| 102 | + | .newLocal fvarId goal => |
| 103 | + if let some goals ← applyCases? goal fvarId then |
| 104 | + goals.forM go |
| 105 | + else |
| 106 | + go goal |
| 107 | + let (_, goals) ← (go goal).run #[] |
| 108 | + return goals.toList |
| 109 | + |
| 110 | +/-- Asserts a new fact `prop` with proof `proof` to the given `goal`. -/ |
| 111 | +def assertAt (goal : Goal) (proof : Expr) (prop : Expr) (generation : Nat) : GrindM (List Goal) := do |
| 112 | + -- TODO: check whether `prop` may benefit from `intros` or not. If not, we should avoid the `assert`+`intros` step and use `Grind.add` |
| 113 | + let mvarId ← goal.mvarId.assert (← mkFreshUserName `h) prop proof |
| 114 | + let goal := { goal with mvarId } |
| 115 | + intros goal generation |
| 116 | + |
| 117 | +/-- Asserts next fact in the `goal` fact queue. -/ |
| 118 | +def assertNext? (goal : Goal) : GrindM (Option (List Goal)) := do |
| 119 | + let some (fact, newFacts) := goal.newFacts.dequeue? |
| 120 | + | return none |
| 121 | + assertAt { goal with newFacts } fact.proof fact.prop fact.generation |
| 122 | + |
| 123 | +partial def iterate (goal : Goal) (f : Goal → GrindM (Option (List Goal))) : GrindM (List Goal) := do |
| 124 | + go [goal] [] |
| 125 | +where |
| 126 | + go (todo : List Goal) (result : List Goal) : GrindM (List Goal) := do |
| 127 | + match todo with |
| 128 | + | [] => return result |
| 129 | + | goal :: todo => |
| 130 | + if let some goalsNew ← f goal then |
| 131 | + go (goalsNew ++ todo) result |
| 132 | + else |
| 133 | + go todo (goal :: result) |
| 134 | + |
| 135 | +/-- Asserts all facts in the `goal` fact queue. -/ |
| 136 | +partial def assertAll (goal : Goal) : GrindM (List Goal) := do |
| 137 | + iterate goal assertNext? |
| 138 | + |
| 139 | +end Lean.Meta.Grind |
0 commit comments