Commit 186da990 authored by Robbert Krebbers's avatar Robbert Krebbers

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

This also solves a name clash with the extension order of CMRAs.
parent 7b63a3da
Pipeline #2719 passed with stage
in 9 minutes and 22 seconds
......@@ -318,11 +318,11 @@ Lemma alloc_fresh e v σ :
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
(** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e X `included` Y is_closed Y e.
Lemma is_closed_weaken X Y e : is_closed X e X Y is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma is_closed_weaken_nil X e : is_closed [] e is_closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e x X subst x es e = e.
Proof.
......
......@@ -711,8 +711,8 @@ Section list_unfold.
Qed.
Global Instance set_unfold_included l k (P Q : A Prop) :
( x, SetUnfold (x l) (P x)) ( x, SetUnfold (x k) (Q x))
SetUnfold (l `included` k) ( x, P x Q x).
Proof. by constructor; unfold included; set_unfold. Qed.
SetUnfold (l k) ( x, P x Q x).
Proof. by constructor; unfold subseteq, list_subseteq; set_unfold. Qed.
End list_unfold.
......
......@@ -1225,14 +1225,14 @@ Qed.
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m3 m2 ⊥ₘ m3 m3 m1 = m3 m2 m1 = m2.
Proof.
intros. apply (anti_symm ());
apply map_union_reflecting_l with m3; auto using (reflexive_eq (R:=())).
intros. apply (anti_symm ()); apply map_union_reflecting_l with m3;
auto using (reflexive_eq (R:=@subseteq (M A) _)).
Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 ⊥ₘ m3 m2 ⊥ₘ m3 m1 m3 = m2 m3 m1 = m2.
Proof.
intros. apply (anti_symm ());
apply map_union_reflecting_r with m3; auto using (reflexive_eq (R:=())).
intros. apply (anti_symm ()); apply map_union_reflecting_r with m3;
auto using (reflexive_eq (R:=@subseteq (M A) _)).
Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
m1 m2 ⊥ₘ m3 m1 ⊥ₘ m3 m2 ⊥ₘ m3.
......
......@@ -303,9 +303,8 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
| 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').
(** Set operations Decisionon lists *)
Definition included {A} (l1 l2 : list A) := x, x l1 x l2.
Infix "`included`" := included (at level 70) : C_scope.
(** Set operations on lists *)
Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, x, x l1 x l2.
Section list_set.
Context `{dec : EqDecision A}.
......@@ -2046,9 +2045,9 @@ Section contains_dec.
End contains_dec.
(** ** Properties of [included] *)
Global Instance included_preorder : PreOrder (@included A).
Global Instance list_subseteq_po : PreOrder (@subseteq (list A) _).
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.
(** ** 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