Skip to content

GitLab

S
stdpp
Commit a8477867 authored by Robbert's avatar Robbert
Browse files
Options

Merge branch 'robbert/rel_disambig' into 'master' 

Notations for relations with explicit type arguments

See merge request robbertkrebbers/coq-stdpp!30
parents 3bcaaf7e ba69172b
Pipeline #7805 passed with stage
    in 24 minutes and 49 seconds
    Show whitespace changes
    Inline Side-by-side
    Showing with 195 additions and 169 deletions
    theories/base.v
    View file @ a8477867
    ......@@ -159,10 +159,16 @@ 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 }" := (@eq A)
    (at level 70, only parsing, no associativity) : stdpp_scope.
    Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
    Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
    Notation "X ≠@{ A } Y":= (¬X =@{ A } Y) (at level 70, no associativity) : stdpp_scope.
    Hint Extern 0 (_ = _) => reflexivity.
    Hint Extern 100 (_ ≠ _) => discriminate.
    Instance: @PreOrder A (=).
    Instance: ∀ A, PreOrder (=@{A}).
    Proof. split; repeat intro; congruence. Qed.
    (** ** Setoid equality *)
    ......@@ -174,6 +180,9 @@ Class Equiv A := equiv: relation A.
    Hint Mode Equiv ! : typeclass_instances. *)
    Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
    Infix "≡@{ A }" := (@equiv A _)
    (at level 70, only parsing, no associativity) : stdpp_scope.
    Notation "(≡)" := equiv (only parsing) : stdpp_scope.
    Notation "( X ≡)" := (equiv X) (only parsing) : stdpp_scope.
    Notation "(≡ X )" := (λ Y, Y ≡ X) (only parsing) : stdpp_scope.
    ......@@ -182,6 +191,10 @@ Notation "X ≢ Y":= (¬X ≡ Y) (at level 70, no associativity) : stdpp_scope.
    Notation "( X ≢)" := (λ Y, X ≢ Y) (only parsing) : stdpp_scope.
    Notation "(≢ X )" := (λ Y, Y ≢ X) (only parsing) : stdpp_scope.
    Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
    Notation "(≢@{ A } )" := (λ X Y, ¬X ≡@{A} Y) (only parsing) : stdpp_scope.
    Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y) (at level 70, no associativity) : stdpp_scope.
    (** The type class [LeibnizEquiv] collects setoid equalities that coincide
    with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
    setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
    ......@@ -189,22 +202,22 @@ reverse. *)
    Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
    Hint Mode LeibnizEquiv ! - : typeclass_instances.
    Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
    Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
    x ≡ y ↔ x = y.
    Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
    Ltac fold_leibniz := repeat
    match goal with
    | H : context [ @equiv ?A _ _ _ ] |- _ =>
    | H : context [ _ ≡@{?A} _ ] |- _ =>
    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
    | |- context [ @equiv ?A _ _ _ ] =>
    | |- context [ _ ≡@{?A} _ ] =>
    setoid_rewrite (leibniz_equiv_iff (A:=A))
    end.
    Ltac unfold_leibniz := repeat
    match goal with
    | H : context [ @eq ?A _ _ ] |- _ =>
    | H : context [ _ =@{?A} _ ] |- _ =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
    | |- context [ @eq ?A _ _ ] =>
    | |- context [ _ =@{?A} _ ] =>
    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
    end.
    ......@@ -249,7 +262,7 @@ Class RelDecision {A B} (R : A → B → Prop) :=
    decide_rel x y :> Decision (R x y).
    Hint Mode RelDecision ! ! ! : typeclass_instances.
    Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
    Notation EqDecision A := (RelDecision (@eq A)).
    Notation EqDecision A := (RelDecision (=@{A})).
    (** ** Inhabited types *)
    (** This type class collects types that are inhabited. *)
    ......@@ -411,9 +424,9 @@ Lemma exist_proper {A} (P Q : A → Prop) :
    (∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
    Proof. firstorder. Qed.
    Instance: Comm (↔) (@eq A).
    Instance: Comm (↔) (=@{A}).
    Proof. red; intuition. Qed.
    Instance: Comm (↔) (λ x y, @eq A y x).
    Instance: Comm (↔) (λ x y, y =@{A} x).
    Proof. red; intuition. Qed.
    Instance: Comm (↔) (↔).
    Proof. red; intuition. Qed.
    ......@@ -551,7 +564,7 @@ Proof. now intros -> ?. Qed.
    (** ** Unit *)
    Instance unit_equiv : Equiv unit := λ _ _, True.
    Instance unit_equivalence : Equivalence (@equiv unit _).
    Instance unit_equivalence : Equivalence (≡@{unit}).
    Proof. repeat split. Qed.
    Instance unit_leibniz : LeibnizEquiv unit.
    Proof. intros [] []; reflexivity. Qed.
    ......@@ -799,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.
    ......@@ -820,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.
    ......@@ -843,6 +863,9 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope.
    Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : stdpp_scope.
    Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
    Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
    Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
    Class Disjoint A := disjoint : A → A → Prop.
    Hint Mode Disjoint ! : typeclass_instances.
    Instance: Params (@disjoint) 2.
    ......@@ -850,6 +873,10 @@ Infix "##" := disjoint (at level 70) : stdpp_scope.
    Notation "(##)" := disjoint (only parsing) : stdpp_scope.
    Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
    Notation "(.## X )" := (λ Y, Y ## X) (only parsing) : stdpp_scope.
    Infix "##@{ A }" := (@disjoint A _) (at level 70, only parsing) : stdpp_scope.
    Notation "(##@{ A } )" := (@disjoint 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.
    ......@@ -881,17 +908,19 @@ Class DisjointList A := disjoint_list : list A → Prop.
    Hint Mode DisjointList ! : typeclass_instances.
    Instance: Params (@disjoint_list) 2.
    Notation "## Xs" := (disjoint_list Xs) (at level 20, format "## Xs") : stdpp_scope.
    Notation "##@{ A } Xs" :=
    (@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
    Section disjoint_list.
    Context `{Disjoint A, Union A, Empty A}.
    Implicit Types X : A.
    Inductive disjoint_list_default : DisjointList A :=
    | disjoint_nil_2 : ## (@nil A)
    | disjoint_nil_2 : ##@{A} []
    | disjoint_cons_2 (X : A) (Xs : list A) : X ## ⋃ Xs → ## Xs → ## (X :: Xs).
    Global Existing Instance disjoint_list_default.
    Lemma disjoint_list_nil : ## @nil A ↔ True.
    Lemma disjoint_list_nil : ##@{A} [] ↔ True.
    Proof. split; constructor. Qed.
    Lemma disjoint_list_cons X Xs : ## (X :: Xs) ↔ X ## ⋃ Xs ∧ ## Xs.
    Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
    ......@@ -1175,6 +1204,10 @@ Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
    Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
    Notation "( x ⊑)" := (sqsubseteq x) (only parsing) : stdpp_scope.
    Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
    Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
    Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
    Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
    Hint Extern 0 (_ ⊑ _) => reflexivity.
    ......
    theories/bset.v
    View file @ a8477867
    ......@@ -29,7 +29,7 @@ Proof.
    - intros X Y x; unfold elem_of, bset_elem_of; simpl.
    destruct (bset_car X x), (bset_car Y x); simpl; tauto.
    Qed.
    Instance bset_elem_of_dec {A} : RelDecision (@elem_of _ (bset A) _).
    Instance bset_elem_of_dec {A} : RelDecision (∈@{bset A}).
    Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
    Typeclasses Opaque bset_elem_of.
    ......
    theories/coPset.v
    View file @ a8477867
    ......@@ -190,16 +190,16 @@ Proof.
    intros p; apply eq_bool_prop_intro, (HXY p).
    Qed.
    Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _).
    Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
    Proof. solve_decision. Defined.
    Instance coPset_equiv_dec : RelDecision (@equiv coPset _).
    Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
    Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
    Instance mapset_disjoint_dec : RelDecision (@disjoint coPset _).
    Instance mapset_disjoint_dec : RelDecision (##@{coPset}).
    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.
    ......
    theories/collections.v
    View file @ a8477867
    ......@@ -19,27 +19,26 @@ Typeclasses Opaque collection_equiv collection_subseteq collection_disjoint.
    Section setoids_simple.
    Context `{SimpleCollection A C}.
    Global Instance collection_equivalence: @Equivalence C (≡).
    Global Instance collection_equivalence : Equivalence (≡@{C}).
    Proof.
    split.
    - done.
    - intros X Y ? x. by symmetry.
    - intros X Y Z ?? x; by trans (x ∈ Y).
    Qed.
    Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)).
    Global Instance singleton_proper : Proper ((=) ==> (≡@{C})) singleton.
    Proof. apply _. Qed.
    Global Instance elem_of_proper :
    Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
    Global Instance elem_of_proper : Proper ((=) ==> (≡) ==> iff) (∈@{C}) | 5.
    Proof. by intros x ? <- X Y. Qed.
    Global Instance disjoint_proper: Proper ((≡) ==> (≡) ==> iff) (@disjoint C _).
    Global Instance disjoint_proper: Proper ((≡) ==> (≡) ==> iff) (##@{C}).
    Proof.
    intros X1 X2 HX Y1 Y2 HY; apply forall_proper; intros x. by rewrite HX, HY.
    Qed.
    Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡)) (@union C _).
    Global Instance union_proper : Proper ((≡) ==> (≡) ==> (≡@{C})) union.
    Proof. intros X1 X2 HX Y1 Y2 HY x. rewrite !elem_of_union. f_equiv; auto. Qed.
    Global Instance union_list_proper: Proper ((≡) ==> (≡)) (union_list (A:=C)).
    Global Instance union_list_proper: Proper ((≡) ==> (≡@{C})) union_list.
    Proof. by induction 1; simpl; try apply union_proper. Qed.
    Global Instance subseteq_proper : Proper ((≡) ==> (≡) ==> iff) ((⊆) : relation C).
    Global Instance subseteq_proper : Proper ((≡@{C}) ==> (≡@{C}) ==> iff) (⊆).
    Proof.
    intros X1 X2 HX Y1 Y2 HY. apply forall_proper; intros x. by rewrite HX, HY.
    Qed.
    ......@@ -50,12 +49,12 @@ Section setoids.
    (** * Setoids *)
    Global Instance intersection_proper :
    Proper ((≡) ==> (≡) ==> (≡)) (@intersection C _).
    Proper ((≡) ==> (≡) ==> (≡@{C})) intersection.
    Proof.
    intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_intersection, HX, HY.
    Qed.
    Global Instance difference_proper :
    Proper ((≡) ==> (≡) ==> (≡)) (@difference C _).
    Proper ((≡) ==> (≡) ==> (≡@{C})) difference.
    Proof.
    intros X1 X2 HX Y1 Y2 HY x. by rewrite !elem_of_difference, HX, HY.
    Qed.
    ......@@ -316,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.
    ......@@ -357,15 +356,15 @@ Section simple_collection.
    Lemma union_mono X1 X2 Y1 Y2 : X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∪ Y1 ⊆ X2 ∪ Y2.
    Proof. set_solver. Qed.
    Global Instance union_idemp : IdemP ((≡) : relation C) (∪).
    Global Instance union_idemp : IdemP (≡@{C}) (∪).
    Proof. intros X. set_solver. Qed.
    Global Instance union_empty_l : LeftId ((≡) : relation C) ∅ (∪).
    Global Instance union_empty_l : LeftId (≡@{C}) ∅ (∪).
    Proof. intros X. set_solver. Qed.
    Global Instance union_empty_r : RightId ((≡) : relation C) ∅ (∪).
    Global Instance union_empty_r : RightId (≡@{C}) ∅ (∪).
    Proof. intros X. set_solver. Qed.
    Global Instance union_comm : Comm ((≡) : relation C) (∪).
    Global Instance union_comm : Comm (≡@{C}) (∪).
    Proof. intros X Y. set_solver. Qed.
    Global Instance union_assoc : Assoc ((≡) : relation C) (∪).
    Global Instance union_assoc : Assoc (≡@{C}) (∪).
    Proof. intros X Y Z. set_solver. Qed.
    Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
    ......@@ -408,7 +407,7 @@ Section simple_collection.
    Lemma elem_of_disjoint X Y : X ## Y ↔ ∀ x, x ∈ X → x ∈ Y → False.
    Proof. done. Qed.
    Global Instance disjoint_sym : Symmetric (@disjoint C _).
    Global Instance disjoint_sym : Symmetric (##@{C}).
    Proof. intros X Y. set_solver. Qed.
    Lemma disjoint_empty_l Y : ∅ ## Y.
    Proof. set_solver. Qed.
    ......@@ -468,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.
    ......@@ -480,15 +478,15 @@ Section simple_collection.
    Proof. unfold_leibniz. apply subseteq_union_2. Qed.
    (** Union *)
    Global Instance union_idemp_L : IdemP (@eq C) (∪).
    Global Instance union_idemp_L : IdemP (=@{C}) (∪).
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
    Global Instance union_empty_l_L : LeftId (@eq C) ∅ (∪).
    Global Instance union_empty_l_L : LeftId (=@{C}) ∅ (∪).
    Proof. intros ?. unfold_leibniz. apply (left_id _ _). Qed.
    Global Instance union_empty_r_L : RightId (@eq C) ∅ (∪).
    Global Instance union_empty_r_L : RightId (=@{C}) ∅ (∪).
    Proof. intros ?. unfold_leibniz. apply (right_id _ _). Qed.
    Global Instance union_comm_L : Comm (@eq C) (∪).
    Global Instance union_comm_L : Comm (=@{C}) (∪).
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
    Global Instance union_assoc_L : Assoc (@eq C) (∪).
    Global Instance union_assoc_L : Assoc (=@{C}) (∪).
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
    Lemma empty_union_L X Y : X ∪ Y = ∅ ↔ X = ∅ ∧ Y = ∅.
    ......@@ -527,7 +525,7 @@ Section simple_collection.
    End leibniz.
    Section dec.
    Context `{!RelDecision (@equiv C _)}.
    Context `{!RelDecision (≡@{C})}.
    Lemma collection_subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
    Proof. destruct (decide (X ≡ Y)); [by right|left;set_solver]. Qed.
    Lemma collection_not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
    ......@@ -580,15 +578,15 @@ Section collection.
    X1 ⊆ X2 → Y1 ⊆ Y2 → X1 ∩ Y1 ⊆ X2 ∩ Y2.
    Proof. set_solver. Qed.
    Global Instance intersection_idemp : IdemP ((≡) : relation C) (∩).
    Global Instance intersection_idemp : IdemP (≡@{C}) (∩).
    Proof. intros X; set_solver. Qed.
    Global Instance intersection_comm : Comm ((≡) : relation C) (∩).
    Global Instance intersection_comm : Comm (≡@{C}) (∩).
    Proof. intros X Y; set_solver. Qed.
    Global Instance intersection_assoc : Assoc ((≡) : relation C) (∩).
    Global Instance intersection_assoc : Assoc (≡@{C}) (∩).
    Proof. intros X Y Z; set_solver. Qed.
    Global Instance intersection_empty_l : LeftAbsorb ((≡) : relation C) ∅ (∩).
    Global Instance intersection_empty_l : LeftAbsorb (≡@{C}) ∅ (∩).
    Proof. intros X; set_solver. Qed.
    Global Instance intersection_empty_r: RightAbsorb ((≡) : relation C) ∅ (∩).
    Global Instance intersection_empty_r: RightAbsorb (≡@{C}) ∅ (∩).
    Proof. intros X; set_solver. Qed.
    Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
    ......@@ -647,15 +645,15 @@ Section collection.
    Lemma subseteq_intersection_2_L X Y : X ∩ Y = X → X ⊆ Y.
    Proof. unfold_leibniz. apply subseteq_intersection_2. Qed.
    Global Instance intersection_idemp_L : IdemP ((=) : relation C) (∩).
    Global Instance intersection_idemp_L : IdemP (=@{C}) (∩).
    Proof. intros ?. unfold_leibniz. apply (idemp _). Qed.
    Global Instance intersection_comm_L : Comm ((=) : relation C) (∩).
    Global Instance intersection_comm_L : Comm (=@{C}) (∩).
    Proof. intros ??. unfold_leibniz. apply (comm _). Qed.
    Global Instance intersection_assoc_L : Assoc ((=) : relation C) (∩).
    Global Instance intersection_assoc_L : Assoc (=@{C}) (∩).
    Proof. intros ???. unfold_leibniz. apply (assoc _). Qed.
    Global Instance intersection_empty_l_L: LeftAbsorb ((=) : relation C) ∅ (∩).
    Global Instance intersection_empty_l_L: LeftAbsorb (=@{C}) ∅ (∩).
    Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
    Global Instance intersection_empty_r_L: RightAbsorb ((=) : relation C) ∅ (∩).
    Global Instance intersection_empty_r_L: RightAbsorb (=@{C}) ∅ (∩).
    Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
    Lemma intersection_singletons_L x : {[x]} ∩ {[x]} = ({[x]} : C).
    ......@@ -695,7 +693,7 @@ Section collection.
    End leibniz.
    Section dec.
    Context `{!RelDecision (@elem_of A C _)}.
    Context `{!RelDecision (∈@{C})}.
    Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
    Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
    Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
    ......@@ -776,17 +774,17 @@ Section of_option_list.
    SetUnfold (x ∈ l) P → SetUnfold (x ∈ of_list (C:=C) l) P.
    Proof. constructor. by rewrite elem_of_of_list, (set_unfold (x ∈ l) P). Qed.
    Lemma of_list_nil : of_list (C:=C) [] = ∅.
    Lemma of_list_nil : of_list [] =@{C} ∅.
    Proof. done. Qed.
    Lemma of_list_cons x l : of_list (C:=C) (x :: l) = {[ x ]} ∪ of_list l.
    Lemma of_list_cons x l : of_list (x :: l) =@{C} {[ x ]} ∪ of_list l.
    Proof. done. Qed.
    Lemma of_list_app l1 l2 : of_list (C:=C) (l1 ++ l2) ≡ of_list l1 ∪ of_list l2.
    Lemma of_list_app l1 l2 : of_list (l1 ++ l2) ≡@{C} of_list l1 ∪ of_list l2.
    Proof. set_solver. Qed.
    Global Instance of_list_perm : Proper ((≡ₚ) ==> (≡)) (of_list (C:=C)).
    Proof. induction 1; set_solver. Qed.
    Context `{!LeibnizEquiv C}.
    Lemma of_list_app_L l1 l2 : of_list (C:=C) (l1 ++ l2) = of_list l1 ∪ of_list l2.
    Lemma of_list_app_L l1 l2 : of_list (l1 ++ l2) =@{C} of_list l1 ∪ of_list l2.
    Proof. set_solver. Qed.
    Global Instance of_list_perm_L : Proper ((≡ₚ) ==> (=)) (of_list (C:=C)).
    Proof. induction 1; set_solver. Qed.
    ......@@ -887,10 +885,9 @@ Section fresh.
    Context `{FreshSpec A C}.
    Implicit Types X Y : C.
    Global Instance fresh_proper: Proper ((≡) ==> (=)) (fresh (C:=C)).
    Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
    Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
    Global Instance fresh_list_proper n:
    Proper ((≡) ==> (=)) (fresh_list (C:=C) n).
    Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
    Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
    Lemma exist_fresh X : ∃ x, x ∉ X.
    ......@@ -1058,13 +1055,13 @@ Section seq_set.
    Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
    Lemma seq_set_S_union start len :
    seq_set start (C:=C) (S len) ≡ {[ start + len ]} ∪ seq_set start len.
    seq_set start (S len) ≡@{C} {[ start + len ]} ∪ seq_set start len.
    Proof.
    intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega.
    Qed.
    Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
    seq_set start (C:=C) (S len) = {[ start + len ]} ∪ seq_set start len.
    seq_set start (S len) =@{C} {[ start + len ]} ∪ seq_set start len.
    Proof. unfold_leibniz. apply seq_set_S_union. Qed.
    End seq_set.
    ......@@ -1078,7 +1075,7 @@ Section minimal.
    Context `{SimpleCollection A C} {R : relation A}.
    Implicit Types X Y : C.
    Global Instance minimal_proper x : Proper (@equiv C _ ==> iff) (minimal R x).
    Global Instance minimal_proper x : Proper ((≡@{C}) ==> iff) (minimal R x).
    Proof. intros X X' y; unfold minimal; set_solver. Qed.
    Lemma minimal_anti_symm_1 `{!AntiSymm (=) R} X x y :
    ......
    theories/fin_collections.v
    View file @ a8477867
    ......@@ -23,7 +23,7 @@ Implicit Types X Y : C.
    Lemma fin_collection_finite X : set_finite X.
    Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
    Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100.
    Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
    Proof.
    refine (λ x X, cast_if (decide_rel (∈) x (elements X)));
    by rewrite <-(elem_of_elements _).
    ......@@ -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 →
    ......
    theories/fin_maps.v
    View file @ a8477867
    ......@@ -147,38 +147,34 @@ Section setoid.
    m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
    Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
    Global Instance map_equivalence :
    Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (M A)).
    Global Instance map_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{M A}).
    Proof.
    split.
    - by intros m i.
    - by intros m1 m2 ? i.
    - by intros m1 m2 m3 ?? i; trans (m2 !! i).
    Qed.
    Global Instance lookup_proper (i : K) :
    Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
    Global Instance lookup_proper (i : K) : Proper ((≡@{M A}) ==> (≡)) (lookup i).
    Proof. by intros m1 m2 Hm. Qed.
    Global Instance partial_alter_proper :
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) partial_alter.
    Proof.
    by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
    rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
    try apply Hf; apply lookup_proper.
    Qed.
    Global Instance insert_proper (i : K) :
    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
    Proper ((≡) ==> (≡) ==> (≡@{M A})) (insert i).
    Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
    Global Instance singleton_proper k :
    Proper ((≡) ==> (≡)) (singletonM k : A → M A).
    Global Instance singleton_proper k : Proper ((≡) ==> (≡@{M A})) (singletonM k).
    Proof.
    intros ???; apply insert_proper; [done|].
    intros ?. rewrite lookup_empty; constructor.
    Qed.
    Global Instance delete_proper (i : K) :
    Proper ((≡) ==> (≡)) (delete (M:=M A) i).
    Global Instance delete_proper (i : K) : Proper ((≡) ==> (≡@{M A})) (delete i).
    Proof. by apply partial_alter_proper; [constructor|]. Qed.
    Global Instance alter_proper :
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{M A})) alter.
    Proof.
    intros ?? Hf; apply partial_alter_proper.
    by destruct 1; constructor; apply Hf.
    ......@@ -186,12 +182,12 @@ Section setoid.
    Lemma merge_ext `{Equiv B, Equiv C} (f g : option A → option B → option C)
    `{!DiagNone f, !DiagNone g} :
    ((≡) ==> (≡) ==> (≡))%signature f g →
    ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
    ((≡) ==> (≡) ==> (≡@{M _}))%signature (merge f) (merge g).
    Proof.
    by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
    Qed.
    Global Instance union_with_proper :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) union_with.
    Proof.
    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
    by do 2 destruct 1; first [apply Hf | constructor].
    ......@@ -205,7 +201,7 @@ Section setoid.
    - intros ?. rewrite lookup_empty; constructor.
    Qed.
    Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f).
    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{M _})) (fmap f).
    Proof.
    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
    Qed.
    ......@@ -228,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 _|].