diff options
author | 2016-07-18 08:36:57 -0400 | |
---|---|---|
committer | 2016-07-18 08:36:57 -0400 | |
commit | 2850867717149c0b93f89e8fbd8c3a3ea2b4c6ec (patch) | |
tree | 83a868c1021d08d18aad371dd06e568f6b792cab | |
parent | d0168dec22e1359e9ae7c0eb6399782f7d03fe9e (diff) |
Fixed unsimplified multiplication definitions in Specific by separating out the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.
-rw-r--r-- | src/Specific/GF1305.v | 25 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 26 |
2 files changed, 44 insertions, 7 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 74f914616..077c98954 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -115,16 +115,35 @@ Definition sub_correct (f g : fe1305) 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) : +Definition mul_simpl_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. (* 8s *) + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. autorewrite with zsimplify. reflexivity. +Defined. + +Definition mul_simpl (f g : fe1305) : fe1305 := + Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in + proj1_sig (mul_simpl_sig f g). + +Definition mul_simpl_correct (f g : fe1305) + : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in + proj2_sig (mul_simpl_sig f g). + +Definition mul_sig (f g : fe1305) : + { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. +Proof. + eexists. + rewrite <-mul_simpl_correct. + rewrite <-appify2_correct. + cbv. + autorewrite with zsimplify. + reflexivity. Defined. (* Coq 8.4 : 14s *) Definition mul (f g : fe1305) : fe1305 := diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index badc17963..6298941db 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -111,25 +111,43 @@ Definition sub_correct (f g : fe25519) Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). -Definition mul_sig (f g : fe25519) : +Definition mul_simpl_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. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. cbv. autorewrite with zsimplify. reflexivity. Defined. +Definition mul_simpl (f g : fe25519) : fe25519 := + Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in + proj1_sig (mul_simpl_sig f g). + +Definition mul_simpl_correct (f g : fe25519) + : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in + proj2_sig (mul_simpl_sig f g). + +Definition mul_sig (f g : fe25519) : + { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. +Proof. + eexists. + rewrite <- mul_simpl_correct. + rewrite <-appify2_correct. + cbv. + reflexivity. +Defined. + Definition mul (f g : fe25519) : fe25519 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). Definition mul_correct (f g : fe25519) : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := - Eval cbv beta iota delta [proj1_sig add_sig] in + Eval cbv beta iota delta [proj1_sig mul_sig] in proj2_sig (mul_sig f g). Import Morphisms. |