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.

1 files changed, 28 insertions, 4 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