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, 5 insertions, 27 deletions

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.