From 4e89dc9568c5e587641a9d22ba837b4123e1c2a5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 11 Nov 2017 01:05:36 -0500 Subject: Add ListUtil.Forall --- src/Util/ListUtil/Forall.v | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 src/Util/ListUtil/Forall.v (limited to 'src/Util/ListUtil') diff --git a/src/Util/ListUtil/Forall.v b/src/Util/ListUtil/Forall.v new file mode 100644 index 000000000..be7bc69cd --- /dev/null +++ b/src/Util/ListUtil/Forall.v @@ -0,0 +1,25 @@ +Require Import Coq.Lists.List. + +Definition Forallb {A} (P : A -> bool) (ls : list A) : bool + := List.fold_right andb true (List.map P ls). + +Lemma unfold_Forallb {A P} ls + : @Forallb A P ls + = match ls with + | nil => true + | cons x xs => andb (P x) (Forallb P xs) + end. +Proof. destruct ls; reflexivity. Qed. + +Lemma Forall_Forallb_iff {A} (P : A -> bool) (Q : A -> Prop) (ls : list A) + (H : forall x, In x ls -> P x = true <-> Q x) + : Forallb P ls = true <-> Forall Q ls. +Proof. + induction ls as [|x xs IHxs]; simpl; rewrite unfold_Forallb. + { intuition. } + { simpl in *. + rewrite Bool.andb_true_iff, IHxs + by (intros; apply H; eauto). + split; intro H'; inversion H'; subst; constructor; intuition; + apply H; eauto. } +Qed. -- cgit v1.2.3