Sixty-five arms become sixty-five rules: InequalityEquality is data (#746) - #1082
Merged
Conversation
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.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd
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.
The set with the most arms after
Common, and the one where nothing collapses: it writesout shapes rather than orientations, so a commutative pattern has nothing to gather. Sixty-five
arms are sixty-five rules.
What it needs that a shape does not say
not (a and b and c)negates each operand and joins them by the dual connective — not a shape. The rule matches
the chain;
PushNotInsideand its guardMayPushNotInsidestay inPatterns.EqualityInequality.csand both forms ask them.opposite or exhaustive signs — which is a
whenover the bindings rather than a shape.i < 0isNaNrather than false (p or not pdepends on which side thenotis written, and reduces to True where the proposition is undefined #876). Asked of the same helpers, never restated.Measured
SolveMediumHard, masterSolveMediumHard, hereSimplifyEasyWhat the transcription found
Two wrong answers, both from writing the rules out as data — which makes the correspondence
between a pattern and its replacement something you have to state.
or-with-equality arms carried their neighbour's comparison, so(y < x) or (x = y)simplified tox <= y— its own negation off the diagonal. Fixedfirst, in Four
or-with-equality rules gave the opposite comparison (#1077) #1078, so this set agrees with aswitchthat is right.x! = 0is answeredFalseunconditioned, including at the negative integers wherex!has a pole and the statement isNaN. TheswitchreadsFactorialf({ DomainCondition: var condition }), a property pattern on the argumentrather than on the factorial. Filed as
x! = 0simplifies to False, including where the factorial has a pole #1081 and not fixed here — this rule is faithfulto the arm, which is what keeps the conversion mechanical. It was the single disagreement
out of 3,485 expressions in the agreement run.
Part of #746 tier 1.
🤖 Generated with Claude Code
https://claude.ai/code/session_01Bjumi5K7fg8yx6UK1mZTQd