diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-05-14 18:35:29 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-05-14 18:35:29 -0400 |
| commit | b59f62e633da3ece4bff29823b6d19e79c3e3714 (patch) | |
| tree | 845a5b6554c698d4b586b518425aaa880423812e /src/Specific/IntegrationTestSquare.v | |
| parent | 8bade36d3e2162e6acacd5f057fe6b106f49a637 (diff) | |
specialize squaring earlier
Diffstat (limited to 'src/Specific/IntegrationTestSquare.v')
| -rw-r--r-- | src/Specific/IntegrationTestSquare.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v index d592717fe..b0b5e5b5a 100644 --- a/src/Specific/IntegrationTestSquare.v +++ b/src/Specific/IntegrationTestSquare.v @@ -52,12 +52,12 @@ Section BoundedField25p5. end. intros. eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig mul_sig). + rewrite <- (proj2_sig square_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig mul_sig a a)). - change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?a)) with (carry_squareZ a). + set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a a)). + change (proj1_sig carry_sig (proj1_sig square_sig ?a ?a)) with (carry_squareZ a). context_to_dlet_in_rhs carry_squareZ. - cbv beta iota delta [carry_squareZ proj1_sig mul_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. + cbv beta iota delta [carry_squareZ proj1_sig square_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. reflexivity. sig_dlet_in_rhs_to_context. apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). |