Commit 596a0a2c by Robbert Krebbers

### Use ⊆ type class for set-like inclusion of lists.

`This also solves a name clash with the extension order of CMRAs.`
parent db08223a
 ... @@ -711,8 +711,8 @@ Section list_unfold. ... @@ -711,8 +711,8 @@ Section list_unfold. Qed. Qed. Global Instance set_unfold_included l k (P Q : A → Prop) : Global Instance set_unfold_included l k (P Q : A → Prop) : (∀ x, SetUnfold (x ∈ l) (P x)) → (∀ x, SetUnfold (x ∈ k) (Q x)) → (∀ x, SetUnfold (x ∈ l) (P x)) → (∀ x, SetUnfold (x ∈ k) (Q x)) → SetUnfold (l `included` k) (∀ x, P x → Q x). SetUnfold (l ⊆ k) (∀ x, P x → Q x). Proof. by constructor; unfold included; set_unfold. Qed. Proof. by constructor; unfold subseteq, list_subseteq; set_unfold. Qed. End list_unfold. End list_unfold. ... ...
 ... @@ -1225,14 +1225,14 @@ Qed. ... @@ -1225,14 +1225,14 @@ Qed. Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) : m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2. m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m3 ∪ m1 = m3 ∪ m2 → m1 = m2. Proof. Proof. intros. apply (anti_symm (⊆)); intros. apply (anti_symm (⊆)); apply map_union_reflecting_l with m3; apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=(⊆))). auto using (reflexive_eq (R:=@subseteq (M A) _)). Qed. Qed. Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) : Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) : m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2. m1 ⊥ₘ m3 → m2 ⊥ₘ m3 → m1 ∪ m3 = m2 ∪ m3 → m1 = m2. Proof. Proof. intros. apply (anti_symm (⊆)); intros. apply (anti_symm (⊆)); apply map_union_reflecting_r with m3; apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=(⊆))). auto using (reflexive_eq (R:=@subseteq (M A) _)). Qed. Qed. Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) : Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) : m1 ∪ m2 ⊥ₘ m3 ↔ m1 ⊥ₘ m3 ∧ m2 ⊥ₘ m3. m1 ∪ m2 ⊥ₘ m3 ↔ m1 ⊥ₘ m3 ∧ m2 ⊥ₘ m3. ... ...
 ... @@ -303,9 +303,8 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) : ... @@ -303,9 +303,8 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) : | Forall3_cons x y z l k k' : | Forall3_cons x y z l k k' : P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). (** Set operations Decisionon lists *) (** Set operations on lists *) Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2. Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → x ∈ l2. Infix "`included`" := included (at level 70) : C_scope. Section list_set. Section list_set. Context `{dec : EqDecision A}. Context `{dec : EqDecision A}. ... @@ -2046,9 +2045,9 @@ Section contains_dec. ... @@ -2046,9 +2045,9 @@ Section contains_dec. End contains_dec. End contains_dec. (** ** Properties of [included] *) (** ** Properties of [included] *) Global Instance included_preorder : PreOrder (@included A). Global Instance list_subseteq_po : PreOrder (@subseteq (list A) _). Proof. split; firstorder. Qed. Proof. split; firstorder. Qed. Lemma included_nil l : [] `included` l. Lemma list_subseteq_nil l : [] ⊆ l. Proof. intros x. by rewrite elem_of_nil. Qed. Proof. intros x. by rewrite elem_of_nil. Qed. (** ** Properties of the [Forall] and [Exists] predicate *) (** ** Properties of the [Forall] and [Exists] predicate *) ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment