Skip to content

Four rewrite rules hold only where they are written to - #2434

Open
Rafael-SOWNet wants to merge 4 commits into
masterfrom
feature/rules-that-hold-as-written
Open

Rafael-SOWNet wants to merge 4 commits into
masterfrom
feature/rules-that-hold-as-written

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Closes #2428.

Four rewrite rules were wrong as written, each the same on 2.6.0. Each fix is its own commit, and each keeps the hand-written switch copy of the rule in Patterns.*.cs in step with the data rule, as MatchedRulesAgreeWithTheSwitchTest requires.

  1. a^n / b^(c n) → (a / b^c)^n, and its mirror. Wrong through Simplify.
  2. (a > b and b > c) implies a > c → True. Wrong through Simplify: at a = i, b = 1, c = 0 the input is NaN.
    • Attaching a in RR, as p or not p depends on which side the not is written, and reduces to True where the proposition is undefined #876 does for x > x, would narrow instead: at a = i, b = 0, c = 1 the input is True, because NaN and False is False.
    • Fix: transitivity is decided only where every operand is known to be ordered (the real reading, or a known-real operand); otherwise the input is left as written.
    • Two BooleanSimplify.TestInequality rows that pinned x > y > z → x > z for symbols on the complex plane move to a theory over the reals, where they still hold.
  3. arcsin(n/d) → arccsc(d/n) at n = 0. Reachable through Transformation.Rewriting(RewriteRules.Trigonometric): arcsin(0/x) → arccsc(x/0) turns 0 into NaN, and arccos(0/x) → arcsec(x/0) likewise. Simplify folds 0/x first and is not affected.
    • Fix: a nonzero-numerator guard on all four rules.
  4. sgn(a) · a / |a| cancels. Reachable through Transformation.Rewriting(RewriteRules.Common): sgn(x)*(y*x)/abs(x) → y for non-real x, where at x = i the input is −y. sgn(a)·a/|a| is a^2/|a|^2, which is 1 only for real a. Simplify is not affected, because the canonical order flattens the product first.
    • Fix: cancel only where the operand is ordered.

soundcheck on master: 12 widen, 1 narrows, 80 none found. On this branch: 12 widen, 0 narrows, 81 none found. The arcsine rule moved from narrows to none found; the 12 widenings are other rules, deferred to #1019 §14. Each changed answer has a BREAKING-CHANGES.md row measured on the 2.6.0 package, each under its own heading.

Checked on this branch:

  • Tests: UnitTests 19381 passed, plus the MCP, Terminal, InteractiveWrapper and F# wrapper suites, and the AOT smoke test. Each fix has its own test.
  • Harnesses: BoundCheck, RootCheck, CasBench, PropCheck, SimpSweep, RuleCheck, CanonCheck and Confluence all pass, with reports identical to master's.
  • limitcheck at DEPTH=3, COUNT=600, on 42 seeds against master: no row changed.

🤖 Generated with Claude Code

Rafael-SOWNet and others added 4 commits November 13, 2026 18:00
…t holds

a^n / b^(c*n) -> (a / b^c)^n and its mirror had no guard. The gathering is
a^n / b^n -> (a/b)^n with b^c for a base, so it holds on that rule's
condition from #802: n whole, or both bases positive reals. Unguarded,
x^n / y^(2n) became (x / y^2)^n, which is 1 at x = 1, y = -1, n = 1/2,
where the quotient is -1. Both the data rule and its switch arm now ask
the same guard.

Found by the v3 definedness specification (work/v3-spec); no issue filed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
… are ordered

(a > b and b > c) implies a > c was simplified to True, carrying the
operands' domains but not that they are ordered. At a = i, b = 1, c = 0
the implication is NaN. The ordered condition cannot be attached as
x > x attaches it (#876): at a = i, b = 0, c = 1 the conjunction is
false and the implication is True, which True provided a in RR is not.
So both rules, and their switch arms, fire only where every operand is
known ordered: the real reading, or a known-real operand.

Two BooleanSimplify rows pinned True for symbols over the complex
plane; they now assert it over the reals, where it holds. Over the
complex plane the input is left as written.

Found by the v3 definedness specification (work/v3-spec); no issue filed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…umerator

arcsin(n / d) -> arccsc(d / n) and its three siblings read n / d as
1 / (d / n), which needs n nonzero. At n = 0 arcsin(0 / x), which is 0
wherever x is not, became arccsc(x / 0), which has no value: the
narrowing soundcheck reports. The data rules and their switch arms now
refuse a zero numerator.

Simplify folds 0 / x before the rules are asked, so no Simplify answer
changes; the rewrite is reachable through the public rule registry,
Transformation.Rewriting(RewriteRules.Trigonometric), and the test asks
it there.

Found by the v3 definedness specification (work/v3-spec); no issue filed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…perand

sgn(a) * (b * a) / abs(a) -> b provided not a = 0 holds for a real a.
The library's sgn(a) is a / abs(a), so off the real line the left side
is b * a^2 / abs(a)^2, which is -1 at a = i, b = 1. Realness is a
reading, not a condition on where a side is defined, so the rule and
its switch arm decide it as the comparison rules do (the real reading,
or an operand known real) and do not fire otherwise.

Simplify sorts the product before Common is asked and the nested
product never reaches the rule, so no Simplify answer changes; the
rewrite is reachable through Transformation.Rewriting(RewriteRules.Common),
and the test asks it there.

Found by the v3 definedness specification (work/v3-spec); no issue filed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@codecov

codecov Bot commented Nov 13, 2026 •

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 89.28571% with 6 lines in your changes missing coverage. Please review.
✅ Project coverage is 86.86%. Comparing base (2eea2e9) to head (6178967).
⚠️ Report is 2 commits behind head on master.

Files with missing lines Patch % Lines
...Math/Core/Transformations/Matching/MatchedRules.cs 91.17% 0 Missing and 3 partials ⚠️
...lification/Patterns/Patterns.EqualityInequality.cs 33.33% 0 Missing and 2 partials ⚠️
...nctions/Simplification/Patterns/Patterns.Common.cs 50.00% 0 Missing and 1 partial ⚠️
Additional details and impacted files

Impacted file tree graph

@@            Coverage Diff             @@
##           master    #2434      +/-   ##
==========================================
+ Coverage   86.81%   86.86%   +0.04%     
==========================================
  Files         312      312              
  Lines       69551    69766     +215     
  Branches    20316    20387      +71     
==========================================
+ Hits        60383    60604     +221     
+ Misses       4932     4916      -16     
- Partials     4236     4246      +10     
Flag Coverage Δ
cpp 37.77% <ø> (ø)
csharp 87.40% <89.28%> (+0.04%) ⬆️
fsharp 32.97% <ø> (ø)
interactive 39.81% <ø> (ø)

Flags with carried forward coverage won't be shown. Click here to find out more.

Files with missing lines Coverage Δ
...unctions/Simplification/Patterns/Patterns.Power.cs 92.09% <100.00%> (+0.20%) ⬆️
...s/Simplification/Patterns/Patterns.Trigonometry.cs 96.75% <100.00%> (ø)
...nctions/Simplification/Patterns/Patterns.Common.cs 91.27% <50.00%> (-0.34%) ⬇️
...lification/Patterns/Patterns.EqualityInequality.cs 87.81% <33.33%> (-0.96%) ⬇️
...Math/Core/Transformations/Matching/MatchedRules.cs 99.47% <91.17%> (-0.08%) ⬇️

... and 13 files with indirect coverage changes

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Status: Todo

Development

Successfully merging this pull request may close these issues.

Four rewrite rules are wrong as written: gathered powers, comparison chains, inverse reciprocals, sign over absolute value

1 participant