Standardize list wf things

Rather than using Forall2 in some places and a combination of length,
combine, and In in others, we now primarily use Forall2.

There is probably some dead tactic code as a result of this that I just
haven't bothered to clean up.

4 files changed, 98 insertions, 34 deletions

diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index 85eef1cae..25c8ba574 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -10,6 +10,7 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.Forall.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -314,13 +315,34 @@ Module Compilers.
                 {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
                 {is_annotated_for_Proper : forall t t', Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t')}
                 (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
-                (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2)
+                (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> List.Forall2 (@abstract_domain'_R t) l1 l2)
                 (extract_option_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2)).
 
         Local Instance abstract_interp_ident_Proper_arrow s d
           : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d))
           := abstract_interp_ident_Proper (type.arrow s d).
 
+        Local Ltac handle_Forall2_step :=
+          first [ match goal with
+                  | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper]
+                  | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff
+                  | [ |- List.Forall2 _ (List.combine _ _) (List.combine _ _) ]
+                    => eapply Forall2_combine; [ intros | eassumption | eassumption ]
+                  | [ |- List.Forall2 _ (List.combine ?x _) (List.combine ?x _) ]
+                    => eapply Forall2_combine;
+                       [ intros
+                       | instantiate (1:=fun a b => a = b /\ List.In a x);
+                         rewrite Forall2_Forall, Forall_forall; cbv [Proper]; auto
+                       | eassumption ]
+                  | [ H : expr.wf _ ?d1 ?d2, H' : List.Forall2 (expr.wf _) ?xs ?ys
+                      |- expr.wf ?G (nth_default ?d1 ?xs ?n) (nth_default ?d2 ?ys ?n) ]
+                    => cut (List.Forall2 (expr.wf G) xs ys /\ expr.wf G d1 d2);
+                       [ rewrite Forall2_forall_iff'';
+                         let H := fresh in intros [? H]; apply H
+                       | ]
+                  end ].
+
+
         Section with_var2.
           Context {var1 var2 : type -> Type}.
 
@@ -472,7 +494,9 @@ Module Compilers.
                                                                                                                                                   |- ?R ?a1 ?a2 ]
                                   => apply H
                                 | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n')
+                                | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H
                                 end
+                              | handle_Forall2_step
                               | break_innermost_match_step
                               | break_innermost_match_hyps_step
                               | progress expr.invert_match
@@ -580,6 +604,7 @@ Module Compilers.
                            | progress expr.invert_subst
                            | progress expr.inversion_wf_constr
                            | progress expr.inversion_expr
+                           | handle_Forall2_step
                            | wf_safe_t_step
                            | progress destruct_head' (@partial.wf_value)
                            | solve [ eapply wf_annotate; wf_t; try apply DefaultValue.expr.base.wf_default
@@ -734,11 +759,10 @@ Module Compilers.
         intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity.
       Qed.
       Lemma extract_list_state_rel
-        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2.
+        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> List.Forall2 (@abstract_domain'_R t) l1 l2.
       Proof.
         intros; cbv [extract_list_state] in *; subst; inversion_option; subst.
-        rewrite combine_same, List.in_map_iff in *.
-        destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity.
+        now rewrite Forall2_Forall, Forall_forall; cbv [Proper].
       Qed.
 
       Lemma extract_option_state_rel
diff --git a/src/LanguageWf.v b/src/LanguageWf.v
index 4485bc841..6c5ce6ea5 100644
--- a/src/LanguageWf.v
+++ b/src/LanguageWf.v
@@ -933,12 +933,12 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         Local Notation expr1 := (@expr.expr base.type ident.ident var1).
         Local Notation expr2 := (@expr.expr base.type ident.ident var2).
 
-        Lemma wf_reify_list_Forall2 G {t} e1 e2
+        Lemma wf_reify_list G {t} e1 e2
           : @wf _ _ var1 var2 G _ (reify_list (t:=t) e1) (reify_list (t:=t) e2)
             <-> List.Forall2 (wf G) e1 e2.
         Proof.
           revert e2; induction e1 as [|e1 e1s IHe1s], e2 as [|e2 e2s];
-            rewrite ?expr.reify_list_cons, ?expr.reify_list_nil; cbn [length combine];
+            rewrite ?expr.reify_list_cons, ?expr.reify_list_nil;
               repeat first [ progress apply conj
                            | progress intros
                            | progress destruct_head'_and
@@ -961,12 +961,6 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
                            | solve [ eauto ] ].
         Qed.
 
-        Lemma wf_reify_list G {t} e1 e2
-          : @wf _ _ var1 var2 G _ (reify_list (t:=t) e1) (reify_list (t:=t) e2)
-            <-> (List.length e1 = List.length e2
-               /\ forall e1' e2', List.In (e1', e2') (List.combine e1 e2) -> wf G e1' e2').
-        Proof. now rewrite wf_reify_list_Forall2, Forall2_forall_In_combine_iff. Qed.
-
         Lemma wf_reflect_list G {t} e1 e2
            : @wf _ _ var1 var2 G (type.base (base.type.list t)) e1 e2
             -> (invert_expr.reflect_list e1 = None <-> invert_expr.reflect_list e2 = None).
@@ -1060,13 +1054,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         Lemma wf_reify {t} v G : expr.wf G (@GallinaReify.base.reify var1 t v) (@GallinaReify.base.reify var2 t v).
         Proof.
           induction t; cbn; cbv [option_map]; break_innermost_match; repeat constructor; auto; [].
-          rewrite wf_reify_list, !map_length, combine_map_map, combine_same, map_map; split; auto; intros *; [].
-          cbn [fst snd]; rewrite in_map_iff; intros.
-          repeat first [ progress destruct_head'_and
-                       | progress destruct_head'_ex
-                       | progress inversion_prod
-                       | progress subst
-                       | solve [ eauto ] ].
+          rewrite wf_reify_list, Forall2_map_map_iff, Forall2_Forall, Forall_forall; cbv [Proper]; auto.
         Qed.
 
         Lemma wf_smart_Literal {t v G}
@@ -1074,20 +1062,10 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         Proof using Type.
           induction t; cbn; eta_expand; repeat constructor; auto.
           all: rewrite wf_reify_list + rewrite wf_reify_option.
-          all: repeat first [ rewrite map_length
-                            | progress cbv [option_map option_eq]
-                            | apply conj
+          all: repeat first [ progress cbv [option_map option_eq Proper]
                             | reflexivity
-                            | progress intros
-                            | progress destruct_head'_ex
-                            | progress destruct_head'_and
-                            | progress inversion_prod
-                            | progress subst
+                            | rewrite Forall2_map_map_iff, Forall2_Forall, Forall_forall
                             | break_innermost_match_step
-                            | progress rewrite combine_map_map in *
-                            | progress rewrite combine_same in *
-                            | progress rewrite map_map in *
-                            | progress rewrite in_map_iff in *
                             | solve [ auto ] ].
         Qed.
 
diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v
index 7cbe4e560..c9c41a392 100644
--- a/src/RewriterRulesGood.v
+++ b/src/RewriterRulesGood.v
@@ -20,6 +20,7 @@ Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.ListUtil.ForallIn.
+Require Import Crypto.Util.ListUtil.Forall.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
@@ -282,6 +283,29 @@ Module Compilers.
                     exfalso; clear -H H'; congruence
                 | [ H : Compile.wf_value _ (reify_list _) (reify_list _) |- _ ]
                   => hnf in H; rewrite expr.wf_reify_list in H
+                | [ |- List.Forall2 _ ?x ?x ] => rewrite Forall2_Forall; cbv [Proper]
+                | [ |- List.Forall2 _ (List.map _ _) (List.map _ _) ] => rewrite Forall2_map_map_iff
+                | [ |- List.Forall2 _ (List.repeat _ _) (List.repeat _ _) ]
+                  => rewrite Forall2_repeat_iff
+                | [ |- List.Forall2 _ (List.rev _) (List.rev _) ]
+                  => rewrite Forall2_rev_iff
+                | [ |- List.Forall _ (seq _ _) ] => rewrite Forall_seq
+                | [ |- List.Forall2 _ (firstn _ _) (firstn _ _) ]
+                  => now apply Forall2_firstn
+                | [ |- List.Forall2 _ (skipn _ _) (skipn _ _) ]
+                  => now apply Forall2_skipn
+                | [ |- List.Forall2 _ (List.combine _ _) (List.combine _ _) ]
+                  => eapply Forall2_combine; [ intros | eassumption | eassumption ]
+                | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ]
+                  => apply Forall2_update_nth; intros
+                | [ H : List.Forall2 _ ?x ?y |- context[@List.length ?T ?y] ]
+                  => rewrite <- (@eq_length_Forall2 _ T _ x y H)
+                | [ H : Forall2 (expr.wf ?G) ?xs ?ys |- Forall2 (fun a b => UnderLets.wf (fun G' => expr.wf G') ?G _ _) ?xs ?ys ]
+                  => eapply Forall2_Proper_impl; [ .. | exact H ]; try reflexivity; repeat intro
+                | [ H : Forall2 ?P ?xs ?ys, Hx : nth_error ?xs ?n = _, Hy : nth_error ?ys ?n = _ |- _ ]
+                  => let H' := fresh in
+                     pose proof H as H';
+                     rewrite Forall2_forall_iff_nth_error in H'; specialize (H' n); rewrite Hx, Hy in H'; clear n Hx Hy
                 | [ H : length ?l = length ?l' |- context[length ?l] ] => rewrite H
                 | [ H : context[combine (firstn ?n _) (firstn ?n _)] |- _ ] => rewrite <- firstn_combine in H
                 | [ H : context[combine (skipn ?n _) (skipn ?n _)] |- _ ] => rewrite <- skipn_combine in H
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v
index 5b7caa0d6..0705ec94d 100644
--- a/src/UnderLetsProofs.v
+++ b/src/UnderLetsProofs.v
@@ -8,10 +8,12 @@ Require Import Crypto.UnderLets.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ListUtil.Forall.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SplitInContext.
 Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 
 Import EqNotations.
@@ -285,7 +287,7 @@ Module Compilers.
             { eapply He; eauto; rewrite ?app_assoc; eauto. } }
         Qed.
 
-        Lemma wf_splice_list_no_order {A1 B1 A2 B2}
+        Lemma wf_splice_list_no_order_nth_error {A1 B1 A2 B2}
               {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop}
               {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop}
               G
@@ -319,6 +321,32 @@ Module Compilers.
                            end ].
         Qed.
 
+        Lemma wf_splice_list_no_order {A1 B1 A2 B2}
+              {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop}
+              {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop}
+              G
+              (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2))
+              (P_Proper_list : forall G1 G2 a1 a2,
+                  (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2)
+                  -> P G1 a1 a2 -> P G2 a1 a2)
+              (Hx : List.Forall2 (wf P G) x1 x2)
+              (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2)
+              (He : forall G' a1 a2, (exists seg, G' = seg ++ G)
+                                     -> length a1 = length x1
+                                     -> length a2 = length x2
+                                     -> List.Forall2 (P G') a1 a2
+                                     -> @wf _ _ Q G' (e1 a1) (e2 a2))
+          : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2).
+        Proof.
+          setoid_rewrite Forall2_forall_In_combine_iff in He.
+          apply @wf_splice_list_no_order_nth_error with (P:=P); try assumption;
+            eauto using eq_length_Forall2.
+          { intro n; rewrite Forall2_forall_iff_nth_error in Hx; specialize (Hx n).
+            intros; cbv [option_eq] in *; break_innermost_match_hyps; inversion_option; subst; assumption. }
+          { rewrite Forall2_forall_In_combine_iff in Hx; destruct Hx.
+            intros; eapply He; try apply conj; eauto; congruence. }
+        Qed.
+
         Lemma wf_list_rect {A B Pnil Pcons ls A' B' Pnil' Pcons' ls'} {RA : A -> A' -> Prop} {RB G}
               (Hnil : wf RB G Pnil Pnil')
               (Hcons : forall x x',
@@ -707,6 +735,10 @@ Module Compilers.
                          | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ]
                            => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
                          | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H
+                         | [ H : List.Forall2 _ ?xs ?ys |- _ ]
+                           => match xs with nil => idtac | _::_ => idtac end;
+                              match ys with nil => idtac | _::_ => idtac end;
+                              inversion H; clear H
                          end
                        | progress subst
                        | progress destruct_head' False
@@ -739,6 +771,8 @@ Module Compilers.
                        | match goal with |- wf _ _ _ _ => constructor end
                        | match goal with
                          | [ H : context[wf _ _ _ _] |- wf _ _ _ _ ] => apply H; eauto with nocore
+                         | [ H : Forall2 (expr.wf _) ?xs ?ys |- Forall2 (expr.wf _) ?xs ?ys ]
+                           => eapply Forall2_Proper_impl; [ .. | exact H ]; repeat intro; try reflexivity
                          end
                        | progress wf_unsafe_t_step
                        | match goal with
@@ -765,7 +799,7 @@ Module Compilers.
           all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
           all: revert dependent k1; revert dependent k2.
           all: lazymatch goal with
-               | [ H : length ?l1 = length ?l2 |- _ ]
+               | [ |- context[List.Forall2 _ ?l1 ?l2] ]
                  => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros
                end;
             wf_reify_and_let_binds_base_cps_t Hk.
@@ -899,6 +933,10 @@ Module Compilers.
                            => pose proof (fun x y pf => H x y (or_introl pf));
                               pose proof (fun x y pf => H x y (or_intror pf));
                               clear H
+                         | [ H : List.Forall2 _ ?xs ?ys |- _ ]
+                           => match xs with nil => idtac | _::_ => idtac end;
+                              match ys with nil => idtac | _::_ => idtac end;
+                              inversion H; clear H
                          end
                        | progress interp_unsafe_t_step
                        | match goal with
@@ -938,7 +976,7 @@ Module Compilers.
           all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
           all: revert dependent k1; revert dependent k2.
           all: lazymatch goal with
-               | [ H : length ?l1 = length ?l2 |- _ ]
+               | [ |- context[List.Forall2 _ ?l1 ?l2 ] ]
                  => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros
                end;
             interp_to_expr_reify_and_let_binds_base_cps_t Hk.