From d95d40c8ce97491b9adeae8466f9bc41526d0c01 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 17:27:57 -0500 Subject: Add more Forall2 lemmas --- src/Util/ListUtil/Forall.v | 50 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v index 7ff7d19d5..d3cb7c861 100644 --- a/src/Util/ListUtil/Forall.v +++ b/src/Util/ListUtil/Forall.v @@ -38,6 +38,7 @@ Local Ltac t_Forall2_step := | progress split_iff | apply conj | progress cbn [List.map List.seq List.repeat List.rev List.firstn List.skipn List.length] in * + | exfalso; assumption | solve [ eauto ] | match goal with | [ |- List.Forall2 _ _ _ ] => constructor @@ -143,3 +144,52 @@ Lemma Forall2_combine {A B C D R1 R2 R3 ls1 ls2 ls3 ls4} Proof using Type. revert ls2 ls3 ls4; induction ls1, ls2, ls3, ls4; t_Forall2. Qed. + +Lemma Forall2_forall_iff_nth_error {A B R xs ys} + : @Forall2 A B R xs ys + <-> forall i, option_eq R (nth_error xs i) (nth_error ys i). +Proof using Type. + revert ys; induction xs as [|x xs IHxs], ys as [|y ys]; + [ | | | specialize (IHxs ys) ]; t_Forall2. + all: repeat first [ t_Forall2_step + | rewrite nth_error_nil_error + | progress cbn [option_eq nth_error] in * + | progress inversion_option + | match goal with + | [ H : forall x, nth_error (cons _ _) x = None |- _ ] => specialize (H O) + | [ H : forall x, option_eq _ (nth_error (cons _ _) x) None |- _ ] => specialize (H O) + | [ H : context[nth_error nil _] |- _ ] + => rewrite nth_error_nil_error in H || setoid_rewrite nth_error_nil_error in H + | [ |- context[nth_error (cons _ _) ?x] ] => is_var x; destruct x + | [ H : forall i, option_eq _ (nth_error (cons _ _) ?x) _ |- _ ] + => pose proof (H O); + pose proof (fun i => H (S i)); + clear H + end ]. +Qed. +Lemma Forall2_forall_iff'' {A B R xs ys d1 d2} + : (@Forall2 A B R xs ys /\ R d1 d2) + <-> (length xs = length ys + /\ (forall i, R (nth_default d1 xs i) (nth_default d2 ys i))). +Proof using Type. + t_Forall2; cbv [nth_default] in *. + all: repeat first [ eapply eq_length_Forall2; eassumption + | rewrite Forall2_forall_iff_nth_error + | t_Forall2_step + | progress cbn [option_eq] in * + | progress inversion_option + | match goal with + | [ H : Forall2 _ _ _ |- _ ] => rewrite Forall2_forall_iff_nth_error in H + | [ H : forall i : nat, _ |- context[nth_error _ ?n] ] + => specialize (H n) + | [ H' : List.length ?ls = _, H : forall i : nat, _ |- _ ] + => specialize (H (List.length ls)); rewrite ?nth_error_length_error in H by lia + end + | break_innermost_match_step + | break_innermost_match_hyps_step + | match goal with + | [ H : nth_error _ _ = None |- _ ] => apply nth_error_error_length in H + | [ H : nth_error _ _ = Some _ |- _ ] => apply nth_error_value_length in H + end + | lia ]. +Qed. -- cgit v1.2.3