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, 3 insertions, 15 deletions

diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v
index 9dc49ca00..0a29973a1 100644
--- a/src/Specific/IntegrationTestKaratsubaMul.v
+++ b/src/Specific/IntegrationTestKaratsubaMul.v
@@ -46,21 +46,9 @@ Section BoundedField25p5.
     { mul : feBW -> feBW -> feBW
     | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }.
   Proof.
-    lazymatch goal with
-    | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ]
-      => apply lift2_sig with (P:=fun a b f => phi f = rhs a b)
-    end.
-    intros a b.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- (proj2_sig mul_sig).
-    symmetry; rewrite <- (proj2_sig carry_sig); symmetry.
-    set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)).
-    change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b).
-    context_to_dlet_in_rhs carry_mulZ.
-    cbv beta iota delta [carry_mulZ proj1_sig mul_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)).
+    start_preglue.
+    do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime.
+    all:fin_preglue.
     (* jgross start here! *)
     (*Set Ltac Profiling.*)
     Time refine_reflectively.