Update display of ladderstep130

1 files changed, 42 insertions, 44 deletions

diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
index be1be63ac..74b2ce674 100644
--- a/src/Specific/IntegrationTestLadderstep130.v
+++ b/src/Specific/IntegrationTestLadderstep130.v
@@ -42,9 +42,11 @@ Section BoundedField25p5.
   Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
   Let feZ : Type := tuple Z sz.
   Let feW : Type := tuple (wordT lgbitwidth) sz.
+  Let feW_bounded : feW -> Prop
+    := fun w => is_bounded_by None bounds (map wordToZ w).
   Let feBW : Type := BoundedWord sz bitwidth bounds.
-  Let phi : feBW -> F m :=
-    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
+  Let phi : feW -> F m :=
+    fun x => B.Positional.Fdecode wt (Tuple.map wordToZ x).
 
   (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
   Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul.
@@ -64,56 +66,52 @@ Section BoundedField25p5.
 
   (* TODO : change this to field once field isomorphism happens *)
   Definition xzladderstep :
-    { xzladderstep : feBW -> feBW -> feBW * feBW -> feBW * feBW -> feBW * feBW * (feBW * feBW)
-    | forall a24 x1 Q Q', Tuple.map (n:=2) (Tuple.map (n:=2) phi) (xzladderstep a24 x1 Q Q') = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
+    { xzladderstep : feW -> feW -> feW * feW -> feW * feW -> feW * feW * (feW * feW)
+    | forall a24 x1 Q Q',
+        let xz := xzladderstep a24 x1 Q Q' in
+        feW_bounded a24
+        -> feW_bounded x1
+        -> feW_bounded (fst Q) /\ feW_bounded (snd Q)
+        -> feW_bounded (fst Q') /\ feW_bounded (snd Q')
+        -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz)))
+            /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz))))
+           /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
   Proof.
     lazymatch goal with
-    | [ |- { f | forall a b c d, ?phi (f a b c d) = @?rhs a b c d } ]
-      => apply lift4_sig with (P:=fun a b c d f => phi f = rhs a b c d)
-    end.
-    intros.
-    eexists_sig_etransitivity. all:cbv [phi].
-    rewrite <- !(Tuple.map_map (B.Positional.Fdecode wt) (BoundedWordToZ sz bitwidth bounds)).
-    rewrite <- (proj2_sig Mxzladderstep_sig).
-    apply f_equal.
-    cbv [proj1_sig]; cbv [Mxzladderstep_sig].
-    context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _).
-    set (k := @M.xzladderstep _ _ _ _); context_to_dlet_in_rhs k; subst k.
-    cbv [M.xzladderstep].
-    lazymatch goal with
-    | [ |- context[@proj1_sig ?a ?b carry_sig] ]
-      => context_to_dlet_in_rhs (@proj1_sig a b carry_sig)
+    | [ |- { op | forall (a:?A) (b:?B) (c:?C) (d:?D),
+               let v := op a b c d in
+               @?P a b c d v } ]
+      => refine (@lift4_sig A B C D _ P _)
     end.
+    intros a b c d; cbv beta iota zeta.
     lazymatch goal with
-    | [ |- context[@proj1_sig ?a ?b mul_sig] ]
-      => context_to_dlet_in_rhs (@proj1_sig a b mul_sig)
+    | [ |- { e | ?A -> ?B -> ?C -> ?D -> @?E e } ]
+      => refine (proj2_sig_map (P:=fun e => A -> B -> C -> D -> (_:Prop)) _ _)
     end.
-    lazymatch goal with
-    | [ |- context[@proj1_sig ?a ?b add_sig] ]
-      => context_to_dlet_in_rhs (@proj1_sig a b add_sig)
-    end.
-    lazymatch goal with
-    | [ |- context[@proj1_sig ?a ?b sub_sig] ]
-      => context_to_dlet_in_rhs (@proj1_sig a b sub_sig)
-    end.
-    cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
-    reflexivity.
-    eexists_sig_etransitivity_for_rewrite_fun.
-    { intro; cbv beta.
-      subst feBW.
-      set_evars.
-      do 2 lazymatch goal with
-           | [ |- context[Tuple.map (n:=?n) (fun x => ?f (?g x))] ]
-             => rewrite <- (Tuple.map_map (n:=n) f g : pointwise_relation _ eq _ _)
+    { 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 (@M.xzladderstep _ _ _ _).
+      cbv [M.xzladderstep].
+      do 4 lazymatch goal with
+           | [ |- context[@proj1_sig ?a ?b ?f_sig _] ]
+             => context_to_dlet_in_rhs (@proj1_sig a b f_sig)
            end.
-      subst_evars.
-      reflexivity. }
-    cbv beta.
-    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)).
-    apply adjust_tuple2_tuple2_sig.
+      cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd].
+      refine (proj2 FINAL). }
+    subst feW feW_bounded; cbv beta.
     (* jgross start here! *)
-    Set Ltac Profiling.
     (*
+    Set Ltac Profiling.
     Time Glue.refine_to_reflective_glue (128::256::nil)%nat%list.
     Time ReflectiveTactics.refine_with_pipeline_correct.
     { Time ReflectiveTactics.do_reify. }