Repository navigation
Simplify can stop before its own answer is simplified #2133
Description
Simplify can return an answer that one more Simplify takes further, here to 0:
| Input | Simplify |
Simplify of that |
|---|---|---|
R^2 - R^2*(a+b)*(1/a+1/b)/4 - R^2*(a-b)*(1/a-1/b)/4 |
R ^ 2 + -1/2 * (R ^ 2 + R ^ 2) provided not a = 0 and not b = 0 |
0 provided … |
a*b*c*(1/a+1/b+1/c) - (a*b+b*c+c*a) |
a * b + b * (-a + c) + -b * c provided … |
0 |
(a*b+b*c+c*a)/3 - (a*b*c)*(1/a+1/b+1/c)/3 |
((-a + a) * (b + c) + c * (-b + b)) / 3 provided … |
0 |
In each case the input is written slightly differently from one that reaches 0 in a single pass:
- With
xin place ofR^2, the first row gives0 provided …. - The second row with its difference reversed gives
0 provided ….
The third answer contains -a + a itself, and InnerSimplified leaves -a + a as it is.
Separately, the result depends on how a sum is written: 2 - 2*cos(2*x) - 4*sin(x)^2 simplifies to 0, but the same expression written 2 + (-2) * cos(2 * x) + (-4) * sin(x) ^ 2 (which is how the first prints) stays as it is. So (cos(2*x) - 1)^2 + sin(2*x)^2 - 4*sin(x)^2 stops at that second form.
Found while reading Modenov's Problems in Geometry for #2131, whose proofs reduce to identities like these.
Activity
A sum of fractions that is a constant over one denominator simplifies…
Rafael-SOWNet commentedon Oct 27, 2026
The three rows of the table are answered since #2174, which offers the rational canonical form as a
Simplifycandidate:0 provided not a * b = 0for the first, and0 provided not a * b * c = 0for the other two. Still open here is the trigonometric part:2 - 2*cos(2*x) - 4*sin(x)^2reaches0, while the same sum written2 + (-2) * cos(2 * x) + (-4) * sin(x) ^ 2stays, so(cos(2*x) - 1)^2 + sin(2*x)^2 - 4*sin(x)^2stops at that second form.A squared sine and cosine with one coefficient are found anywhere in …
A trigonometric identity is decided over the sines and cosines of its…
Rafael-SOWNet commentedon Oct 28, 2026
(cos(2*x) - 1)^2 + sin(2*x)^2 - 4*sin(x)^2is0since #2179, which decides a rational function of sines and cosines whose angles are rational combinations of the variables. #2174 already answered the three rational rows, so every row of the table above now reaches0in oneSimplify.Still open here is the general point in the title: an answer that one more
Simplifytakes further. That property is what canoncheck's idempotence check measures.🤖 Generated with Claude Code
https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
Rafael-SOWNet commentedon Oct 31, 2026
Closing. Every row of the table reaches
0in oneSimplifyon master (5d973db): the rational rows since #2174, and the trigonometric one since #2179.The general point in the title, an answer that one more
Simplifytakes further, is idempotence, and canoncheck measures it on every change againstcanoncheck-baseline.tsv. A new instance turned up in #2306: a cancellation landedSimplifyon a candidate one step short of0for #557's second expression, andDoubleAngleOverSineTestcaught it before merge. A case found this way gets its own issue.🤖 Generated with Claude Code