more changes to Specific for 8.4 compatibility

3 files changed, 102 insertions, 68 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index 998e7d959..c79dce1d3 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -17,21 +17,20 @@ Section s.
 
   Definition fe := tuple Z (length base).
 
+  Arguments to_list {_ _} _.
+
   Definition mul  (x y:fe) : fe :=
     carry_mul_opt_cps k_ c_ (from_list_default 0%Z (length base))
-      (to_list _ x) (to_list _ y).
+      (to_list x) (to_list y).
 
-  Definition add : fe -> fe -> fe.
-    refine (on_tuple2 add_opt _).
-    abstract (intros; rewrite add_opt_correct, add_length_exact; case_max; omega).
-  Defined.
+  Definition add (x y : fe) : fe :=
+    from_list_default 0%Z (length base) (add_opt (to_list x) (to_list y)).
 
   Definition sub : fe -> fe -> fe.
     refine (on_tuple2 sub_opt _).
     abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto).
   Defined.
 
-  Arguments to_list {_ _} _.
   Definition phi (a : fe) : ModularArithmetic.F m := decode (to_list a).
   Definition phi_inv (a : ModularArithmetic.F m) : fe :=
     from_list_default 0%Z _ (encode a).
@@ -72,9 +71,12 @@ Section s.
   Lemma add_correct : forall a b,
     to_list (add a b) = BaseSystem.add (to_list a) (to_list b).
   Proof.
-    intros; cbv [add on_tuple2].
-    rewrite to_list_from_list.
-    apply add_opt_correct.
+    intros; cbv [add].
+    rewrite add_opt_correct.
+    erewrite from_list_default_eq.
+    apply to_list_from_list.
+    Grab Existential Variables.
+    apply add_same_length; auto using length_to_list.
   Qed.
 
   Lemma add_phi : forall a b : fe,
@@ -125,22 +127,22 @@ Section s.
   Proof.
     eapply (Field.isomorphism_to_subfield_field (phi := phi) (fieldR := PrimeFieldTheorems.field_modulo  (prime_q := prime_modulus))).
     Grab Existential Variables.
-    + intros; apply phi_inv_spec.
-    + intros; apply phi_inv_spec.
-    + intros; apply phi_inv_spec.
-    + intros; apply phi_inv_spec.
-    + intros; apply mul_phi.
-    + intros; apply sub_phi.
-    + intros; apply add_phi.
-    + intros; apply phi_inv_spec.
-    + cbv [eq zero one]. rewrite !phi_inv_spec. intro A.
+    + intros; eapply phi_inv_spec.
+    + intros; eapply phi_inv_spec.
+    + intros; eapply phi_inv_spec.
+    + intros; eapply phi_inv_spec.
+    + intros; eapply mul_phi.
+    + intros; eapply sub_phi.
+    + intros; eapply add_phi.
+    + intros; eapply phi_inv_spec.
+    + cbv [eq zero one]. erewrite !phi_inv_spec. 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]. rewrite !mul_phi. congruence.
-    + repeat intro. cbv [eq]. rewrite !sub_phi. congruence.
-    + repeat intro. cbv [eq]. rewrite !add_phi. congruence.
+    + repeat intro. cbv [eq]. erewrite !mul_phi. congruence.
+    + repeat intro. cbv [eq]. erewrite !sub_phi. congruence.
+    + repeat intro. cbv [eq]. erewrite !add_phi. congruence.
     + repeat intro. cbv [opp]. congruence.
     + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec.
   Qed.
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 2bc42b68e..74f914616 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -53,72 +53,88 @@ 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_sig (f g : fe1305) :
-  { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}.
+Definition app_5 (f : fe1305) (P : fe1305 -> fe1305) : fe1305.
+Proof.
+  cbv [fe1305] in *.
+  set (f0 := f).
+  repeat (let g := fresh "g" in destruct f as [f g]).
+  apply P.
+  apply f0.
+Defined.
+
+Definition app_5_correct f (P : fe1305 -> fe1305) : app_5 f P = P f.
 Proof.
+  intros.
   cbv [fe1305] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  reflexivity.
+Qed.
+
+Definition appify2 (op : fe1305 -> fe1305 -> fe1305) (f g : fe1305):= 
+  app_5 f (fun f0 => (app_5 g (fun g0 => op f0 g0))).
+
+Lemma appify2_correct : forall op f g, appify2 op f g = op f g.
+Proof.
+  intros. cbv [appify2].
+  etransitivity; apply app_5_correct.
+Qed.
+
+Definition add_sig (f g : fe1305) :
+  { fg : fe1305 | fg = ModularBaseSystemInterface.add f g}.
+Proof.
   eexists.
+  rewrite <-appify2_correct. (* Coq 8.4 : 6s *)
   cbv.
   reflexivity.
-Defined.
+Defined. (* Coq 8.4 : 7s *)
 
 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)).
+  proj1_sig (add_sig f g).
 
 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)).
+  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}.
 Proof.
-  cbv [fe1305] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
+  rewrite <-appify2_correct.
   cbv.
   reflexivity.
 Defined.
 
 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)).
+  proj1_sig (sub_sig f g).
 
 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)).
+  Eval cbv beta iota delta [proj1_sig sub_sig] in
+  proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *)
 
 Definition mul_sig (f g : fe1305) :
   { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
+  rewrite <-appify2_correct. (* Coq 8.4 : 5s; changes the [repeat match ... => destruct] below from 25s to 8s *)
   cbv [fe1305] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. (* 8s *)
   eexists.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
-Defined.
+Defined. (* Coq 8.4 : 14s *)
 
 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)).
+  proj1_sig (mul_sig f g).
 
 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)).
+  Eval cbv beta iota delta [proj1_sig add_sig] in
+  proj2_sig (mul_sig f g). (* Coq 8.4 : 5s *)
 
 Import Morphisms.
 
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 261b6f4fe..badc17963 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -49,53 +49,72 @@ 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_sig (f g : fe25519) :
-  { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}.
+Definition app_10 (f : fe25519) (P : fe25519 -> fe25519) : fe25519.
+Proof.
+  cbv [fe25519] in *.
+  set (f0 := f).
+  repeat (let g := fresh "g" in destruct f as [f g]).
+  apply P.
+  apply f0.
+Defined.
+
+Lemma app_10_correct : forall f P, app_10 f P = P f.
 Proof.
+  intros.
   cbv [fe25519] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  reflexivity.
+Qed.
+
+Definition appify2 (op : fe25519 -> fe25519 -> fe25519) (f g : fe25519):= 
+  app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))).
+
+Lemma appify2_correct : forall op f g, appify2 op f g = op f g.
+Proof.
+  intros. cbv [appify2].
+  etransitivity; apply app_10_correct.
+Qed.
+
+Definition add_sig (f g : fe25519) :
+  { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}.
+Proof.
   eexists.
+  rewrite <-appify2_correct.
   cbv.
   reflexivity.
 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)).
+  proj1_sig (add_sig f g).
 
 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)).
+  Eval cbv beta iota delta [proj1_sig add_sig] in
+  proj2_sig (add_sig f 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.
+  rewrite <-appify2_correct.
   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)).
+  proj1_sig (sub_sig f g).
 
 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)).
+  Eval cbv beta iota delta [proj1_sig sub_sig] in
+  proj2_sig (sub_sig f g).
 
 Definition mul_sig (f g : fe25519) :
   { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
+  rewrite <-appify2_correct.
   cbv [fe25519] in *.
   repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
   eexists.
@@ -106,15 +125,12 @@ 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)).
+  proj1_sig (mul_sig f g).
 
 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)).
+  Eval cbv beta iota delta [proj1_sig add_sig] in
+  proj2_sig (mul_sig f g).
 
 Import Morphisms.