Repository navigation
Four or-with-equality rules gave the opposite comparison (#1077) - #1078
Merged
Merged
Conversation
`a < b or a = b` is `a <= b`. Written with the comparison the other way round it answers the other way round -- `b < a or a = b` is `a >= b` -- and four of the eight arms of `InequalityEqualityRules` that say this carried their neighbour's answer. Off the diagonal the result was the negation of the input: `(y < x) or (x = y)` simplified to `x <= y`, which at x = 3, y = 2 is False where the input is True. They are only reachable with both operands symbolic, which is why four wrong arms sat there. With a number on one side, the `Lessf(var @const, ...)` arm further down the same set rewrites `2 < x` to `x > 2` earlier in the pass, so the disjunction is only ever looked at with both halves written the same way round and one of the four correct arms matches. Every affected shape needs two symbols. The test evaluates both sides at sample points rather than reading the rewritten comparison, because a wrong rewrite here is a well-formed comparison -- a test that records the answer records whichever answer it was given. It fails 16 of its 48 cases without the fix. Its remark says why the points straddle the diagonal and why both operands are symbols, so neither can be simplified away later without noticing. Found by transcribing the set into `MatchedRules` for #746 tier 1. Writing a rule out as data makes the correspondence between its pattern and its replacement something you have to state, and four of these did not survive stating it -- the same way the branch-cut gap in the reciprocal-logarithm rules turned up (#1062). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd
Rafael-SOWNet
added a commit
that referenced
this pull request
Aug 26, 2026
…1082) The set with the most arms after `Common`, and the one where nothing collapses: it writes out shapes rather than orientations, so a commutative pattern has nothing to gather. Sixty-five arms are sixty-five rules, and the gain is elsewhere. Three things it needs that a shape does not say, and each stays where it was written: * The two De Morgan arms are a **fold over a chain of any length** -- `not (a and b and c)` negates each operand and joins them by the dual connective. That is not a shape, so the rule matches the chain and `PushNotInside` in `Patterns.EqualityInequality.cs` does the fold, asked by both forms. Its guard is `MayPushNotInside`, likewise. * The excluded-middle pair reads **two bound comparisons against each other** -- same operands, opposite or exhaustive signs -- which is a `when` over the bindings. * The conditions those attach are about where the ordering is defined at all, since `i < 0` is `NaN` rather than false, and they are asked of the same helpers. Measured: `SolveMediumHard` allocates 165,054,016 B with this wired, which is master's figure to the byte, and `SimplifyEasy` 129,648 B likewise. **The transcription found a second wrong answer**, and the agreement run over 3,485 expressions reported it as its only disagreement. The `switch` reads `Factorialf({ DomainCondition: var condition })`, which is a property pattern on the factorial's *argument* rather than on the factorial -- so `x! = 0` is answered `False` unconditioned, including at the negative integers where `x!` has a pole and the statement is `NaN`. Filed as #1081 rather than fixed here: this rule is faithful to the arm, which is what makes the conversion mechanical, and the arm is a separate question. The first wrong answer that transcription found, four `or`-with-equality arms carrying their neighbour's comparison, was fixed first (#1077, #1078) so that this set agrees with a `switch` that is right. Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #1077.
a < b or a = bisa <= b. Written with the comparison the other way round it answersthe other way round:
b < a or a = bisa >= b. Four of the eight arms ofInequalityEqualityRulesthat say this carried their neighbour's answer, so off thediagonal the result was the negation of the input.
(y < x) or (x = y)x <= yApplyOnce("(y < x) or (x = y)")x <= yx >= yApplyOnce("(y > x) or (x = y)")x >= yx <= yApplyOnce("(x = y) or (y < x)")x <= yx >= yApplyOnce("(x = y) or (y > x)")x >= yx <= yApplyOnce("(x < y) or (x = y)")x <= yx <= y— this half was rightApplyOnce("(x > y) or (x = y)")x >= yx >= y— and so was thisBoth columns measured on a build of each side, not read off the diff.
Why four wrong arms survived. They are only reachable with both operands symbolic.
With a number on one side,
Lessf(var @const, ...)further down the same set rewrites2 < xtox > 2earlier in the pass, so the disjunction is only ever seen with bothhalves written the same way round and one of the four correct arms matches —
"(2 < x) or (x = 2)".Simplify()was and isx >= 2. A test written with a numericoperand would have passed on the defect.
The test evaluates rather than reads. A wrong rewrite here is a well-formed
comparison, so asserting on the printed answer records whichever answer it was given.
OrWithEqualityTestsubstitutes below, on and above the diagonal and requires the truthvalue to survive: 48 cases, 16 of which fail without this change.
Found by transcribing the set into
MatchedRulesfor #746 tier 1 — the same way thebranch-cut gap in the reciprocal-logarithm rules turned up (#1062). Writing a rule out as
data makes the correspondence between its pattern and its replacement something you have
to state.
🤖 Generated with Claude Code
https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd