re-cleaned operations in Specific and updated GF25519 to match GF1305

2 files changed, 115 insertions, 78 deletions

diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 5fefcae24..2bc42b68e 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -53,104 +53,78 @@ Definition fe1305 : Type := Eval cbv in fe.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In phi.
 
-
-
-Definition add_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) :
-  { fg | fg = ModularBaseSystemInterface.add (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }.
+Definition add_sig (f g : fe1305) :
+  { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}.
 Proof.
+  cbv [fe1305] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
   cbv.
   reflexivity.
 Defined.
 
-Definition add_formula_correct := Eval cbv [proj2_sig] in
-(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (add_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)).
-
-Definition add (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig add_formula_sig] in 
-  let (f03, f4) := f   in
-  let (f02, f3) := f03 in
-  let (f01, f2) := f02 in
-  let (f0, f1)  := f01 in
-  let (g03, g4) := g   in
-  let (g02, g3) := g03 in
-  let (g01, g2) := g02 in
-  let (g0, g1)  := g01 in
-  proj1_sig (add_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4).
-
-Definition add_correct f g : add f g = ModularBaseSystemInterface.add f g.
+Definition add (f g : fe1305) : fe1305 :=
+  Eval cbv beta iota delta [proj1_sig add_sig] in
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj1_sig (add_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
+
+Definition add_correct (f g : fe1305)
+  : add f g = ModularBaseSystemInterface.add f g :=
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj2_sig (add_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
+
+Definition sub_sig (f g : fe1305) :
+  { fg : fe1305 | fg = ModularBaseSystemInterface.sub f g}.
 Proof.
   cbv [fe1305] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
-  rewrite <-add_formula_correct.
-  reflexivity.
-Qed.
-
-Definition sub_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) :
-  { fg | fg = ModularBaseSystemInterface.sub (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }.
-Proof.
   eexists.
   cbv.
   reflexivity.
 Defined.
 
-Definition sub_formula_correct := Eval cbv [proj2_sig] in
-(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (sub_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)).
-
-Definition sub (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig sub_formula_sig] in 
-  let (f03, f4) := f   in
-  let (f02, f3) := f03 in
-  let (f01, f2) := f02 in
-  let (f0, f1)  := f01 in
-  let (g03, g4) := g   in
-  let (g02, g3) := g03 in
-  let (g01, g2) := g02 in
-  let (g0, g1)  := g01 in
-  proj1_sig (sub_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4).
-
-Definition sub_correct f g : sub f g = ModularBaseSystemInterface.sub f g.
+Definition sub (f g : fe1305) : fe1305 :=
+  Eval cbv beta iota delta [proj1_sig sub_sig] in
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj1_sig (sub_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
+
+Definition sub_correct (f g : fe1305)
+  : sub f g = ModularBaseSystemInterface.sub f g :=
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj2_sig (sub_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
+
+Definition mul_sig (f g : fe1305) :
+  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
   cbv [fe1305] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
-  rewrite <-sub_formula_correct.
-  reflexivity.
-Qed.
-
-Definition mul_formula_sig (f0 f1 f2 f3 f4 g0 g1 g2 g3 g4: Z) :
-  { fg | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4) }.
-Proof.
   eexists.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
 Defined.
 
-Definition mul_formula_correct := Eval cbv [proj2_sig] in
-(fun f0 f1 f2 f3 f4 g0 g1 g2 g3 g4 => proj2_sig (mul_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4)).
-
-Definition mul (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig mul_formula_sig] in 
-  let (f03, f4) := f   in
-  let (f02, f3) := f03 in
-  let (f01, f2) := f02 in
-  let (f0, f1)  := f01 in
-  let (g03, g4) := g   in
-  let (g02, g3) := g03 in
-  let (g01, g2) := g02 in
-  let (g0, g1)  := g01 in
-  proj1_sig (mul_formula_sig f0 f1 f2 f3 f4 g0 g1 g2 g3 g4).
-
-Definition mul_correct f g : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g.
-Proof.
-  cbv [fe1305] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
-  rewrite <-mul_formula_correct.
-  reflexivity.
-Qed.
+Definition mul (f g : fe1305) : fe1305 :=
+  Eval cbv beta iota delta [proj1_sig mul_sig] in
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj1_sig (mul_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
+
+Definition mul_correct (f g : fe1305)
+  : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  let '(f0,f1,f2,f3,f4) := f in
+  let '(g0,g1,g2,g3,g4) := g in
+  proj2_sig (mul_sig (f0,f1,f2,f3,f4) (g0,g1,g2,g3,g4)).
 
 Import Morphisms.
 
 Lemma field1305 : @field fe eq zero one opp add sub mul inv div.
 Proof.
-  pose proof Equivalence_Reflexive.
+  pose proof (Equivalence_Reflexive : Reflexive eq).
   eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)).
   Grab Existential Variables.
   + reflexivity.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index a361e7207..261b6f4fe 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -2,11 +2,12 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
-Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface.
 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 Algebra.
 Import ListNotations.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Require Import Crypto.Util.Notations.
@@ -48,29 +49,91 @@ Definition fe25519 : Type := Eval cbv in fe.
 
 Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In.
 
-Definition add (f g:fe25519) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
+Definition add_sig (f g : fe25519) :
+  { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}.
 Proof.
   cbv [fe25519] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
-  rewrite <-add_phi.
-  apply f_equal.
   cbv.
   reflexivity.
-Qed.
+Defined.
+
+Definition add (f g : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig add_sig] in
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj1_sig (add_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
+
+Definition add_correct (f g : fe25519)
+  : add f g = ModularBaseSystemInterface.add f g :=
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj2_sig (add_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
 
-Definition mul (f g:fe25519) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
+Definition sub_sig (f g : fe25519) :
+  { fg : fe25519 | fg = ModularBaseSystemInterface.sub f g}.
+Proof.
+  cbv [fe25519] in *.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  eexists.
+  cbv.
+  reflexivity.
+Defined.
+
+Definition sub (f g : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig sub_sig] in
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj1_sig (sub_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
+
+Definition sub_correct (f g : fe25519)
+  : sub f g = ModularBaseSystemInterface.sub f g :=
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj2_sig (sub_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
+
+Definition mul_sig (f g : fe25519) :
+  { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
   cbv [fe25519] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
-  rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst.
-  apply f_equal.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
+Defined.
+
+Definition mul (f g : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig mul_sig] in
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj1_sig (mul_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
+
+Definition mul_correct (f g : fe25519)
+  : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  let '(f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) := f in
+  let '(g0,g1,g2,g3,g4,g5,g6,g7,g8,g9) := g in
+  proj2_sig (mul_sig (f0,f1,f2,f3,f4,f5,f6,f7,f8,f9) (g0,g1,g2,g3,g4,g5,g6,g7,g8,g9)).
+
+Import Morphisms.
+
+Lemma field25519 : @field fe25519 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)).
+  Grab Existential Variables.
+  + reflexivity.
+  + reflexivity.
+  + reflexivity.
+  + intros; rewrite mul_correct; reflexivity.
+  + intros; rewrite sub_correct; reflexivity.
+  + intros; rewrite add_correct; reflexivity.
+  + reflexivity.
+  + reflexivity.
 Qed.
 
+
 (*
 Local Transparent Let_In.
 Eval cbv iota beta delta [proj1_sig mul Let_In] in (fun f0 f1 f2 f3 f4  g0 g1 g2 g3 g4 => proj1_sig (mul (f4,f3,f2,f1,f0) (g4,g3,g2,g1,g0))).