Montgomery-add-commutativity
Commutativity of Montgomery addition.
This is easy when at least one of the points is the one at infinity.
When the two points are both finite,
there are two cases, according to the definition of addition:
either the points have the same x or not.
If they do, we know from theorem
montgomery-points-with-same-x-have-same-or-neg-y
that the y are either the same or inverses:
if they are inverses, they are still inverses if swapped,
and the result is the point at infinite in both cases,
so commutativity holds;
if they are the same, then the two points are the same
and commutativity clearly holds.
The more elaborate case is when the two points have different x.
Looking at the formula to compute the addition,
first note that \lambda does not change if the points are swapped,
because the swapping negates both dividend and divisor,
and the negations simplify away.
The x of the addition is obtained by combining \lambda
with A and B and the two xs of the points:
the latter are both subtracted,
and if swapped the final result is the same.
So addition commutes at least for the x coordinate.
For the y of the addition, things are a bit more complex:
it is not immediately clear that
\lambda (x_1 - x_3) - y_1 = \lambda (x_2 - x_3) - y_2,
where we write \lambda for both because that part commutes,
as explained above.
If we distribute \lambda over (x_1 - x_3) and (x_2 - x_3),
we see that \lambda x_3 is the same for both,
so we are left with showing
\lambda x_1 - y_1 = \lambda x_2 - y_2.
Expanding \lambda
and extending the fraction to y-1 and y_2,
things simplify and both reduce to the same
\frac{x_1 y_2 - x_2 y_1}{x_2 - x_1},
thus ensuring commutativity.
To carry out the argument above for the case of different xs,
we introduce local functions that define
\lambda, x_3, and y_2,
show they commute,
show them equivalent to montgomery-add under suitable conditions,
and thus conclude the commutativity under those conditions,
which together with the commutativity theorems under other conditions,
allow us to conclude commutativity under all conditions.
Definitions and Theorems
Theorem: montgomery-add-commutative
(defthm montgomery-add-commutative
(implies (and (point-on-montgomery-p point1 curve)
(point-on-montgomery-p point2 curve))
(equal (montgomery-add point1 point2 curve)
(montgomery-add point2 point1 curve))))
