Commit 6aba4a3f by Robbert Krebbers

Notations `=@{A}` and `≡@{A}` for being explicit about the type of (setoid) equality.

`This followed from discussions in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134`
parent 3bcaaf7e
 ... ... @@ -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. ... ...
 ... ... @@ -192,7 +192,7 @@ Qed. Instance coPset_elem_of_dec : RelDecision (@elem_of _ 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 _). Proof. ... ...
 ... ... @@ -19,14 +19,14 @@ 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. ... ... @@ -35,11 +35,11 @@ Section setoids_simple. 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 +50,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. ... ... @@ -357,15 +357,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 ≡ ∅. ... ... @@ -480,15 +480,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 +527,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 +580,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 +647,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). ... ... @@ -776,17 +776,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 +887,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 +1057,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 +1077,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 : ... ...
 ... ... @@ -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. ... ... @@ -921,13 +917,13 @@ Section map_of_to_collection. Proof. unfold map_to_collection; simpl. by rewrite map_to_list_empty. Qed. Lemma map_to_collection_insert (f : K → A → B)(m : M A) i x : m !! i = None → map_to_collection (C:=C) f (<[i:=x]>m) ≡ {[f i x]} ∪ map_to_collection f m. map_to_collection f (<[i:=x]>m) ≡@{C} {[f i x]} ∪ map_to_collection f m. Proof. intros. unfold map_to_collection; simpl. by rewrite map_to_list_insert. Qed. Lemma map_to_collection_insert_L `{!LeibnizEquiv C} (f : K → A → B) (m : M A) i x : m !! i = None → map_to_collection (C:=C) f (<[i:=x]>m) = {[f i x]} ∪ map_to_collection f m. map_to_collection f (<[i:=x]>m) =@{C} {[f i x]} ∪ map_to_collection f m. Proof. unfold_leibniz. apply map_to_collection_insert. Qed. End map_of_to_collection. ... ... @@ -1166,19 +1162,19 @@ Lemma merge_comm m1 m2 : (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → merge f m1 m2 = merge f m2 m1. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Global Instance merge_comm' : Comm (=) f → Comm (=) (merge (M:=M) f). Global Instance merge_comm' : Comm (=) f → Comm (=@{M _}) (merge f). Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed. Lemma merge_assoc m1 m2 m3 : (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = f (f (m1 !! i) (m2 !! i)) (m3 !! i)) → merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge (M:=M) f). Global Instance merge_assoc' : Assoc (=) f → Assoc (=@{M _}) (merge f). Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed. Lemma merge_idemp m1 : (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge (M:=M) f). Global Instance merge_idemp' : IdemP (=) f → IdemP (=@{M _}) (merge f). Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed. End merge. ... ... @@ -1433,9 +1429,9 @@ Proof. rewrite lookup_union_with. destruct (m1 !! i), (m2 !! i); compute; naive_solver. Qed. Global Instance: LeftId (@eq (M A)) ∅ (union_with f). Global Instance: LeftId (=@{M A}) ∅ (union_with f). Proof. unfold union_with, map_union_with. apply _. Qed. Global Instance: RightId (@eq (M A)) ∅ (union_with f). Global Instance: RightId (=@{M A}) ∅ (union_with f). Proof. unfold union_with, map_union_with. apply _. Qed. Lemma union_with_comm m1 m2 : (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) → ... ... @@ -1444,7 +1440,7 @@ Proof. intros. apply (merge_comm _). intros i. destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. Qed. Global Instance: Comm (=) f → Comm (@eq (M A)) (union_with f). Global Instance: Comm (=) f → Comm (=@{M A}) (union_with f). Proof. intros ???. apply union_with_comm. eauto. Qed. Lemma union_with_idemp m : (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m. ... ... @@ -1502,15 +1498,15 @@ Qed. End union_with. (** ** Properties of the [union] operation *) Global Instance: LeftId (@eq (M A)) ∅ (∪) := _. Global Instance: RightId (@eq (M A)) ∅ (∪) := _. Global Instance: Assoc (@eq (M A)) (∪). Global Instance: LeftId (=@{M A}) ∅ (∪) := _. Global Instance: RightId (=@{M A}) ∅ (∪) := _. Global Instance: Assoc (=@{M A}) (∪). Proof. intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with. apply (merge_assoc _). intros i. by destruct (m1 !! i), (m2 !! i), (m3 !! i). Qed. Global Instance: IdemP (@eq (M A)) (∪). Global Instance: IdemP (=@{M A}) (∪). Proof. intros A ?. by apply union_with_idemp. Qed. Lemma lookup_union_Some_raw {A} (m1 m2 : M A) i x : (m1 ∪ m2) !! i = Some x ↔ ... ... @@ -1766,9 +1762,9 @@ Proof. intro. by rewrite map_disjoint_of_list_zip_r. Qed. Section intersection_with. Context {A} (f : A → A → option A). Implicit Type (m: M A). Global Instance : LeftAbsorb (@eq (M A)) ∅ (intersection_with f). Global Instance : LeftAbsorb (=@{M A}) ∅ (intersection_with f). Proof. unfold intersection_with, map_intersection_with. apply _. Qed. Global Instance: RightAbsorb (@eq (M A)) ∅ (intersection_with f). Global Instance: RightAbsorb (=@{M A}) ∅ (intersection_with f). Proof. unfold intersection_with, map_intersection_with. apply _. Qed. Lemma lookup_intersection_with m1 m2 i : intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i). ... ... @@ -1787,7 +1783,7 @@ Proof. intros. apply (merge_comm _). intros i. destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto. Qed. Global Instance: Comm (=) f → Comm (@eq (M A)) (intersection_with f). Global Instance: Comm (=) f → Comm (=@{M A}) (intersection_with f). Proof. intros ???. apply intersection_with_comm. eauto. Qed. Lemma intersection_with_idemp m : (∀ i x, m !! i = Some x → f x x = Some x) → intersection_with f m m = m. ... ... @@ -1817,16 +1813,16 @@ Proof. by intros; apply (partial_alter_merge _). Qed. End intersection_with. (** ** Properties of the [intersection] operation *) Global Instance: LeftAbsorb (@eq (M A)) ∅ (∩) := _. Global Instance: RightAbsorb (@eq (M A)) ∅ (∩) := _. Global Instance: Assoc (@eq (M A)) (∩). Global Instance: LeftAbsorb (=@{M A}) ∅ (∩) := _. Global Instance: RightAbsorb (=@{M A}) ∅ (∩) := _. Global Instance: Assoc (=@{M A}) (∩). Proof. intros A m1 m2 m3. unfold intersection, map_intersection, intersection_with, map_intersection_with. apply (merge_assoc _). intros i. by destruct (m1 !! i), (m2 !! i), (m3 !! i). Qed. Global Instance: IdemP (@eq (M A)) (∩). Global Instance: IdemP (=@{M A}) (∩). Proof. intros A ?. by apply intersection_with_idemp. Qed. Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x : ... ...
 ... ... @@ -102,20 +102,20 @@ Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _) Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined. (* Algebraic laws *) Global Instance gmultiset_comm : Comm (@eq (gmultiset A)) (∪). Global Instance gmultiset_comm : Comm (=@{gmultiset A}) (∪). Proof. intros X Y. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. Qed. Global Instance gmultiset_assoc : Assoc (@eq (gmultiset A)) (∪). Global Instance gmultiset_assoc : Assoc (=@{gmultiset A}) (∪). Proof. intros X Y Z. apply gmultiset_eq; intros x. rewrite !multiplicity_union; omega. Qed. Global Instance gmultiset_left_id : LeftId (@eq (gmultiset A)) ∅ (∪). Global Instance gmultiset_left_id : LeftId (=@{gmultiset A}) ∅ (∪). Proof. intros X. apply gmultiset_eq; intros x. by rewrite multiplicity_union, multiplicity_empty. Qed. Global Instance gmultiset_right_id : RightId (@eq (gmultiset A)) ∅ (∪). Global Instance gmultiset_right_id : RightId (=@{gmultiset A}) ∅ (∪). Proof. intros X. by rewrite (comm_L (∪)), (left_id_L _ _). Qed. Global Instance gmultiset_union_inj_1 X : Inj (=) (=) (X ∪). ... ... @@ -126,7 +126,7 @@ Qed. Global Instance gmultiset_union_inj_2 X : Inj (=) (=) (∪ X). Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed. Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠ (∅ : gmultiset A). Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅. Proof. rewrite gmultiset_eq. intros Hx; generalize (Hx x). by rewrite multiplicity_singleton, multiplicity_empty. ... ...
 ... ... @@ -358,7 +358,7 @@ Tactic Notation "discriminate_list" hyp(H) := apply (f_equal length) in H; repeat (csimpl in H || rewrite app_length in H); exfalso; lia. Tactic Notation "discriminate_list" := match goal with H : @eq (list _) _ _ |- _ => discriminate_list H end. match goal with H : _ =@{list _} _ |- _ => discriminate_list H end. (** The tactic [simplify_list_eq] simplifies hypotheses involving equalities on lists using injectivity of [(::)] and [(++)]. Also, it simplifies ... ... @@ -830,7 +830,7 @@ Section find. End find. (** ** Properties of the [reverse] function *) Lemma reverse_nil : reverse [] = @nil A. Lemma reverse_nil : reverse [] =@{list A} []. Proof. done. Qed. Lemma reverse_singleton x : reverse [x] = [x]. Proof. done. Qed. ... ... @@ -883,7 +883,7 @@ Lemma take_drop_middle l i x : Proof. revert i x. induction l; intros [|?] ??; simplify_eq/=; f_equal; auto. Qed. Lemma take_nil n : take n (@nil A) = []. Lemma take_nil n : take n [] =@{list A} []. Proof. by destruct n. Qed. Lemma take_app l k : take (length l) (l ++ k) = l. Proof. induction l; f_equal/=; auto. Qed. ... ... @@ -935,7 +935,7 @@ Qed. (** ** Properties of the [drop] function *) Lemma drop_0 l : drop 0 l = l. Proof. done. Qed. Lemma drop_nil n : drop n (@nil A) = []. Lemma drop_nil n : drop n [] =@{list A} []. Proof. by destruct n. Qed. Lemma drop_length l n : length (drop n l) = length l - n. Proof. revert n. by induction l; intros [|i]; f_equal/=. Qed. ... ... @@ -1323,7 +1323,7 @@ Proof. Qed. (** ** Properties of the [mask] function *) Lemma mask_nil f βs : mask f βs (@nil A) = []. Lemma mask_nil f βs : mask f βs [] =@{list A} []. Proof. by destruct βs. Qed. Lemma mask_length f βs l : length (mask f βs l) = length l. Proof. revert βs. induction l; intros [|??]; f_equal/=; auto. Qed. ... ... @@ -2826,7 +2826,7 @@ Section setoid. Qed. Global Instance list_equivalence : Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (list A)). Equivalence (≡@{A}) → Equivalence (≡@{list A}). Proof. split. - intros l. by apply equiv_Forall2. ... ... @@ -2836,51 +2836,50 @@ Section setoid. Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A). Proof. induction 1; f_equal; fold_leibniz; auto. Qed. Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A). Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) cons. Proof. by constructor. Qed. Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A). Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡@{list A})) app. Proof. induction 1; intros ???; simpl; try constructor; auto. Qed. Global Instance length_proper : Proper ((≡) ==> (=)) (@length A). Global Instance length_proper : Proper ((≡@{list A}) ==> (=)) length. Proof. induction 1; f_equal/=; auto. Qed. Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail