From 863f30c014887d5f87e80b20d2f65a397e2c9208 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 21 Nov 2016 15:40:30 +0100 Subject: [PATCH] Move the defs of set_Forall and set_Exists out of the section. --- prelude/collections.v | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/prelude/collections.v b/prelude/collections.v index f5e77ccb..1ff1e7b1 100644 --- a/prelude/collections.v +++ b/prelude/collections.v @@ -756,33 +756,34 @@ End collection_monad_base. (** * Quantifiers *) +Definition set_Forall `{ElemOf A C} (P : A → Prop) (X : C) := ∀ x, x ∈ X → P x. +Definition set_Exists `{ElemOf A C} (P : A → Prop) (X : C) := ∃ x, x ∈ X ∧ P x. + Section quantifiers. Context `{SimpleCollection A B} (P : A → Prop). - Definition set_Forall X := ∀ x, x ∈ X → P x. - Definition set_Exists X := ∃ x, x ∈ X ∧ P x. - - Lemma set_Forall_empty : set_Forall ∅. + Lemma set_Forall_empty : set_Forall P ∅. Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Forall_singleton x : set_Forall {[ x ]} ↔ P x. + Lemma set_Forall_singleton x : set_Forall P {[ x ]} ↔ P x. Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Forall_union X Y : set_Forall X → set_Forall Y → set_Forall (X ∪ Y). + Lemma set_Forall_union X Y : + set_Forall P X → set_Forall P Y → set_Forall P (X ∪ Y). Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Forall_union_inv_1 X Y : set_Forall (X ∪ Y) → set_Forall X. + Lemma set_Forall_union_inv_1 X Y : set_Forall P (X ∪ Y) → set_Forall P X. Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Forall_union_inv_2 X Y : set_Forall (X ∪ Y) → set_Forall Y. + Lemma set_Forall_union_inv_2 X Y : set_Forall P (X ∪ Y) → set_Forall P Y. Proof. unfold set_Forall. set_solver. Qed. - Lemma set_Exists_empty : ¬set_Exists ∅. + Lemma set_Exists_empty : ¬set_Exists P ∅. Proof. unfold set_Exists. set_solver. Qed. - Lemma set_Exists_singleton x : set_Exists {[ x ]} ↔ P x. + Lemma set_Exists_singleton x : set_Exists P {[ x ]} ↔ P x. Proof. unfold set_Exists. set_solver. Qed. - Lemma set_Exists_union_1 X Y : set_Exists X → set_Exists (X ∪ Y). + Lemma set_Exists_union_1 X Y : set_Exists P X → set_Exists P (X ∪ Y). Proof. unfold set_Exists. set_solver. Qed. - Lemma set_Exists_union_2 X Y : set_Exists Y → set_Exists (X ∪ Y). + Lemma set_Exists_union_2 X Y : set_Exists P Y → set_Exists P (X ∪ Y). Proof. unfold set_Exists. set_solver. Qed. Lemma set_Exists_union_inv X Y : - set_Exists (X ∪ Y) → set_Exists X ∨ set_Exists Y. + set_Exists P (X ∪ Y) → set_Exists P X ∨ set_Exists P Y. Proof. unfold set_Exists. set_solver. Qed. End quantifiers. -- GitLab