cleaned Specific operations so they produce code without proof terms, and proved that GF1305 is a field

1 files changed, 89 insertions, 17 deletions

diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index e539eaa8d..5fefcae24 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -53,43 +53,115 @@ 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 (f g:fe1305) : { fg | phi fg = @ModularArithmetic.add modulus (phi f) (phi g) }.
+
+
+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) }.
 Proof.
-  cbv [fe1305] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
-  rewrite <-add_phi.
   cbv.
-  apply f_equal.
   reflexivity.
-Qed.
-Definition add f g := proj1_sig (add_formula f g).
+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 sub_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.sub modulus (phi f) (phi g) }.
+Definition add_correct f g : add f g = ModularBaseSystemInterface.add 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.
-  rewrite <-sub_phi.
   cbv.
-  apply f_equal.
   reflexivity.
-Qed.
-Definition sub f g := proj1_sig (sub_formula f g).
+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 mul_formula (f g:fe1305) : { fg | phi fg = @ModularArithmetic.mul modulus (phi f) (phi g) }.
+Definition sub_correct f g : sub f g = ModularBaseSystemInterface.sub 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.
-  rewrite <-(mul_phi (c_ := c_) (k_ := k_)) by auto using k_subst,c_subst.
   cbv.
-  apply f_equal.
   autorewrite with zsimplify.
-  repeat match goal with |- appcontext[?a * 1] => rewrite (Z.mul_1_r a) end.
   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.
+
+Import Morphisms.
+
+Lemma field1305 : @field fe eq zero one opp add sub mul inv div.
+Proof.
+  pose proof Equivalence_Reflexive.
+  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.
-Definition mul f g := proj1_sig (mul_formula f g).
 
 (*
 Local Transparent Let_In.