Factor out some of the preglue synthesis code

This makes it a bit more uniform, and hopefully more automatable and
packageable.  Unfortunately, there's still no spec for this part of the
pipeline, so the tactics simply aggregate common patterns.

Alas, this also makes things a bit slower; I suspect that [Defined] is
the place where things are slower.

After     | File Name                                          | Before    || Change
---------------------------------------------------------------------------------------
13m51.14s | Total                                              | 12m59.29s || +0m51.84s
---------------------------------------------------------------------------------------
1m54.18s  | Specific/IntegrationTestKaratsubaMul               | 1m43.12s  || +0m11.06s
1m38.97s  | Specific/IntegrationTestLadderstep130              | 1m30.26s  || +0m08.70s
2m19.75s  | Specific/NISTP256/AMD64/femul                      | 2m14.08s  || +0m05.66s
0m39.90s  | Specific/IntegrationTestMontgomeryP256_128         | 0m34.21s  || +0m05.68s
0m21.95s  | Specific/NISTP256/AMD64/fesub                      | 0m19.23s  || +0m02.71s
0m21.37s  | Specific/NISTP256/AMD64/feadd                      | 0m18.82s  || +0m02.55s
0m21.02s  | Specific/X25519/C64/femul                          | 0m18.32s  || +0m02.69s
0m20.53s  | Specific/IntegrationTestFreeze                     | 0m23.26s  || -0m02.73s
0m18.28s  | Specific/IntegrationTestMontgomeryP256_128_Sub     | 0m15.32s  || +0m02.96s
0m18.20s  | Specific/IntegrationTestMontgomeryP256_128_Add     | 0m15.52s  || +0m02.67s
0m16.35s  | Specific/IntegrationTestMontgomeryP256_128_Opp     | 0m13.52s  || +0m02.83s
0m13.92s  | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s  || +0m02.08s
0m18.23s  | Specific/NISTP256/AMD64/MontgomeryP256             | 0m16.62s  || +0m01.60s
0m15.54s  | Specific/IntegrationTestSub                        | 0m14.53s  || +0m01.00s
0m14.78s  | Specific/X25519/C64/fesquare                       | 0m13.13s  || +0m01.64s
0m13.71s  | Specific/NISTP256/AMD64/fenz                       | 0m12.69s  || +0m01.02s
3m14.34s  | Specific/X25519/C64/ladderstep                     | 3m14.32s  || +0m00.02s
0m16.54s  | Specific/NISTP256/AMD64/feopp                      | 0m16.48s  || +0m00.05s
0m12.21s  | Specific/MontgomeryP256_128                        | 0m12.70s  || -0m00.48s
0m00.73s  | Specific/IntegrationTestTemporaryMiscCommon        | 0m00.72s  || +0m00.01s
0m00.64s  | Specific/IntegrationTestDisplayCommon              | 0m00.60s  || +0m00.04s

1 files changed, 9 insertions, 26 deletions

diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v
index ef4ea6aa6..14342c238 100644
--- a/src/Specific/NISTP256/AMD64/feopp.v
+++ b/src/Specific/NISTP256/AMD64/feopp.v
@@ -40,37 +40,20 @@ Section BoundedField25p5.
   Let phi : feBW -> F m :=
     fun x => montgomery_to_F (eval x).
 
+  Local Ltac op_sig_side_conditions_t _ :=
+    try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption.
+
   (* TODO : change this to field once field isomorphism happens *)
   Definition opp
     : { opp : feBW_small -> feBW_small
       | forall A, phi (opp A) = F.opp (phi A) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a, ?phi (?proj (f a)) = @?rhs a } ]
-      => apply lift1_sig with (P:=fun a f => phi (proj f) = rhs a)
-    end.
-    intros a.
-    cbv [feBW_of_feBW_small].
-    eexists_sig_etransitivity. all:cbv [phi eval].
-    rewrite <- (proj1 (proj2_sig opp))
-      by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption).
-    reflexivity.
-    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)).
-    Associativity.sig_sig_assoc.
-    apply sig_conj_by_impl2.
-    { intros ? H; cbv [eval]; rewrite H; clear H.
-      apply (proj2 (proj2_sig opp)); destruct_head' feBW_small; try assumption;
-        hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. }
-    eexists_sig_etransitivity.
-    set (oppZ := proj1_sig opp).
-    context_to_dlet_in_rhs oppZ; cbv [oppZ].
-    cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr].
-    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)).
-    match goal with
-    | [ H : feBW_small |- _ ] => destruct H as [? _]
-    end.
+    start_preglue.
+    all:cbv [feBW_of_feBW_small eval].
+    do_rewrite_with_sig_by opp op_sig_side_conditions_t.
+    cbv_runtime.
+    all:fin_preglue.
+    factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t.
     (* jgross start here! *)
     Set Ltac Profiling.
     (*     Set Ltac Profiling.