diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-07-08 14:37:08 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-07-08 14:37:08 -0400 |
| commit | 9dbd0015fc2f895260720a08c0844e9c75cccbd0 (patch) | |
| tree | 148de4a92afcbe145c7d4cda78c756eab86bf8bc /src/Specific | |
| parent | 3cc4485c69839443b1a94df785d5d2f838b54f51 (diff) | |
defined some group operations, stated group lemma for tuple-based [add] (in terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/GF1305.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index edb122ac2..057676ee2 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -48,11 +48,11 @@ Definition fe1305 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. -Definition mul (f g:fe1305) : { fg | fg = ModularBaseSystemInterface.mul k_subst c_subst f g }. +Definition mul (f g:fe1305) : { fg | fg = @ModularBaseSystemInterface.mul _ _ k_ c_ f g }. (* NOTE: beautiful example of reduction slowness: stack overflow if [f] [g] are not destructed first *) cbv [fe1305] in *. repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. - eexists. + eexists. cbv. autorewrite with zsimplify. reflexivity. |