diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/ListUtil/Forall.v | 25 |
2 files changed, 26 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index ee096ee70..30b5c9c70 100644 --- a/_CoqProject +++ b/_CoqProject @@ -4187,6 +4187,7 @@ src/Util/ForLoop/InvariantFramework.v src/Util/ForLoop/Tests.v src/Util/ForLoop/Unrolling.v src/Util/ListUtil/FoldBool.v +src/Util/ListUtil/Forall.v src/Util/Logic/ImplAnd.v src/Util/SideConditions/Autosolve.v src/Util/SideConditions/CorePackages.v 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. |