Twisted-edwards-neg-inverse
Property that negation is left and right inverse for addition.
The proof is very simple on paper,
looking at the formula for addition:
the abscissa is (xy-yx)/\ldots, i.e. 0;
the ordinate is (yy+axx)/(1-dxxyy),
but yy+axx = 1+dxxyy because the point is on the curve,
and thus the ordinate is 1,
since the denominators are known to be non-0 in the addition formula.
The prime field rules get the part about the abscissa,
since it follows a simplifying rewriting pattern.
For the ordinate, enabling div makese things worse,
splitting the fraction into two
(i.e. the direction of the rules is not appropriate
for this part of the proof).
Leaving div disabled prevents that,
and the hypothesis that the point is on the curve
turns the numerator into more or less the same term as the denominator.
We use the rule div-of-same to simplify that to 1,
but that rule requires the common term to be non-0.
We instantiate the general theorem about the denominator being non-0
to prove that the specific term is not 0.
Because of the term reordering done by the rules,
the general theorem about the denominator does not readily apply here;
but we need those rules to prove the abscissa to be 0,
so this is another case in which different part of the same proof
need different rules, necessitating some user guidance.
Once we prove the left inverse theorem,
the right inverse theorem follows by commutativity,
but we need a :use hint because
commutativity rewrites in the other direction.
Definitions and Theorems
Theorem: twisted-edwards-add-of-neg-left
(defthm twisted-edwards-add-of-neg-left
(implies
(and (twisted-edwards-curve-completep curve)
(point-on-twisted-edwards-p point curve))
(equal (twisted-edwards-add (twisted-edwards-neg point curve)
point curve)
(twisted-edwards-zero))))
Theorem: twisted-edwards-add-of-neg-right
(defthm twisted-edwards-add-of-neg-right
(implies
(and (twisted-edwards-curve-completep curve)
(point-on-twisted-edwards-p point curve))
(equal
(twisted-edwards-add point (twisted-edwards-neg point curve)
curve)
(twisted-edwards-zero))))