7897dc91e6
This PR fixes an issue where `grind` could prove each conjunct individually but failed on the conjunction. The root cause: `solverAction`'s `.propagated` path calls `processNewFacts` which drains the `newFacts` queue, but the resulting propagation cascade (congruence closure, or-propagation, `propagateForallPropDown`) can call `addNewRawFact`, enqueuing to the separate `newRawFacts` queue. These raw facts were never drained. The fix moves `Solvers.mkAction` from `Types.lean` to `Intro.lean` where it can compose the core solver action with `assertAll`, unconditionally draining `newRawFacts` after every solver step. Closes #12581 Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
7 lines
388 B
Text
7 lines
388 B
Text
-- Testing conjunction of grind-provable goals
|
|
-- See https://github.com/leanprover/lean4/issues/12581
|
|
|
|
-- `grind` should be able to prove a conjunction of things it can prove individually
|
|
example {a b c d : Int} (f : Int → Nat → Int) (h₁ : a = 0) (h₁' : ∀ k, 0 ≤ f c k) (h₂ : b = 0) (h₂' : ∀ k, 0 ≤ f d k) :
|
|
a + b = 0 ∧ ∀ k, 0 ≤ f c k + f d k := by
|
|
grind
|