Factor out some bits of ladderstep preglue

This requires some changes to nonzero, which now needs to unfold
proj1_sig itself.

4 files changed, 111 insertions, 34 deletions

diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
index 3c605e348..27e710fe6 100644
--- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
+++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v
@@ -80,6 +80,7 @@ Section BoundedField25p5.
     cbv_runtime.
     reflexivity.
     sig_dlet_in_rhs_to_context.
+    cbv [proj1_sig].
     match goal with
     | [ H : feBW_small |- _ ] => destruct H as [? _]
     end.
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v
index 2e46d22eb..4aae7ee0a 100644
--- a/src/Specific/IntegrationTestTemporaryMiscCommon.v
+++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v
@@ -121,23 +121,90 @@ Ltac apply_lift_sig :=
   | [ |- { f | _ } ]
     => idtac
   end.
+Ltac get_proj2_sig_map_arg_helper P :=
+  lazymatch P with
+  | (fun e => ?A -> @?B e)
+    => let B' := get_proj2_sig_map_arg_helper B in
+       uconstr:(A -> B')
+  | _ => uconstr:(_ : Prop)
+  end.
+Ltac get_proj2_sig_map_arg _ :=
+  lazymatch goal with
+  | [ |- { e : ?T | @?E e } ]
+    => let P := get_proj2_sig_map_arg_helper E in
+       uconstr:(fun e : T => P)
+  end.
+Ltac get_phi_for_preglue _ :=
+  lazymatch goal with
+  | [ |- { e | @?E e } ]
+    => lazymatch E with
+       | context[Tuple.map (Tuple.map ?phi) _ = _]
+         => phi
+       | context[?phi _ = _]
+         => phi
+       end
+  end.
 Ltac start_preglue :=
-  apply_lift_sig; intros;
-  let phi := lazymatch goal with |- { f | ?phi _ = _ } => phi end in
-  eexists_sig_etransitivity; cbv [phi].
+  apply_lift_sig; intros; cbv beta iota zeta;
+  let phi := get_phi_for_preglue () in
+  let P' := get_proj2_sig_map_arg () in
+  refine (proj2_sig_map (P:=P') _ _);
+  [ let FINAL := fresh "FINAL" in
+    let a := fresh "a" in
+    intros a FINAL;
+    repeat (let H := fresh in intro H; specialize (FINAL H));
+    lazymatch goal with
+    | [ |- ?phi _ = ?RHS ]
+      => refine (@eq_trans _ _ _ RHS FINAL _); cbv [phi]; clear a FINAL
+    | [ |- _ /\ Tuple.map (Tuple.map ?phi) _ = _ ]
+      => split; cbv [phi]; [ refine (proj1 FINAL); shelve | ]
+    end
+  | cbv [phi] ].
 Ltac do_set_sig f_sig :=
   let fZ := fresh f_sig in
   set (fZ := proj1_sig f_sig);
-  context_to_dlet_in_rhs fZ; cbv beta delta [fZ];
-  try cbv beta iota delta [proj1_sig f_sig];
+  context_to_dlet_in_rhs fZ;
+  try cbv beta iota delta [proj1_sig f_sig] in fZ;
+  cbv beta delta [fZ]; clear fZ;
   cbv beta iota delta [fst snd].
-Ltac do_rewrite_with_sig_by f_sig by_tac :=
+Ltac do_set_sig_1arg f_sig :=
+  let fZ := fresh f_sig in
+  set (fZ := proj1_sig f_sig);
+  context_to_dlet_in_rhs (fZ _);
+  try cbv beta iota delta [proj1_sig f_sig] in fZ;
+  cbv beta delta [fZ]; clear fZ;
+  cbv beta iota delta [fst snd].
+Ltac do_set_sigs _ :=
+  lazymatch goal with
+  | [ |- context[@proj1_sig ?a ?b ?f_sig] ]
+    => let fZ := fresh f_sig in
+       set (fZ := proj1_sig f_sig);
+       context_to_dlet_in_rhs fZ;
+       do_set_sigs (); (* we recurse before unfolding, because that's faster *)
+       try cbv beta iota delta [proj1_sig f_sig] in fZ;
+       cbv beta delta [fZ];
+       cbv beta iota delta [fst snd]
+  | _ => idtac
+  end.
+Ltac trim_after_do_rewrite_with_sig _ :=
+  repeat match goal with
+         | [ |- Tuple.map ?f _ = Tuple.map ?f _ ]
+           => apply f_equal
+         end.
+Ltac do_rewrite_with_sig_no_set_by f_sig by_tac :=
   let lem := constr:(proj2_sig f_sig) in
   let lemT := type of lem in
   let lemT := (eval cbv beta zeta in lemT) in
   rewrite <- (lem : lemT) by by_tac ();
+  trim_after_do_rewrite_with_sig ().
+Ltac do_rewrite_with_sig_by f_sig by_tac :=
+  do_rewrite_with_sig_no_set_by f_sig by_tac;
   do_set_sig f_sig.
+Ltac do_rewrite_with_sig_1arg_by f_sig by_tac :=
+  do_rewrite_with_sig_no_set_by f_sig by_tac;
+  do_set_sig_1arg f_sig.
 Ltac do_rewrite_with_sig f_sig := do_rewrite_with_sig_by f_sig ltac:(fun _ => idtac).
+Ltac do_rewrite_with_sig_1arg f_sig := do_rewrite_with_sig_1arg_by f_sig ltac:(fun _ => idtac).
 Ltac do_rewrite_with_1sig_add_carry_by f_sig carry_sig by_tac :=
   let fZ := fresh f_sig in
   rewrite <- (proj2_sig f_sig) by by_tac ();
@@ -164,6 +231,34 @@ Ltac do_rewrite_with_2sig_add_carry_by f_sig carry_sig by_tac :=
   try cbv beta iota delta [proj1_sig f_sig carry_sig];
   cbv beta iota delta [fst snd].
 Ltac do_rewrite_with_2sig_add_carry f_sig carry_sig := do_rewrite_with_2sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac).
+Ltac unmap_map_tuple _ :=
+  repeat match goal with
+         | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ]
+           => rewrite <- (Tuple.map_map (n:=N) f g
+                          : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x))))
+         end.
+Ltac subst_feW _ :=
+  let T := lazymatch goal with |- @sig ?T _ => T end in
+  let boundedT := lazymatch goal with |- { e | ?A -> _ } => A end in
+  match goal with
+  | [ feW := _ : Type |- _ ]
+    => match goal with
+       | [ feW_bounded := _ : feW -> Prop |- _ ]
+         => lazymatch T with
+            | context[feW] => idtac
+            end;
+            lazymatch boundedT with
+            | context[feW_bounded _] => idtac
+            end;
+            subst feW feW_bounded
+       end
+  end;
+  cbv beta.
+Ltac finish_conjoined_preglue _ :=
+  [ > match goal with
+      | [ FINAL : _ /\ ?e |- _ ] => is_evar e; refine (proj2 FINAL)
+      end
+  | try subst_feW () ].
 Ltac fin_preglue :=
   [ > reflexivity
   | repeat sig_dlet_in_rhs_to_context;
@@ -191,6 +286,7 @@ Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t :=
       | .. ];
       op_sig_side_conditions_t ()
   | 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));
+    cbv [proj1_sig];
     repeat match goal with
            | [ H : feBW_small |- _ ] => destruct H as [? _]
            end ].
diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v
index b46460550..c74e7a872 100644
--- a/src/Specific/NISTP256/AMD64/fenz.v
+++ b/src/Specific/NISTP256/AMD64/fenz.v
@@ -80,6 +80,7 @@ Section BoundedField25p5.
     cbv_runtime.
     reflexivity.
     sig_dlet_in_rhs_to_context.
+    cbv [proj1_sig].
     match goal with
     | [ H : feBW_small |- _ ] => destruct H as [? _]
     end.
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index 9e2187a81..7b9062a6b 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -112,34 +112,13 @@ Section BoundedField25p5.
             /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
            /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
   Proof.
-    apply_lift_sig.
-    intros a b c; cbv beta iota zeta.
-    lazymatch goal with
-    | [ |- { e | ?A -> ?B -> ?C -> @?E e } ]
-      => refine (proj2_sig_map (P:=fun e => A -> B -> C -> (_:Prop)) _ _)
-    end.
-    { intros ? FINAL.
-      repeat let H := fresh in intro H; specialize (FINAL H).
-      cbv [phi].
-      split; [ refine (proj1 FINAL); shelve | ].
-      do 4 match goal with
-           | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ]
-             => rewrite <- (Tuple.map_map (n:=N) f g
-                            : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x))))
-           end.
-      rewrite <- (proj2_sig Mxzladderstep_sig).
-      apply f_equal.
-      cbv [proj1_sig]; cbv [Mxzladderstep_sig].
-      context_to_dlet_in_rhs (@Mxzladderstep _).
-      cbv [Mxzladderstep M.xzladderstep a24_sig].
-      repeat lazymatch goal with
-             | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
-               => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
-             end.
-      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig].
-      cbv_runtime.
-      refine (proj2 FINAL). }
-    subst feW feW_bounded; cbv beta.
+    start_preglue.
+    unmap_map_tuple ().
+    do_rewrite_with_sig_1arg Mxzladderstep_sig.
+    cbv [Mxzladderstep M.xzladderstep a24_sig]; cbn [proj1_sig].
+    do_set_sigs ().
+    cbv_runtime.
+    all:finish_conjoined_preglue ().
     (* jgross start here! *)
     Set Ltac Profiling.
     (*