a9946fe4ac
This PR makes `lia` (and `grind`'s arithmetic case-split heuristic) recognize implications whose antecedent is an `And` or `Or` of arithmetic predicates as relevant case-split candidates. Previously, `Arith.isRelevantPred` only matched `Not`, `LE`, `LT`, `Eq`, and `Dvd`. With `splitImp := false` (the default), implications `p → q` are added as split candidates only when `p` is arith-relevant, so a hypothesis like `(b ≤ e ∧ e < b + c → a ≤ e ∧ e < a + d)` was never registered as a candidate. cutsat/lia would then find a satisfying assignment for the constraints it had been told about, but that assignment would not necessarily satisfy the original implication, yielding the bad counterexample reported in #13575. After this change, `isRelevantPred` recurses through `And` and `Or` (returning `true` if either operand is relevant), so the implication is split, modus ponens fires in the True branch, and cutsat/lia closes the False branch via the disjunction over negated atoms. Closes #13575.
15 lines
551 B
Text
15 lines
551 B
Text
-- MWE for lia regression generated by the new canonicalizer
|
|
|
|
example (n : Nat) (i : Fin (n + 1 + 1)) (h : n + 1 + 1 ≤ ↑i + ↑i + 1) :
|
|
↑i + ↑i + 1 - (n + 1 + 1) < n + 1 + 1 := by
|
|
lia
|
|
|
|
-- Regression test for issue #13575: `lia` should case-split on implications
|
|
-- whose antecedent is a conjunction of arithmetic predicates.
|
|
example (a b c d e : Int) :
|
|
e = b + c - 1 →
|
|
0 < c →
|
|
(b ≤ b ∧ b < b + c → a ≤ b ∧ b < a + d) →
|
|
(b ≤ e ∧ e < b + c → a ≤ e ∧ e < a + d) →
|
|
b + c ≤ a + d := by
|
|
lia
|