		Search-engine friendly clone of the ACL2 documentation.

Montgomery

Montgomery-sub

Subtraction of two points of the Montgomery group.

Signature
(montgomery-sub point1 point2 curve) → point
Arguments: point1 — Guard (pointp point1).; point2 — Guard (pointp point2).; curve — Guard (montgomery-curvep curve).
Returns: point — Type (pointp point).

This is, as usual in groups, essentially an abbreviation for adding the first point to the negation of the second point.

Definitions and Theorems

Function: montgomery-sub

(defun montgomery-sub (point1 point2 curve)
 (declare (xargs :guard (and (pointp point1)
                             (pointp point2)
                             (montgomery-curvep curve))))
 (declare (xargs :guard (and (point-on-montgomery-p point1 curve)
                             (point-on-montgomery-p point2 curve))))
 (let ((acl2::__function__ 'montgomery-sub))
   (declare (ignorable acl2::__function__))
   (montgomery-add point1 (montgomery-neg point2 curve)
                   curve)))

Theorem: pointp-of-montgomery-sub

(defthm pointp-of-montgomery-sub
  (b* ((point (montgomery-sub point1 point2 curve)))
    (pointp point))
  :rule-classes :rewrite)

Theorem: montgomery-sub-of-point-fix-point1

(defthm montgomery-sub-of-point-fix-point1
  (equal (montgomery-sub (point-fix point1)
                         point2 curve)
         (montgomery-sub point1 point2 curve)))

Theorem: montgomery-sub-point-equiv-congruence-on-point1

(defthm montgomery-sub-point-equiv-congruence-on-point1
  (implies (point-equiv point1 point1-equiv)
           (equal (montgomery-sub point1 point2 curve)
                  (montgomery-sub point1-equiv point2 curve)))
  :rule-classes :congruence)

Theorem: montgomery-sub-of-point-fix-point2

(defthm montgomery-sub-of-point-fix-point2
  (equal (montgomery-sub point1 (point-fix point2)
                         curve)
         (montgomery-sub point1 point2 curve)))

Theorem: montgomery-sub-point-equiv-congruence-on-point2

(defthm montgomery-sub-point-equiv-congruence-on-point2
  (implies (point-equiv point2 point2-equiv)
           (equal (montgomery-sub point1 point2 curve)
                  (montgomery-sub point1 point2-equiv curve)))
  :rule-classes :congruence)

Theorem: montgomery-sub-of-montgomery-curve-fix-curve

(defthm montgomery-sub-of-montgomery-curve-fix-curve
  (equal (montgomery-sub point1
                         point2 (montgomery-curve-fix curve))
         (montgomery-sub point1 point2 curve)))

Theorem: montgomery-sub-montgomery-curve-equiv-congruence-on-curve

(defthm montgomery-sub-montgomery-curve-equiv-congruence-on-curve
  (implies (montgomery-curve-equiv curve curve-equiv)
           (equal (montgomery-sub point1 point2 curve)
                  (montgomery-sub point1 point2 curve-equiv)))
  :rule-classes :congruence)