Repository navigation
Answer an identity equation with every value, not with none (#550) - #679
Merged
Happypig375 merged 1 commit intoAug 4, 2026
Merged
Conversation
An equation that puts no condition on the variable is satisfied by every value of
it. AngouriMath said the opposite in two different ways:
(0 = 0).Solve(x) gave { } -- no value satisfies it
(x - x = 0).Solve(x) gave { 0 } -- exactly one does
The second is the more damaging of the two, because it is a wrong answer rather
than a missing one, and it is also where the reported symptom comes from. The
polynomial solver never checked whether a monomial's coefficient had cancelled,
so x - x was read as one times x, of degree one, with the root 0. A system that
happens to leave such an equation behind after substitution therefore came back
with a tuple that is a solution but not the solution set:
{ x - y = 0, 2x - 2y = 0 }.Solve(x, y) gave [[0, 0]]
Coefficients that evaluate to zero are now dropped before the degree is read.
When none is left the equation is an identity, and the solver says so with the
whole of C instead of the empty set. The same distinction is made where the
solver already knew it was there: the branch that gave up once the variable had
disappeared carried the comment "there is either 0 or +oo solutions" and returned
the empty set for both cases; it now decides which of the two it is.
A system whose equations no longer constrain a variable then has infinitely many
solutions, which is what the null return in SolveSystem was reporting as nothing
at all. It is now answered with a free parameter, the way the trigonometric
solvers already answer sin(x) = 0 with n_1:
{ x - y = 0, 2x - 2y = 0 }.Solve(x, y) [[t_1, t_1]]
{ x + y - 1, 2x + 2y - 2 }.Solve(x, y) [[t_1, 1 - t_1]]
null still means there are no solutions, which is the answer for a system that
contradicts itself.
The system in the report solves on master already, in all four combinations of
the two equation orders and the two ways of writing the ninth equation; a test
pins that, since a cosmetic rewrite deciding whether it solved is what was
reported. Nine of the twenty-five new tests fail without this change.
3905 unit tests and 127 F# tests pass, corpus unchanged at 85/117 with no wrong
answers, and the property checker's 1320 checks are clean.
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## master #679 +/- ##
==========================================
- Coverage 80.99% 80.09% -0.90%
==========================================
Files 155 156 +1
Lines 13687 12652 -1035
Branches 1957 2069 +112
==========================================
- Hits 11086 10134 -952
+ Misses 1990 1921 -69
+ Partials 611 597 -14 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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
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 #550.
@Happypig375 — you said the null-returning line is the one to be fixed, so this is about that line and not about a 3x3 example. What follows is where the null comes from.
The line, and what reaches it
SolveSystemreturnsnullwhenInSolveSystemhands back nothing. It gets nothing because an equation that has stopped constraining the variable is reported as having no solutions, when it has all of them.The second is a wrong answer rather than a missing one.
GatherMonomialInformationcollectsxand-xinto a single monomial of degree one whose coefficient is1 + (-1), and nothing ever looks at that coefficient — so the equation is read as1 * xand solved for the root0.That is what the report is about. Substituting one variable routinely leaves an equation that cancels away, and then:
which is a solution but not the solution set — every
x = yis one.What this changes
Coefficients that evaluate to zero are dropped before the degree is read. When none is left the equation is an identity, and it is answered with
Crather than the empty set. This also stops a cancelled leading term being counted towards the degree.The branch that already knew about this now decides. It carried the comment
in this case there is either 0 or +oo solutionsand returned the empty set for both; it now looks at whether what is left is zero.A free variable in a system gets a parameter instead of ending the search, the way
sin(x) = 0is already answered withn_1:nullnow means what it says in the doc comment: there are no solutions. That is still the answer for a system that contradicts itself, e.g.{ x + y - 1, x + y - 2 }.What this does not change
A variable mentioned in no equation at all still ends in
null, because dropping it leaves more equations than unknowns and the recursion is built on the two being equal. That belongs with #212 and I have not touched it here.On the reported system
The 13-equation system in the report solves on
mastertoday — in both of the equation orders and both of the ways of writing the ninth equation that the reporter tried.TheReportedSystemSolvesWhicheverWayItIsWrittenpins all four combinations, since a cosmetic rewrite deciding whether it solved is the complaint. It is a pin, not a demonstration of this fix; the nine tests that do fail without the change are marked below.Verification
EveryValueSatisfiesAnIdentityx6,ARepeatedEquationLeavesAFreeParameterx3).Simplifying the residual to exactly0, so they hold for every value of the parameter rather than at a sample point.masterand on this branch with the same harness.