Finally, a fully working IntegrationTest

1 files changed, 45 insertions, 56 deletions

diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Reflection/Z/Bounds/Pipeline/Glue.v
index 7621a466b..af6a5548b 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Glue.v
+++ b/src/Reflection/Z/Bounds/Pipeline/Glue.v
@@ -12,84 +12,65 @@ Require Import Crypto.Util.Curry.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.SigmaAssoc.
+Require Import Crypto.Util.Tactics.EvarExists.
 
 Module Export Exports.
   Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
 End Exports.
 
+(** The [reassoc_sig_and_eexists] tactic operates on a goal convertible with
+<<
+{ f : { a | is_bounded_by bounds a }
+| BoundedWordToZ f = rexprZ (BoundedWordToZ a) ... (BoundedWordToZ z) }
+>>
+    and leaves a goal of the form
+<<
+is_bounded_by bounds (map wordToZ ?f)
+  /\ map wordToZ ?f = rexprZ (map wordToZ (proj1_sig a)) ... (map wordToZ (proj1_sig z))
+>>
+    where [?f] is a context variable set to a new evar.  This tactic
+    relies on the exact definition of [BoundedWordToZ]. *)
+Ltac reassoc_sig_and_eexists :=
+  cbv [BoundedWordToZ];
+  sig_sig_assoc;
+  evar_exists.
+
 (** The [do_curry] tactic takes a goal of the form
 <<
-BoundedWordToZ (?f a b ... z) = F A B ... Z
+_ /\ BoundedWordToZ (?f a b ... z) = F A B ... Z
 >>
     and turns it into a goal of the form
 <<
-BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z)
+_ /\ BoundedWordToZ (f' (a, b, ..., z)) = F' (A, B, ..., Z)
 >>
 
     Note that the number of arguments on the left and on the right DO
     NOT need to be the same.  *)
 Ltac do_curry :=
   lazymatch goal with
-  | [ |- ?BWtoZ ?f_bw = ?f_Z ]
+  | [ |- _ /\ ?BWtoZ ?f_bw = ?f_Z ]
     => let f_bw := head f_bw in
        let f_Z := head f_Z in
        change_with_curried f_Z;
-       let f_bw_name := fresh f_bw in
-       set (f_bw_name := f_bw);
-       change_with_curried f_bw_name
+       change_with_curried f_bw
   end.
 
 (** The [split_BoundedWordToZ] tactic takes a goal of the form
 <<
-BoundedWordToZ f = F
+_ /\ map wordToZ (proj1_sig f) = F ARGS
 >>
-    and splits it into a conjunction, one part about the computational
-    behavior, and another part about the boundedness.
+    and splits [f] and any arguments in ARGS into two parts, part
+    about the computational behavior, and another part about the
+    boundedness.
 
-    This tactic relies on the specific definition of [BoundedWordToZ],
+    This pipeline relies on the specific definition of [BoundedWordToZ],
     and requires [f] to be a context variable which is set to a single
     evar. *)
-Ltac make_evar_for_first_projection :=
+Ltac check_precondition _ :=
   lazymatch goal with
-  | [ |- @map ?N1 ?A ?B wordToZ (@proj1_sig _ ?P ?f) = _ ]
-    => let f1 := fresh f in
-       let f2 := fresh f in
-       let pf := fresh in
-       revert f; refine (_ : let f := exist P _ _ in _);
-       intro f;
-       pose (proj1_sig f) as f1;
-       pose (proj2_sig f : P f1) as f2;
-       change f with (exist P f1 f2);
-       subst f; cbn [proj1_sig proj2_sig] in f1, f2 |- *; revert f2;
-       (** Now we rely on the behavior of Coq's unifier to transform
-           the goal for us; we a goal like [let f' : A := ?f_evar in
-           B], and we want a goal like [A /\ B].  So we refine with a
-           hole named [pf] which is proof of [A /\ B], and then assert
-           that the second projection of the proof (which has type
-           [B]) actually has type [let f' : A := proj1 pf in B].  If
-           done naïvely, this would give a circlular type, which Coq
-           disallows.  However, Coq is happy to zeta-reduce away the
-           circlularity; happily, this is done after Coq unifies [let
-           f' : A := proj1 pf in B] with [let f' : A := ?f_evar in B],
-           hence filling [?f_evar] with the first projection of the
-           proof.  Since Coq instantiates the two existing evars
-           ([?f_evar] and the current goal, which is represented by an
-           evar under the hood) with projections of the new evar
-           (which becomes the new goal)---and let us hope that Coq
-           devs never decide both to turn on judgmental η (currently
-           controlled by primitive projections) for [and], and to
-           prefer η-expansion of evars before dropping context
-           variables (we might also be in trouble if someone adds a
-           [Canonical Structure] for [and])---we get the desired
-           behavior--for now. *)
-       lazymatch goal with
-       | [ |- let f' := _ in ?B ]
-         => refine (let pf := _ in (proj2 pf : let f' := proj1 pf in B))
-       end
-  end.
-Ltac check_split_BoundedWordToZ_precondition :=
-  lazymatch goal with
-  | [ |- BoundedWordToZ _ _ _ ?f = _ ]
+  | [ |- @ZRange.is_bounded_by ?option_bit_width ?count ?bounds (map wordToZ ?f)
+         /\ map wordToZ ?f = _ ]
     => first [ is_var f | fail 1 "The argument to BoundedWordToZ must be a bare context-definition set to an evar, not"
                                f "which is not a variable" ];
        match goal with
@@ -103,19 +84,26 @@ Ltac check_split_BoundedWordToZ_precondition :=
                  f' "which has no body"
        | _ => fail 1 "The argument to BoundedWordToZ must be a context-definition, not" f "which does not appear in the context"
        end
+  | [ |- ?G ]
+    => let expected := uconstr:(@ZRange.is_bounded_by _ _ _ (map wordToZ ?[f])
+                                /\ map wordToZ ?[f] = _) in
+       fail "The post-processed goal should have the form"
+            expected
+            "not"
+            G
   end.
 Ltac split_BoundedWordToZ :=
-  check_split_BoundedWordToZ_precondition;
   (** first revert the context definition which is an evar named [f]
       in the docs above, so that it becomes evar 1 (for
       [instantiate]), and so that [make_evar_for_first_projection]
       works *)
+  check_precondition ();
   lazymatch goal with
-  | [ |- BoundedWordToZ _ _ _ ?f = _ ]
+  | [ |- _ /\ map wordToZ ?f = _ ]
     => revert f
   end;
   repeat match goal with
-         | [ |- context[BoundedWordToZ _ _ _ ?x] ]
+         | [ |- context[map wordToZ (proj1_sig ?x)] ]
            => is_var x;
               first [ clearbody x; fail 1
                     | (** we want to keep the same context variable in
@@ -124,8 +112,8 @@ Ltac split_BoundedWordToZ :=
                     instantiate (1:=ltac:(destruct x)); destruct x ]
          end;
   cbv beta iota; intro; (* put [f] back in the context so that [cbn] doesn't remove this let-in *)
-  unfold BoundedWordToZ; cbn [proj1_sig];
-  make_evar_for_first_projection.
+  cbn [proj1_sig].
+
 (** The [zrange_to_reflective] tactic takes a goal of the form
 <<
 is_bounded_by _ bounds (map wordToZ (?fW args)) /\ map wordToZ (?fW args) = fZ argsZ
@@ -200,6 +188,7 @@ BoundedWordToZ ?f = F (BoundedWordToZ A) (BoundedWordToZ B) ... (BoundedWordToZ
     where [?f] is an evar, and turns it into a goal the that
     reflective automation pipeline can handle. *)
 Ltac refine_to_reflective_glue :=
+  reassoc_sig_and_eexists;
   do_curry;
   split_BoundedWordToZ;
-  zrange_to_reflective.
+  zrange_to_reflective_goal.