From 3fd9d15cfeb0b3c5de09c7a53e0fb91033fee908 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Dec 2018 16:54:41 -0500 Subject: Add more ListUtil Forall Lemmas --- src/Util/ListUtil/Forall.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'src/Util') diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v index a537edb19..7ff7d19d5 100644 --- a/src/Util/ListUtil/Forall.v +++ b/src/Util/ListUtil/Forall.v @@ -37,7 +37,7 @@ Local Ltac t_Forall2_step := | progress specialize_by_assumption | progress split_iff | apply conj - | progress cbn [List.map List.seq List.repeat List.rev List.firstn List.skipn] in * + | progress cbn [List.map List.seq List.repeat List.rev List.firstn List.skipn List.length] in * | solve [ eauto ] | match goal with | [ |- List.Forall2 _ _ _ ] => constructor @@ -128,3 +128,18 @@ Lemma Forall2_skipn {A B R ls1 ls2 n} Proof using Type. revert ls1 ls2; induction n as [|n IHn], ls1 as [|l1 ls2], ls2 as [|l2 ls2]; t_Forall2. Qed. + +Lemma eq_length_Forall2 {A B R ls1 ls2} + : @List.Forall2 A B R ls1 ls2 -> List.length ls1 = List.length ls2. +Proof using Type. + revert ls2; induction ls1, ls2; t_Forall2. +Qed. + +Lemma Forall2_combine {A B C D R1 R2 R3 ls1 ls2 ls3 ls4} + (HR : forall x y z w, (R1 x y : Prop) -> (R2 z w : Prop) -> (R3 (x, z) (y, w) : Prop)) + : @List.Forall2 A B R1 ls1 ls2 + -> @List.Forall2 C D R2 ls3 ls4 + -> List.Forall2 R3 (List.combine ls1 ls3) (List.combine ls2 ls4). +Proof using Type. + revert ls2 ls3 ls4; induction ls1, ls2, ls3, ls4; t_Forall2. +Qed. -- cgit v1.2.3