more changes to Specific for 8.4 compatibility

1 files changed, 41 insertions, 25 deletions

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.