|
|
|---|
|
|
|
|---|
Assumption of closure of Montgomery addition.
We plan to prove the closure of montgomery-add, but since that will take a bit of work, for now we capture the closure property in this nullary predicate, which we can use as hypothesis in theorems whose proof needs closure. This is preferable to stating an axiom, because an incorrect axiom (either because it is misstated or because addition is misdefined) would make the logic inconsistent. In contrast, if this nullary predicate is actually false (due to the same kind of mistake mentioned just above), it just means that any theorem with it as hypothesis is vacuous (a much less severe problem).
We enable the rewrite rule associated to this defun-sk because it is essentially the closure theorem, which is a good rewrite rule to have enabled, with the only difference that it has this nullary predicate as hypothesis.
Theorem:
(defthm montgomery-add-closure-necc (implies (montgomery-add-closure) (implies (and (point-on-montgomery-p point1 curve) (point-on-montgomery-p point2 curve)) (point-on-montgomery-p (montgomery-add point1 point2 curve) curve))))
Theorem:
(defthm booleanp-of-montgomery-add-closure (b* ((yes/no (montgomery-add-closure))) (booleanp yes/no)) :rule-classes :rewrite)