Commit 863f30c0 by Robbert Krebbers

### Move the defs of set_Forall and set_Exists out of the section.

parent 40e98b1b
 ... @@ -756,33 +756,34 @@ End collection_monad_base. ... @@ -756,33 +756,34 @@ End collection_monad_base. (** * Quantifiers *) (** * 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. Section quantifiers. Context `{SimpleCollection A B} (P : A → Prop). Context `{SimpleCollection A B} (P : A → Prop). Definition set_Forall X := ∀ x, x ∈ X → P x. Lemma set_Forall_empty : set_Forall P ∅. Definition set_Exists X := ∃ x, x ∈ X ∧ P x. Lemma set_Forall_empty : set_Forall ∅. Proof. unfold set_Forall. set_solver. Qed. 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. 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. 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. 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. 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. 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. 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. 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. Proof. unfold set_Exists. set_solver. Qed. Lemma set_Exists_union_inv X Y : 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. Proof. unfold set_Exists. set_solver. Qed. End quantifiers. End quantifiers. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!