From 6281aef8fcc940b0a38d7c5491a0655114bd9a2a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 19 Oct 2016 13:38:56 -0400 Subject: Add fold_right_andb_true_iff_fold_right_and_True --- src/Util/ListUtil.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Util/ListUtil.v') diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 84553d64b..9131a0d20 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1543,6 +1543,13 @@ Proof. intuition (congruence || eauto). Qed. +Lemma fold_right_andb_true_iff_fold_right_and_True (ls : list bool) + : List.fold_right andb true ls = true <-> List.fold_right and True (List.map (fun b => b = true) ls). +Proof. + rewrite <- (map_id ls) at 1. + 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))). Proof. -- cgit v1.2.3