Shifted around some of the proofs in ModularBaseSystemField.v and propagated field proof through GF1305.v as a proof of concept; working towards deleting that ModularBaseSystemField.v

2 files changed, 76 insertions, 10 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index c062a232b..d26422bcf 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -20,11 +20,6 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z.
 
-Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
-  coeff : tuple Z (length limb_widths);
-  coeff_mod: decode coeff = 0%F
-}.
-
 (* Computed versions of some functions. *)
 
 Definition plus_opt := Eval compute in plus.
@@ -411,7 +406,7 @@ Section Carries.
 End Carries.
 
 Section Addition.
-  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient}.
   Local Notation digits := (tuple Z (length limb_widths)).
 
   Definition add_opt_sig (us vs : digits) : { b : digits | b = add us vs }.
@@ -429,7 +424,7 @@ Section Addition.
 End Addition.
 
 Section Subtraction.
-  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}.
+  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 }.
@@ -448,7 +443,7 @@ Section Subtraction.
 End Subtraction.
 
 Section Multiplication.
-  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} {cc : CarryChain limb_widths}
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient} {cc : CarryChain limb_widths}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
   Local Notation digits := (tuple Z (length limb_widths)).
@@ -740,7 +735,7 @@ Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos
     c_reduce1 c_reduce2 two_pow_k_le_2modulus.
 
 Section Canonicalization.
-  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm}
+  Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_)
     {int_width} (preconditions : freezePreconditions prm int_width).
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 4543cde2e..5c9bdc52c 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -30,6 +30,17 @@ Class CarryChain (limb_widths : list Z) :=
     carry_chain_valid : forall i, In i carry_chain -> (i < length limb_widths)%nat
   }.
 
+  Class SubtractionCoefficient {m : Z} {prm : PseudoMersenneBaseParams m} := {
+    coeff : tuple Z (length limb_widths);
+    coeff_mod: decode coeff = 0%F
+  }.
+
+  Class InvExponentiationChain {m : Z} {prm : PseudoMersenneBaseParams m} := {
+    chain : list (nat * nat);
+    chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (m - 2)
+  }.
+
+
 Section FieldOperationProofs.
   Context `{prm :PseudoMersenneBaseParams}.
 
@@ -194,7 +205,7 @@ Section FieldOperationProofs.
     f_equal; assumption.
   Qed.
   End Subtraction.
-  
+
   Section PowInv.
   Context (modulus_gt_2 : 2 < modulus).
 
@@ -229,7 +240,67 @@ Section FieldOperationProofs.
     etransitivity; [ apply pow_rep; eassumption | ].
     congruence.
   Qed.
+
   End PowInv.
+
+
+  Import Morphisms.
+
+  Global Instance encode_Proper : Proper (Logic.eq ==> eq) encode.
+  Proof.
+    repeat intro; cbv [eq].
+    rewrite !encode_rep. assumption.
+  Qed.
+
+  Global Instance opp_Proper : Proper (eq ==> eq) opp.
+  Admitted.
+
+  Global Instance add_Proper : Proper (eq ==> eq ==> eq) add.
+  Admitted.
+
+  Global Instance sub_Proper : Proper (eq ==> eq ==> eq ==> eq) sub.
+  Admitted.
+  
+  Global Instance mul_Proper : Proper (eq ==> eq ==> eq) mul.
+  Admitted.
+
+  Global Instance inv_Proper chain chain_correct : Proper (eq ==> eq) (inv chain chain_correct).
+  Admitted.
+
+  Global Instance div_Proper : Proper (eq ==> eq ==> eq) div.
+  Admitted.
+
+
+  Section FieldProofs.
+  Context (modulus_gt_2 : 2 < modulus)
+          {sc : SubtractionCoefficient}
+          {ic : InvExponentiationChain}.
+
+  Lemma _zero_neq_one : not (eq zero one).
+  Proof.
+    cbv [eq zero one]; erewrite !encode_rep.
+    pose proof (@F.field_modulo modulus prime_modulus).
+    apply zero_neq_one.
+  Qed.
+
+  Lemma modular_base_system_field :
+    @field digits eq zero one opp add (sub coeff) 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.
+    + intros; eapply encode_rep.
+    + intros; eapply encode_rep.
+    + intros; eapply encode_rep.
+    + intros; eapply inv_rep; auto.
+    + intros; eapply mul_rep; auto.
+    + intros; eapply sub_rep; auto using coeff_mod.
+    + intros; eapply add_rep; auto.
+    + intros; eapply encode_rep.
+    + eapply _zero_neq_one.
+    + trivial.
+  Qed.
+  End FieldProofs.
+  
 End FieldOperationProofs.
 Opaque encode add mul sub inv pow.