Changed definition of [sub] to require proof that the modulus multiple actually is a multiple of the modulus. This allows for proving the Proper properties of [sub] based on its correctness proof alone, which has the modulus multiple correctness as a precondition.

3 files changed, 25 insertions, 21 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 6534c31b5..28ae5836b 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -35,7 +35,9 @@ Section ModularBaseSystem.
   Definition mul (us vs : digits) : digits := from_list (mul [[us]] [[vs]])
     (length_mul length_to_list length_to_list).
 
-  Definition sub (modulus_multiple us vs : digits) : digits :=
+  Definition sub (modulus_multiple: digits)
+                 (modulus_multiple_correct : decode modulus_multiple = 0%F)
+                 (us vs : digits) : digits :=
    from_list (sub [[modulus_multiple]] [[us]] [[vs]])
    (length_sub length_to_list length_to_list length_to_list).
 
@@ -43,8 +45,10 @@ Section ModularBaseSystem.
 
   Definition one : digits := encode (F.of_Z _ 1).
 
-  Definition opp (modulus_multiple x : digits) :
-    digits := sub modulus_multiple zero x.
+  Definition opp (modulus_multiple : digits)
+                 (modulus_multiple_correct : decode modulus_multiple = 0%F)
+                 (x : digits) :
+    digits := sub modulus_multiple modulus_multiple_correct zero x.
 
   Definition pow (x : digits) (chain : list (nat * nat)) : digits :=
     fold_chain one mul chain (x :: nil).
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 31fab7cd8..28ff29081 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -428,7 +428,7 @@ Section Subtraction.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient}.
   Local Notation digits := (tuple Z (length limb_widths)).
 
-  Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff us vs }.
+  Definition sub_opt_sig (us vs : digits) : { b : digits | b = sub coeff coeff_mod us vs }.
   Proof.
     eexists.
     cbv [BaseSystem.add ModularBaseSystem.sub BaseSystem.sub].
@@ -439,10 +439,10 @@ Section Subtraction.
     := Eval cbv [proj1_sig sub_opt_sig] in proj1_sig (sub_opt_sig us vs).
 
   Definition sub_opt_correct us vs
-    : sub_opt us vs = sub coeff us vs
+    : sub_opt us vs = sub coeff coeff_mod us vs
     := proj2_sig (sub_opt_sig us vs).
 
-  Definition opp_opt_sig (us : digits) : { b : digits | b = opp coeff us }.
+  Definition opp_opt_sig (us : digits) : { b : digits | b = opp coeff coeff_mod us }.
   Proof.
     eexists.
     cbv [opp].
@@ -454,7 +454,7 @@ Section Subtraction.
     := Eval cbv [proj1_sig opp_opt_sig] in proj1_sig (opp_opt_sig us).
 
   Definition opp_opt_correct us
-    : opp_opt us = opp coeff us
+    : opp_opt us = opp coeff coeff_mod us
     := proj2_sig (opp_opt_sig us).
   
 End Subtraction.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 371da7767..1369bbbf1 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -189,23 +189,20 @@ Section FieldOperationProofs.
     apply F.to_Z_of_Z.
   Qed.
 
-  Section Subtraction.
-  Context (mm : digits) (mm_spec : decode mm = 0%F).
-
-  Lemma sub_rep : forall u v x y, u ~= x -> v ~= y ->
-    ModularBaseSystem.sub mm u v ~= (x-y)%F.
+  Lemma sub_rep : forall mm pf u v x y, u ~= x -> v ~= y ->
+    ModularBaseSystem.sub mm pf u v ~= (x-y)%F.
   Proof.
     autounfold; cbv [sub]; intros.
     rewrite to_list_from_list; autounfold.
     cbv [ModularBaseSystemList.sub].
     rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep.
     rewrite F.of_Z_sub, F.of_Z_add, F.of_Z_mod.
-    apply Fdecode_decode_mod in mm_spec; cbv [BaseSystem.decode] in *.
-    rewrite mm_spec. rewrite Algebra.left_identity.
+    apply Fdecode_decode_mod in pf; cbv [BaseSystem.decode] in *.
+    rewrite pf. rewrite Algebra.left_identity.
     f_equal; assumption.
   Qed.
 
-  Lemma opp_rep : forall u x, u ~= x -> opp mm u ~= F.opp x.
+  Lemma opp_rep : forall mm pf u x, u ~= x -> opp mm pf u ~= F.opp x.
   Proof.
     cbv [opp rep]; intros.
     rewrite sub_rep by (apply encode_rep || eassumption).
@@ -217,7 +214,6 @@ Section FieldOperationProofs.
       [ rewrite F.of_Z_sub, F.of_Z_to_Z; reflexivity | ].
     rewrite F.to_Z_of_Z. reflexivity.
   Qed.
-  End Subtraction.
 
   Section PowInv.
   Context (modulus_gt_2 : 2 < modulus).
@@ -272,11 +268,16 @@ Section FieldOperationProofs.
     erewrite !add_rep; cbv [rep] in *; try reflexivity; assumption.
   Qed.
   
-  Global Instance sub_Proper : Proper (eq ==> eq ==> eq ==> eq) sub.
+  Global Instance sub_Proper mm mm_correct
+    : Proper (eq ==> eq ==> eq) (sub mm mm_correct).
   Proof.
-  Admitted.
+    repeat intro.
+    cbv beta delta [eq] in *.
+    erewrite !sub_rep; cbv [rep] in *; try reflexivity; assumption.
+  Qed.
   
-  Global Instance opp_Proper : Proper (eq ==> eq ==> eq) opp.
+  Global Instance opp_Proper mm mm_correct
+    : Proper (eq ==> eq) (opp mm mm_correct).
   Proof.
      cbv [opp]; repeat intro.
      apply sub_Proper; assumption || reflexivity.
@@ -289,7 +290,6 @@ Section FieldOperationProofs.
     erewrite !mul_rep; cbv [rep] in *; try reflexivity; assumption.
   Qed.
 
-  Check pow.
   Global Instance pow_Proper : Proper (eq ==> Logic.eq ==> eq) pow.
   Proof.
     repeat intro.
@@ -322,7 +322,7 @@ Section FieldOperationProofs.
   Qed.
 
   Lemma modular_base_system_field :
-    @field digits eq zero one (opp coeff) add (sub coeff) mul (inv chain chain_correct) div.
+    @field digits eq zero one (opp coeff coeff_mod) add (sub coeff coeff_mod) mul (inv chain chain_correct) div.
   Proof.
     eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := @F.field_modulo modulus prime_modulus)).
     Grab Existential Variables.