diff --git a/theories/base.v b/theories/base.v index c0733e1f8629d5a5bb9ddeaf22b5a8320cb79a0f..b229cba6bd0884bd5cfd379df236cd6f8c22e453 100644 --- a/theories/base.v +++ b/theories/base.v @@ -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. diff --git a/theories/bset.v b/theories/bset.v index 1c17ee660e15cf56fe6600088f18726395718c7c..f0b7a05037b75f08b6fc4462440d57c814b681eb 100644 --- a/theories/bset.v +++ b/theories/bset.v @@ -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. diff --git a/theories/coPset.v b/theories/coPset.v index 6110295d5b4a4c081643facae3c62d5592a6415c..ef6eb504ac31079a58e17c820ea3811e666230a5 100644 --- a/theories/coPset.v +++ b/theories/coPset.v @@ -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. diff --git a/theories/collections.v b/theories/collections.v index a650917f115b4f60e636b2a66dc136a469a5a29f..007e95e3c12aef028cfb22ca9a8f642fb893507a 100644 --- a/theories/collections.v +++ b/theories/collections.v @@ -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 : diff --git a/theories/fin_collections.v b/theories/fin_collections.v index c2e6487e7459e22a22cbd8e0aebca231415b4e14..a33efd6d09cc8bba3bda01d4471324c33b8c9854 100644 --- a/theories/fin_collections.v +++ b/theories/fin_collections.v @@ -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 → diff --git a/theories/fin_maps.v b/theories/fin_maps.v index 21bea1850194a2fbfbb8576abd889fb77ab14be8..121a13ffe16a94be11673bcd1fe488be45357ed8 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -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 _|]. intros m1 m2; rewrite !map_subseteq_spec. @@ -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. @@ -969,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. @@ -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 ↔ @@ -1600,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. @@ -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 : diff --git a/theories/gmultiset.v b/theories/gmultiset.v index a3ed60e826e0f1c6498993495c661c958bbdafcb..6d6e03565bce2a86de3523424ac8d562b77885f2 100644 --- a/theories/gmultiset.v +++ b/theories/gmultiset.v @@ -98,24 +98,24 @@ Proof. by split; auto with lia. - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega. Qed. -Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _). +Global Instance gmultiset_elem_of_dec : RelDecision (∈@{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. @@ -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. diff --git a/theories/infinite.v b/theories/infinite.v index 7b5c08f8c551b3ca75a68b92521958f0ee1846d1..81863ebc800f2a5214829dded22bab57e7b204f1 100644 --- a/theories/infinite.v +++ b/theories/infinite.v @@ -26,7 +26,7 @@ Qed. (** * Fresh elements *) Section Fresh. - Context `{FinCollection A C, Infinite A, !RelDecision (@elem_of A C _)}. + Context `{FinCollection A C, Infinite A, !RelDecision (∈@{C})}. Definition fresh_generic_body (s : C) (rec : ∀ s', s' ⊂ s → nat → A) (n : nat) : A := let cand := inject n in diff --git a/theories/list.v b/theories/list.v index ace7fc8382abfd72103af04b33c58a6a8550d972..3027ce81e6fd054d3d83dcf11e3ce366ff198d15 100644 --- a/theories/list.v +++ b/theories/list.v @@ -46,6 +46,10 @@ Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_s Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope. Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope. +Infix "≡ₚ@{ A }" := + (@Permutation A) (at level 70, no associativity, only parsing) : stdpp_scope. +Notation "(≡ₚ@{ A } )" := (@Permutation A) (only parsing) : stdpp_scope. + Instance maybe_cons {A} : Maybe2 (@cons A) := λ l, match l with x :: l => Some (x,l) | _ => None end. @@ -311,7 +315,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → Section list_set. Context `{dec : EqDecision A}. - Global Instance elem_of_list_dec : RelDecision (@elem_of A (list A) _). + Global Instance elem_of_list_dec : RelDecision (∈@{list A}). Proof. refine ( fix go x l := @@ -358,7 +362,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 +834,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 +887,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 +939,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 +1327,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. @@ -2115,7 +2119,7 @@ Section submseteq_dec. refine (λ l1 l2, cast_if (decide (is_Some (list_remove_list l1 l2)))); abstract (rewrite list_remove_list_submseteq; tauto). Defined. - Global Instance Permutation_dec : RelDecision (Permutation : relation (list A)). + Global Instance Permutation_dec : RelDecision (≡ₚ@{A}). Proof. refine (λ l1 l2, cast_if_and (decide (length l1 = length l2)) (decide (l1 ⊆+ l2))); @@ -2124,7 +2128,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. @@ -2826,7 +2830,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 +2840,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 A). + Global Instance tail_proper : Proper ((≡@{list A}) ==> (≡)) tail. Proof. destruct 1; try constructor; auto. Qed. - Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n). + Global Instance take_proper n : Proper ((≡@{list A}) ==> (≡)) (take n). Proof. induction n; destruct 1; constructor; auto. Qed. - Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n). + Global Instance drop_proper n : Proper ((≡@{list A}) ==> (≡)) (drop n). Proof. induction n; destruct 1; simpl; try constructor; auto. Qed. - Global Instance list_lookup_proper i : - Proper ((≡) ==> (≡)) (lookup (M:=list A) i). + Global Instance list_lookup_proper i : Proper ((≡@{list A}) ==> (≡)) (lookup i). Proof. induction i; destruct 1; simpl; try constructor; auto. Qed. Global Instance list_alter_proper f i : - Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i). + Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{list A})) (alter f i). Proof. intros. induction i; destruct 1; constructor; eauto. Qed. Global Instance list_insert_proper i : - Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i). + Proper ((≡) ==> (≡) ==> (≡@{list A})) (insert i). Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed. Global Instance list_inserts_proper i : - Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i). + Proper ((≡) ==> (≡) ==> (≡@{list A})) (list_inserts i). Proof. intros k1 k2 Hk; revert i. induction Hk; intros ????; simpl; try f_equiv; naive_solver. Qed. Global Instance list_delete_proper i : - Proper ((≡) ==> (≡)) (delete (M:=list A) i). + Proper ((≡) ==> (≡@{list A})) (delete i). Proof. induction i; destruct 1; try constructor; eauto. Qed. - Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A). + Global Instance option_list_proper : Proper ((≡) ==> (≡@{list A})) option_list. Proof. destruct 1; repeat constructor; auto. Qed. Global Instance list_filter_proper P `{∀ x, Decision (P x)} : - Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P). + Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡@{list A})) (filter P). Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed. - Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n). + Global Instance replicate_proper n : Proper ((≡@{A}) ==> (≡)) (replicate n). Proof. induction n; constructor; auto. Qed. - Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A). + Global Instance reverse_proper : Proper ((≡) ==> (≡@{list A})) reverse. Proof. induction 1; rewrite ?reverse_cons; simpl; [constructor|]. apply app_proper; repeat constructor; auto. Qed. Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A). Proof. induction 1 as [|????? []]; simpl; repeat constructor; auto. Qed. - Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡)) (@resize A n). + Global Instance resize_proper n : Proper ((≡) ==> (≡) ==> (≡@{list A})) (resize n). Proof. induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto. Qed. @@ -3111,8 +3114,7 @@ Section ret_join. Lemma list_join_bind (ls : list (list A)) : mjoin ls = ls ≫= id. Proof. by induction ls; f_equal/=. Qed. - Global Instance mjoin_Permutation: - Proper (@Permutation (list A) ==> (≡ₚ)) mjoin. + Global Instance mjoin_Permutation : Proper ((≡ₚ@{list A}) ==> (≡ₚ)) mjoin. Proof. intros ?? E. by rewrite !list_join_bind, E. Qed. Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y. Proof. apply elem_of_list_singleton. Qed. @@ -3646,7 +3648,7 @@ Ltac solve_length := simplify_eq/=; repeat (rewrite fmap_length || rewrite app_length); repeat match goal with - | H : @eq (list _) _ _ |- _ => apply (f_equal length) in H + | H : _ =@{list _} _ |- _ => apply (f_equal length) in H | H : Forall2 _ _ _ |- _ => apply Forall2_length in H | H : context[length (_ <$> _)] |- _ => rewrite fmap_length in H end; done || congruence. diff --git a/theories/mapset.v b/theories/mapset.v index 6e9f72cbc2c50ecc4e7bea1a79576ae700ce11a9..1143b152bc20fbf404b577242aa9efdb9d98164c 100644 --- a/theories/mapset.v +++ b/theories/mapset.v @@ -76,16 +76,16 @@ Section deciders. match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); abstract congruence. Defined. - Global Instance mapset_equiv_dec : RelDecision (@equiv (mapset M)_) | 1. + Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1. Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined. - Global Instance mapset_elem_of_dec : RelDecision (@elem_of _ (mapset M) _) | 1. + Global Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1. Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined. - Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _). + Global Instance mapset_disjoint_dec : RelDecision (##@{mapset M}). Proof. 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). diff --git a/theories/option.v b/theories/option.v index f539f4bfd26d6fac769f23c8c5f13aab02c62b92..fa3fbd61ea6e27ae8ec702dc873cfd972a9f368d 100644 --- a/theories/option.v +++ b/theories/option.v @@ -122,11 +122,11 @@ Section setoids. Proof. done. Qed. Global Instance option_equivalence : - Equivalence ((≡) : relation A) → Equivalence ((≡) : relation (option A)). + Equivalence (≡@{A}) → Equivalence (≡@{option A}). Proof. apply _. Qed. - Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A). + Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some. Proof. by constructor. Qed. - Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A). + Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some. Proof. by inversion_clear 1. Qed. Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A). Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed. @@ -141,11 +141,11 @@ Section setoids. Proof. destruct 1; naive_solver. Qed. Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'. Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed. - Lemma equiv_Some_inv_r' `{!Equivalence ((≡) : relation A)} mx y : + Lemma equiv_Some_inv_r' `{!Equivalence (≡@{A})} mx y : mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'. Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed. - Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A). + Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some. Proof. inversion_clear 1; split; eauto. Qed. Global Instance from_option_proper {B} (R : relation B) (f : A → B) : Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f). @@ -188,8 +188,7 @@ Lemma fmap_Some_1 {A B} (f : A → B) mx y : Proof. apply fmap_Some. Qed. Lemma fmap_Some_2 {A B} (f : A → B) mx x : mx = Some x → f <$> mx = Some (f x). Proof. intros. apply fmap_Some; eauto. Qed. -Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)} - (f : A → B) mx y : +Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y : f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x. Proof. destruct mx; simpl; split. @@ -198,8 +197,7 @@ Proof. - intros ?%symmetry%equiv_None. done. - intros (? & ? & ?). done. Qed. -Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)} - (f : A → B) mx y : +Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y : f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x. Proof. by rewrite fmap_Some_equiv. Qed. Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None. @@ -237,13 +235,13 @@ Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx. Proof. by destruct mx. Qed. Instance option_fmap_proper `{Equiv A, Equiv B} : - Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (fmap (M:=option) (A:=A) (B:=B)). + Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) fmap. Proof. destruct 2; constructor; auto. Qed. Instance option_mbind_proper `{Equiv A, Equiv B} : - Proper (((≡) ==> (≡)) ==> (≡) ==> (≡)) (mbind (M:=option) (A:=A) (B:=B)). + Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) mbind. Proof. destruct 2; simpl; try constructor; auto. Qed. Instance option_mjoin_proper `{Equiv A} : - Proper ((≡) ==> (≡)) (mjoin (M:=option) (A:=A)). + Proper ((≡) ==> (≡@{option (option A)})) mjoin. Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed. (** ** Inverses of constructors *) @@ -312,14 +310,14 @@ Section union_intersection_difference. Global Instance union_with_right_id : RightId (=) None (union_with f). Proof. by intros [?|]. Qed. Global Instance union_with_comm : - Comm (=) f → Comm (=) (union_with (M:=option A) f). + Comm (=) f → Comm (=@{option A}) (union_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f). Proof. by intros [?|]. Qed. Global Instance difference_with_comm : - Comm (=) f → Comm (=) (intersection_with (M:=option A) f). + Comm (=) f → Comm (=@{option A}) (intersection_with f). Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed. Global Instance difference_with_right_id : RightId (=) None (difference_with f). Proof. by intros [?|]. Qed. diff --git a/theories/pmap.v b/theories/pmap.v index 05c9b94c27ce36d01ba7329d592c52699bb1b886..0eba03ef9cbab4060cb01f01c1058a0459e8adf4 100644 --- a/theories/pmap.v +++ b/theories/pmap.v @@ -13,8 +13,8 @@ From stdpp Require Export fin_maps. Set Default Proof Using "Type". Local Open Scope positive_scope. -Local Hint Extern 0 (@eq positive _ _) => congruence. -Local Hint Extern 0 (¬@eq positive _ _) => congruence. +Local Hint Extern 0 (_ =@{positive} _) => congruence. +Local Hint Extern 0 (_ ≠@{positive} _) => congruence. (** * The tree data structure *) (** The data type [Pmap_raw] specifies radix-2 search trees. These trees do diff --git a/theories/pretty.v b/theories/pretty.v index a1e85a4642318e669e66fbdb09eff3ae80e7723c..a26e574b794112f9ba097590afb559625fb7ea27 100644 --- a/theories/pretty.v +++ b/theories/pretty.v @@ -40,7 +40,7 @@ Qed. Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string. Lemma pretty_N_unfold x : pretty x = pretty_N_go x "". Proof. done. Qed. -Instance pretty_N_inj : Inj (@eq N) (=) pretty. +Instance pretty_N_inj : Inj (=@{N}) (=) pretty. Proof. assert (∀ x y, x < 10 → y < 10 → pretty_N_char x = pretty_N_char y → x = y)%N. @@ -71,6 +71,6 @@ Instance pretty_Z : Pretty Z := λ x, | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x) end%string. Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x). -Instance pretty_nat_inj : Inj (@eq nat) (=) pretty. +Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty. Proof. apply _. Qed. diff --git a/theories/streams.v b/theories/streams.v index 747141eb94329c878bef1856ea3d211a0087c5c0..0a1be8b6ea16a4566382ee7edaea6d7961c4403d 100644 --- a/theories/streams.v +++ b/theories/streams.v @@ -38,7 +38,7 @@ Implicit Types s t : stream A. Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1 ≡ s2. Proof. by constructor. Qed. -Global Instance equal_equivalence : Equivalence (@equiv (stream A) _). +Global Instance equal_equivalence : Equivalence (≡@{stream A}). Proof. split. - now cofix; intros [??]; constructor. @@ -47,10 +47,10 @@ Proof. Qed. Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x). Proof. by constructor. Qed. -Global Instance shead_proper : Proper ((≡) ==> (=)) (@shead A). +Global Instance shead_proper : Proper ((≡) ==> (=@{A})) shead. Proof. by intros ?? [??]. Qed. -Global Instance stail_proper : Proper ((≡) ==> (≡)) (@stail A). +Global Instance stail_proper : Proper ((≡) ==> (≡@{stream A})) stail. Proof. by intros ?? [??]. Qed. -Global Instance slookup_proper : Proper ((≡) ==> eq) (@slookup A i). +Global Instance slookup_proper : Proper ((≡@{stream A}) ==> (=)) (slookup i). Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed. End stream_properties. diff --git a/theories/tactics.v b/theories/tactics.v index 849228769060084f48401cb9b77ef3eeb181635a..4b42a8f6f6fab451dabf069cf32632bdbe75e1b1 100644 --- a/theories/tactics.v +++ b/theories/tactics.v @@ -241,7 +241,7 @@ Tactic Notation "simplify_eq" := repeat assert (y = x) by congruence; clear H2 | H1 : ?o = Some ?x, H2 : ?o = None |- _ => congruence | H : @existT ?A _ _ _ = existT _ _ |- _ => - apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (@eq A))) in H + apply (Eqdep_dec.inj_pair2_eq_dec _ (decide_rel (=@{A}))) in H end. Tactic Notation "simplify_eq" "/=" := repeat (progress csimpl in * || simplify_eq).