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

1 files changed, 44 insertions, 70 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.