more changes to Specific for 8.4 compatibility

1 files changed, 38 insertions, 22 deletions

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.