Skip to content

v4.26.0-rc2

Pre-release
Pre-release

Choose a tag to compare

@github-actions github-actions released this 21 Nov 02:01
· 1214 commits to master since this release
fix: bug `ite`/`dite` propagator used in `grind` (#11295)

This PR fixes a bug in the propagation rules for `ite` and `dite` used
in `grind`. The bug prevented equalities from being propagated to the
satellite solvers. Here is an example affected by this issue.

```lean
example
    [LE α] [LT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α]
    [Lean.Grind.CommRing α] [DecidableLE α] [Lean.Grind.OrderedRing α]
    (a b c : α) :
  (if a - b ≤ -(a - b) then -(a - b) else a - b) ≤
  ((if a - c ≤ -(a - c) then -(a - c) else a - c) + if c - d ≤ -(c - d) then -(c - d) else c - d) +
    if b - d ≤ -(b - d) then -(b - d) else b - d := by
  grind
```