restructured ModularBaseSystem pipeline to put tuple conversion before ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt

1 files changed, 51 insertions, 29 deletions

diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 077c98954..9e9b69dbd 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -1,13 +1,14 @@
-Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.ModularBaseSystem.
+Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
 Require Import Coq.Lists.List Crypto.Util.ListUtil.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.BaseSystem.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Algebra.
 Import ListNotations.
@@ -26,12 +27,13 @@ Instance params1305 : PseudoMersenneBaseParams modulus.
   construct_params prime_modulus 5%nat 130.
 Defined.
 
-Definition mul2modulus := Eval compute in (construct_mul2modulus params1305).
+Definition fe1305 := Eval compute in (tuple Z (length limb_widths)).
+
+Definition mul2modulus : fe1305 :=
+  Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params1305)).
 
 Instance subCoeff : SubtractionCoefficient modulus params1305.
   apply Build_SubtractionCoefficient with (coeff := mul2modulus).
-  cbv; auto.
-  cbv [ModularBaseSystem.decode].
   apply ZToField_eqmod.
   cbv; reflexivity.
 Defined.
@@ -49,9 +51,7 @@ Definition c_ := Eval compute in c.
 Definition k_subst : k = k_ := eq_refl k_.
 Definition c_subst : c = c_ := eq_refl c_.
 
-Definition fe1305 : Type := Eval cbv in fe.
-
-Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi.
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
 Definition app_5 (f : fe1305) (P : fe1305 -> fe1305) : fe1305.
 Proof.
@@ -80,7 +80,7 @@ Proof.
 Qed.
 
 Definition add_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.add f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct. (* Coq 8.4 : 6s *)
@@ -93,12 +93,12 @@ Definition add (f g : fe1305) : fe1305 :=
   proj1_sig (add_sig f g).
 
 Definition add_correct (f g : fe1305)
-  : add f g = ModularBaseSystemInterface.add f g :=
+  : add f g = ModularBaseSystem.add f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (add_sig f g). (* Coq 8.4 : 10s *)
 
 Definition sub_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.sub f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.sub mul2modulus f g}.
 Proof.
   eexists.
   rewrite <-appify2_correct.
@@ -111,16 +111,19 @@ Definition sub (f g : fe1305) : fe1305 :=
   proj1_sig (sub_sig f g).
 
 Definition sub_correct (f g : fe1305)
-  : sub f g = ModularBaseSystemInterface.sub f g :=
+  : sub f g = ModularBaseSystem.sub mul2modulus f g :=
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *)
 
+(* For multiplication, we add another layer of definition so that we can
+   rewrite under the [let] binders. *)
 Definition mul_simpl_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.mul f g}.
 Proof.
   cbv [fe1305] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
+  rewrite <-mul_opt_correct with (k_ := k_) (c_ := c_) by auto.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
@@ -131,18 +134,17 @@ Definition mul_simpl (f g : fe1305) : fe1305 :=
   proj1_sig (mul_simpl_sig f g).
 
 Definition mul_simpl_correct (f g : fe1305)
-  : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  : mul_simpl f g = ModularBaseSystem.mul f g :=
   Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
   proj2_sig (mul_simpl_sig f g).
 
 Definition mul_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+  { fg : fe1305 | fg = ModularBaseSystem.mul f g}.
 Proof.
   eexists.
   rewrite <-mul_simpl_correct.
   rewrite <-appify2_correct.
   cbv.
-  autorewrite with zsimplify.
   reflexivity.
 Defined. (* Coq 8.4 : 14s *)
 
@@ -151,25 +153,45 @@ Definition mul (f g : fe1305) : fe1305 :=
   proj1_sig (mul_sig f g).
 
 Definition mul_correct (f g : fe1305)
-  : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  : mul f g = ModularBaseSystem.mul f g :=
   Eval cbv beta iota delta [proj1_sig add_sig] in
   proj2_sig (mul_sig f g). (* Coq 8.4 : 5s *)
 
+Definition decode := Eval compute in ModularBaseSystem.decode.
+
 Import Morphisms.
 
-Lemma field1305 : @field fe eq zero one opp add sub mul inv div.
+Lemma field1305 : @field fe1305 eq zero one opp add sub mul inv div.
 Proof.
   pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)).
+  eapply (Field.isomorphism_to_subfield_field (phi := decode)
+    (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))).
   Grab Existential Variables.
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  + intros; rewrite mul_correct; reflexivity.
-  + intros; rewrite sub_correct; reflexivity.
-  + intros; rewrite add_correct; reflexivity.
-  + reflexivity.
-  + reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite mul_correct; apply mul_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite sub_correct; apply sub_rep; try reflexivity.
+    rewrite <- coeff_mod. reflexivity.
+  + intros; change decode with ModularBaseSystem.decode.
+    rewrite add_correct; apply add_rep; reflexivity.
+  + intros; change decode with ModularBaseSystem.decode; apply encode_rep.
+  + cbv [eq zero one]. change decode with ModularBaseSystem.decode.
+    rewrite !encode_rep. intro A.
+    eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence.
+  + trivial.
+  + repeat intro. cbv [div]. congruence.
+  + repeat intro. cbv [inv]. congruence.
+  + repeat intro. cbv [eq] in *. rewrite !mul_correct, !mul_rep by reflexivity; congruence.
+  + repeat intro. cbv [eq] in *. rewrite !sub_correct. rewrite !sub_rep by
+      (rewrite <-?coeff_mod; reflexivity); congruence.
+  + repeat intro. cbv [eq] in *. rewrite !add_correct, !add_rep by reflexivity; congruence.
+  + repeat intro. cbv [opp]. congruence.
+  + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
+  + apply (eq_Equivalence (prm := params1305)).
 Qed.
 
 (*