diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-09 21:42:26 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-09 21:42:26 -0500 |
commit | 55e4267912401456dc762d7987d4e5914b3bdde4 (patch) | |
tree | 70e6c2416cf3d76c04bd2e21224c7abd56f4a5fa | |
parent | 11f0cdcc3ab2518ffcdb23426168ae74f48358c2 (diff) |
Generalize Forall2_forall_iff
-rw-r--r-- | src/Util/ListUtil.v | 12 |
1 files changed, 8 insertions, 4 deletions
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. |