Distributivity of scalar multiplication over scalar addition.
We first prove it on twisted-edwards-mul-nonneg by induction, then we lift it to twisted-edwards-mul, but only for non-negative scalars. To extend it to negative scalars, we consider different cases. If both scalars are non-positive, the definition of twisted-edwards-mul is expanded, and the theorem about twisted-edwards-mul-nonneg applies. If one is non-negative and the other non-positive, we consider two subcases: when the sum is non-negative, and when the sum is non-positive. The first subcase requires adding and subtracting the same quantity, and thus we use Isar to explicate this proof strategy. The second subcase is proved by considering the negated scalars and thus applying the theorem for the first subcase; we use Isar, but it might be possible to shorten the proof. Finally, the case in which one is non-positive and the other non-negative is handled by swapping the roles, and implicitly using commutativity. With all the cases in hand, we prove the main theorem, which applies to any integer scalars. We keep the theorem disabled, because distribution is not always desired.
Note that we consider non-negative and non-positive cases, which overlap at zero, rather than non-overlapping non-negative and negative cases. The overlap is intentional, so that the cases are more symmetric and it is easy to swap signs, as we do in some of the proofs.
Theorem:
(defthm twisted-edwards-mul-of-scalar-addition (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (integerp scalar1) (integerp scalar2)) (equal (twisted-edwards-mul (+ scalar1 scalar2) point curve) (twisted-edwards-add (twisted-edwards-mul scalar1 point curve) (twisted-edwards-mul scalar2 point curve) curve))))
Theorem:
(defthm twisted-edwards-mul-of-scalar-addition-converse (implies (and (twisted-edwards-add-associativity) (twisted-edwards-curve-completep curve) (pointp point) (point-on-twisted-edwards-p point curve) (integerp scalar1) (integerp scalar2)) (equal (twisted-edwards-add (twisted-edwards-mul scalar1 point curve) (twisted-edwards-mul scalar2 point curve) curve) (twisted-edwards-mul (+ scalar1 scalar2) point curve))))