diff options
Diffstat (limited to 'src/Specific/GF1305.v')
-rw-r--r-- | src/Specific/GF1305.v | 66 |
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. |