Commit 08ce9e37 authored by Robbert Krebbers's avatar Robbert Krebbers

Notations `⊆@{A}` and `⊂@{A}`.

parent 10edecb6
......@@ -812,6 +812,10 @@ Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : stdpp_scope.
Notation "(⊈)" := (λ X Y, X Y) (only parsing) : stdpp_scope.
Notation "( X ⊈)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊈ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊆@{ A }" := (@subseteq A _) (at level 70, only parsing) : stdpp_scope.
Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
Infix "⊆*" := (Forall2 ()) (at level 70) : stdpp_scope.
Notation "(⊆*)" := (Forall2 ()) (only parsing) : stdpp_scope.
Infix "⊆**" := (Forall2 (*)) (at level 70) : stdpp_scope.
......@@ -833,6 +837,9 @@ Notation "(⊄)" := (λ X Y, X ⊄ Y) (only parsing) : stdpp_scope.
Notation "( X ⊄)" := (λ Y, X Y) (only parsing) : stdpp_scope.
Notation "(⊄ X )" := (λ Y, Y X) (only parsing) : stdpp_scope.
Infix "⊂@{ A }" := (strict (@{A})) (at level 70, only parsing) : stdpp_scope.
Notation "(⊂@{ A } )" := (strict (@{A})) (only parsing) : stdpp_scope.
Notation "X ⊆ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊆ Y ⊂ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
Notation "X ⊂ Y ⊆ Z" := (X Y Y Z) (at level 70, Y at next level) : stdpp_scope.
......
......@@ -199,7 +199,7 @@ Proof.
refine (λ X Y, cast_if (decide (X Y = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Instance mapset_subseteq_dec : RelDecision (@subseteq coPset _).
Instance mapset_subseteq_dec : RelDecision (@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.
......
......@@ -315,10 +315,10 @@ Section simple_collection.
Proof. set_solver. Qed.
(** Subset relation *)
Global Instance collection_subseteq_antisymm: AntiSymm () (() : relation C).
Global Instance collection_subseteq_antisymm: AntiSymm () (@{C}).
Proof. intros ??. set_solver. Qed.
Global Instance collection_subseteq_preorder: PreOrder (() : relation C).
Global Instance collection_subseteq_preorder: PreOrder (@{C}).
Proof. split. by intros ??. intros ???; set_solver. Qed.
Lemma subseteq_union X Y : X Y X Y Y.
......@@ -467,8 +467,7 @@ Section simple_collection.
Proof. unfold_leibniz. apply collection_equiv_spec. Qed.
(** Subset relation *)
Global Instance collection_subseteq_partialorder :
PartialOrder (() : relation C).
Global Instance collection_subseteq_partialorder : PartialOrder (@{C}).
Proof. split. apply _. intros ??. unfold_leibniz. apply (anti_symm _). Qed.
Lemma subseteq_union_L X Y : X Y X Y = Y.
......
......@@ -149,7 +149,7 @@ Proof.
Qed.
(** * Induction principles *)
Lemma collection_wf : wf (strict (@subseteq C _)).
Lemma collection_wf : wf (@{C}).
Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
Lemma collection_ind (P : C Prop) :
Proper (() ==> iff) P
......
......@@ -224,7 +224,7 @@ Proof.
destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
done || etrans; eauto.
Qed.
Global Instance map_subseteq_po : PartialOrder (() : relation (M A)).
Global Instance map_subseteq_po : PartialOrder (@{M A}).
Proof.
split; [apply _|].
intros m1 m2; rewrite !map_subseteq_spec.
......@@ -965,7 +965,7 @@ Proof.
destruct (insert_subset_inv m m2 i x) as (m2'&?&?&?); auto; subst.
rewrite !map_to_list_insert; simpl; auto with arith.
Qed.
Lemma map_wf {A} : wf (strict (@subseteq (M A) _)).
Lemma map_wf {A} : wf (@{M A}).
Proof.
apply (wf_projected (<) (length map_to_list)).
- by apply map_to_list_length.
......@@ -1596,13 +1596,13 @@ 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:=@subseteq (M A) _)).
auto using (reflexive_eq (R:=(@{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:=@subseteq (M A) _)).
auto using (reflexive_eq (R:=(@{M A}))).
Qed.
Lemma map_disjoint_union_l {A} (m1 m2 m3 : M A) :
m1 m2 ## m3 m1 ## m3 m2 ## m3.
......
......@@ -231,7 +231,7 @@ Proof.
Qed.
(* Order stuff *)
Global Instance gmultiset_po : PartialOrder (@subseteq (gmultiset A) _).
Global Instance gmultiset_po : PartialOrder (@{gmultiset A}).
Proof.
split; [split|].
- by intros X x.
......@@ -246,7 +246,7 @@ Proof.
apply forall_proper; intros x. unfold multiplicity.
destruct (gmultiset_car X !! x), (gmultiset_car Y !! x); naive_solver omega.
Qed.
Global Instance gmultiset_subseteq_dec : RelDecision (@subseteq (gmultiset A) _).
Global Instance gmultiset_subseteq_dec : RelDecision (@{gmultiset A}).
Proof.
refine (λ X Y, cast_if (decide (map_relation ()
(λ _, False) (λ _, True) (gmultiset_car X) (gmultiset_car Y))));
......@@ -342,7 +342,7 @@ Proof.
Qed.
(* Well-foundedness *)
Lemma gmultiset_wf : wf (strict (@subseteq (gmultiset A) _)).
Lemma gmultiset_wf : wf (@{gmultiset A}).
Proof.
apply (wf_projected (<) size); auto using gmultiset_subset_size, lt_wf.
Qed.
......
......@@ -2124,7 +2124,7 @@ Section submseteq_dec.
End submseteq_dec.
(** ** Properties of [included] *)
Global Instance list_subseteq_po : PreOrder (@subseteq (list A) _).
Global Instance list_subseteq_po : PreOrder (@{list A}).
Proof. split; firstorder. Qed.
Lemma list_subseteq_nil l : [] l.
Proof. intros x. by rewrite elem_of_nil. Qed.
......
......@@ -85,7 +85,7 @@ Section deciders.
refine (λ X1 X2, cast_if (decide (X1 X2 = )));
abstract (by rewrite disjoint_intersection_L).
Defined.
Global Instance mapset_subseteq_dec : RelDecision (@subseteq (mapset M) _).
Global Instance mapset_subseteq_dec : RelDecision (@{mapset M}).
Proof.
refine (λ X1 X2, cast_if (decide (X1 X2 = X2)));
abstract (by rewrite subseteq_union_L).
......
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