From 55e4267912401456dc762d7987d4e5914b3bdde4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Nov 2017 21:42:26 -0500 Subject: Generalize Forall2_forall_iff --- src/Util/ListUtil.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index ee4fb0b9b..38678ac59 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1654,10 +1654,10 @@ Proof. rewrite fold_right_andb_true_map_iff, fold_right_and_True_forall_In_iff; reflexivity. Qed. -Lemma Forall2_forall_iff : forall {A} R (xs ys : list A) d, length xs = length ys -> - (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). +Lemma Forall2_forall_iff : forall {A B} (R : A -> B -> Prop) (xs : list A) (ys : list B) d1 d2, length xs = length ys -> + (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d1 xs i) (nth_default d2 ys i))). Proof. - intros A R xs ys d H; split; [ intros H0 i H1 | intros H0 ]. + intros A B R xs ys d1 d2 H; split; [ intros H0 i H1 | intros H0 ]. + revert xs ys H H0 H1. induction i as [|i IHi]; intros xs ys H H0 H1; destruct H0; distr_length; autorewrite with push_nth_default; auto. @@ -1673,6 +1673,10 @@ Proof. apply H0; omega. Qed. +Lemma Forall2_forall_iff' : forall {A} R (xs ys : list A) d, length xs = length ys -> + (Forall2 R xs ys <-> (forall i, (i < length xs)%nat -> R (nth_default d xs i) (nth_default d ys i))). +Proof. intros; apply Forall2_forall_iff; assumption. Qed. + Lemma nth_default_firstn : forall {A} (d : A) l i n, nth_default d (firstn n l) i = if le_dec n (length l) then if lt_dec i n then nth_default d l i else d @@ -1774,4 +1778,4 @@ Lemma map2_map {A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:list A' Proof. revert ys; induction xs as [|a xs IHxs]; destruct ys; intros; try reflexivity; []. simpl. rewrite IHxs. reflexivity. -Qed. \ No newline at end of file +Qed. -- cgit v1.2.3