The RingSolver fails to solve some equations #513
Comments
felixwellen
added a commit
to felixwellen/cubical
that referenced
this issue
Mar 26, 2021
felixwellen
added a commit
to felixwellen/cubical
that referenced
this issue
Mar 26, 2021
…malization-proof
mortberg
pushed a commit
that referenced
this issue
Aug 18, 2021
* Issue #513: Write an example that fails * Issue #513: Add missing simplification, open new goals in the normalization-proof * Prove that the new zero-detection is compatible with evaluation * Add computation for evaluation, to abstract over cases * Refactor * Refactor * Prove homomorphism property for + * Prove homomorphism property for + * Remove obsolete * Refactor * Prove lemmata * Refactor, new Utility * Eval is homomorphic for scalar multiplication * Refactor * Eval is homomorphic for \cdot * Fix * Update comment * More examples * Whitespace * Whitespace * Remove obsolete options * Refactor rename
|
Solved by #530. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I found two examples of equations the RingSolver fails to solve:
x · 0r ≡ 0r
and
x · (y - z) ≡ x · y - x · z
Since the examples are small, it should be easy to find the problem and fix it. My guess is, that in the definition of the multiplication of HornerForms, an additional special case has to be considered.
The text was updated successfully, but these errors were encountered: