Relate `forallb`/`existsb` to `Forall`/`Exists`.

e37edc7e · Robbert Krebbers · b6d58ca6 · e37edc7e
Commit e37edc7e authored Jan 17, 2018 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

theories/list.v theories/list.v +5 -0

No files found.
--- a/theories/list.v
+++ b/theories/list.v
@@ -2331,6 +2331,11 @@ Section Forall_Exists.
    end.
 End Forall_Exists.

+Lemma forallb_True (f : A → bool) xs : forallb f xs ↔ Forall f xs.
+Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+Lemma existb_True (f : A → bool) xs : existsb f xs ↔ Exists f xs.
+Proof. split. induction xs; naive_solver. induction 1; naive_solver. Qed.
+
 Lemma replicate_as_Forall (x : A) n l :
  replicate n x = l ↔ length l = n ∧ Forall (x =) l.
 Proof. rewrite replicate_as_elem_of, Forall_forall. naive_solver. Qed.