diff --git a/tests/telescopes.v b/tests/telescopes.v
index ede324c066e674a4f04c01e4e686deb49f73d954..56633586fa2e6089fa9e591c61b2a8f505e48c4f 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -30,3 +30,4 @@ Proof.
left. done.
Qed.
End tests.
+End accessor.
diff --git a/theories/base.v b/theories/base.v
index c1fa499aabd67cfbc18e34f346daad88ef06f511..812635a402860f8b6203a0c547a8242324e3cd45 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -54,8 +54,8 @@ Section seal.
Local Set Primitive Projections.
Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
End seal.
-Arguments unseal {_ _} _ : assert.
-Arguments seal_eq {_ _} _ : assert.
+Global Arguments unseal {_ _} _ : assert.
+Global Arguments seal_eq {_ _} _ : assert.
(** * Non-backtracking type classes *)
(** The type class [TCNoBackTrack P] can be used to establish [P] without ever
@@ -92,7 +92,7 @@ Global Hint Extern 0 (TCIf _ _ _) =>
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque.
-Arguments tc_opaque {_} _ /.
+Global Arguments tc_opaque {_} _ /.
(** Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the
@@ -282,7 +282,7 @@ Instance: Params (@equiv) 2 := {}.
(** The following instance forces [setoid_replace] to use setoid equality
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
-Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3 := {}.
+Global Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3 := {}.
Global Hint Extern 0 (_ ≡ _) => reflexivity : core.
Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
@@ -293,7 +293,7 @@ Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
propositions. *)
Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Hint Mode Decision ! : typeclass_instances.
-Arguments decide _ {_} : simpl never, assert.
+Global Arguments decide _ {_} : simpl never, assert.
(** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
an explicit class instead of a notation for two reasons:
@@ -312,14 +312,14 @@ an explicit class instead of a notation for two reasons:
Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :> Decision (R x y).
Global Hint Mode RelDecision ! ! ! : typeclass_instances.
-Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
+Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
Notation EqDecision A := (RelDecision (=@{A})).
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Global Hint Mode Inhabited ! : typeclass_instances.
-Arguments populate {_} _ : assert.
+Global Arguments populate {_} _ : assert.
(** ** Proof irrelevant types *)
(** This type class collects types that are proof irrelevant. That means, all
@@ -368,22 +368,22 @@ Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x :
R (f (f x)) x.
Proof. auto. Qed.
-Arguments irreflexivity {_} _ {_} _ _ : assert.
-Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
-Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
-Arguments cancel {_ _ _} _ _ {_} _ : assert.
-Arguments surj {_ _ _} _ {_} _ : assert.
-Arguments idemp {_ _} _ {_} _ : assert.
-Arguments comm {_ _ _} _ {_} _ _ : assert.
-Arguments left_id {_ _} _ _ {_} _ : assert.
-Arguments right_id {_ _} _ _ {_} _ : assert.
-Arguments assoc {_ _} _ {_} _ _ _ : assert.
-Arguments left_absorb {_ _} _ _ {_} _ : assert.
-Arguments right_absorb {_ _} _ _ {_} _ : assert.
-Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
-Arguments total {_} _ {_} _ _ : assert.
-Arguments trichotomy {_} _ {_} _ _ : assert.
-Arguments trichotomyT {_} _ {_} _ _ : assert.
+Global Arguments irreflexivity {_} _ {_} _ _ : assert.
+Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
+Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
+Global Arguments cancel {_ _ _} _ _ {_} _ : assert.
+Global Arguments surj {_ _ _} _ {_} _ : assert.
+Global Arguments idemp {_ _} _ {_} _ : assert.
+Global Arguments comm {_ _ _} _ {_} _ _ : assert.
+Global Arguments left_id {_ _} _ _ {_} _ : assert.
+Global Arguments right_id {_ _} _ _ {_} _ : assert.
+Global Arguments assoc {_ _} _ {_} _ _ _ : assert.
+Global Arguments left_absorb {_ _} _ _ {_} _ : assert.
+Global Arguments right_absorb {_ _} _ _ {_} _ : assert.
+Global Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
+Global Arguments total {_} _ {_} _ _ : assert.
+Global Arguments trichotomy {_} _ {_} _ _ : assert.
+Global Arguments trichotomyT {_} _ {_} _ _ : assert.
Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
Proof. intuition. Qed.
@@ -402,9 +402,9 @@ Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B)
`{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
Proof. firstorder. Qed.
-Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
+Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
-Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
+Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} :
@@ -448,7 +448,7 @@ Class TotalOrder {A} (R : relation A) : Prop := {
}.
(** * Logic *)
-Instance prop_inhabited : Inhabited Prop := populate True.
+Global Instance prop_inhabited : Inhabited Prop := populate True.
Notation "(∧)" := and (only parsing) : stdpp_scope.
Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
@@ -482,43 +482,43 @@ Lemma exist_proper {A} (P Q : A → Prop) :
(∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
Proof. firstorder. Qed.
-Instance eq_comm {A} : Comm (↔) (=@{A}).
+Global Instance eq_comm {A} : Comm (↔) (=@{A}).
Proof. red; intuition. Qed.
-Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x).
+Global Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x).
Proof. red; intuition. Qed.
-Instance iff_comm : Comm (↔) (↔).
+Global Instance iff_comm : Comm (↔) (↔).
Proof. red; intuition. Qed.
-Instance and_comm : Comm (↔) (∧).
+Global Instance and_comm : Comm (↔) (∧).
Proof. red; intuition. Qed.
-Instance and_assoc : Assoc (↔) (∧).
+Global Instance and_assoc : Assoc (↔) (∧).
Proof. red; intuition. Qed.
-Instance and_idemp : IdemP (↔) (∧).
+Global Instance and_idemp : IdemP (↔) (∧).
Proof. red; intuition. Qed.
-Instance or_comm : Comm (↔) (∨).
+Global Instance or_comm : Comm (↔) (∨).
Proof. red; intuition. Qed.
-Instance or_assoc : Assoc (↔) (∨).
+Global Instance or_assoc : Assoc (↔) (∨).
Proof. red; intuition. Qed.
-Instance or_idemp : IdemP (↔) (∨).
+Global Instance or_idemp : IdemP (↔) (∨).
Proof. red; intuition. Qed.
-Instance True_and : LeftId (↔) True (∧).
+Global Instance True_and : LeftId (↔) True (∧).
Proof. red; intuition. Qed.
-Instance and_True : RightId (↔) True (∧).
+Global Instance and_True : RightId (↔) True (∧).
Proof. red; intuition. Qed.
-Instance False_and : LeftAbsorb (↔) False (∧).
+Global Instance False_and : LeftAbsorb (↔) False (∧).
Proof. red; intuition. Qed.
-Instance and_False : RightAbsorb (↔) False (∧).
+Global Instance and_False : RightAbsorb (↔) False (∧).
Proof. red; intuition. Qed.
-Instance False_or : LeftId (↔) False (∨).
+Global Instance False_or : LeftId (↔) False (∨).
Proof. red; intuition. Qed.
-Instance or_False : RightId (↔) False (∨).
+Global Instance or_False : RightId (↔) False (∨).
Proof. red; intuition. Qed.
-Instance True_or : LeftAbsorb (↔) True (∨).
+Global Instance True_or : LeftAbsorb (↔) True (∨).
Proof. red; intuition. Qed.
-Instance or_True : RightAbsorb (↔) True (∨).
+Global Instance or_True : RightAbsorb (↔) True (∨).
Proof. red; intuition. Qed.
-Instance True_impl : LeftId (↔) True impl.
+Global Instance True_impl : LeftId (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
-Instance impl_True : RightAbsorb (↔) True impl.
+Global Instance impl_True : RightAbsorb (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
@@ -538,54 +538,54 @@ Notation "(∘)" := compose (only parsing) : stdpp_scope.
Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
-Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
+Global Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
populate (λ _, inhabitant).
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
-Arguments id _ _ / : assert.
-Arguments compose _ _ _ _ _ _ / : assert.
-Arguments flip _ _ _ _ _ _ / : assert.
-Arguments const _ _ _ _ / : assert.
+Global Arguments id _ _ / : assert.
+Global Arguments compose _ _ _ _ _ _ / : assert.
+Global Arguments flip _ _ _ _ _ _ / : assert.
+Global Arguments const _ _ _ _ / : assert.
Typeclasses Transparent id compose flip const.
Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
g ∘ h ∘ f.
-Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
+Global Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
Reflexive R2 → Proper (R1 ==> R2) (λ _, x).
Proof. intros ? y1 y2; reflexivity. Qed.
-Instance id_inj {A} : Inj (=) (=) (@id A).
+Global Instance id_inj {A} : Inj (=) (=) (@id A).
Proof. intros ??; auto. Qed.
-Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
+Global Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f).
Proof. red; intuition. Qed.
-Instance id_surj {A} : Surj (=) (@id A).
+Global Instance id_surj {A} : Surj (=) (@id A).
Proof. intros y; exists y; reflexivity. Qed.
-Instance compose_surj {A B C} R (f : A → B) (g : B → C) :
+Global Instance compose_surj {A B C} R (f : A → B) (g : B → C) :
Surj (=) f → Surj R g → Surj R (g ∘ f).
Proof.
intros ?? x. unfold compose. destruct (surj g x) as [y ?].
destruct (surj f y) as [z ?]. exists z. congruence.
Qed.
-Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
+Global Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
Proof. intros ?; reflexivity. Qed.
-Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
+Global Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
Proof. intros ???; reflexivity. Qed.
-Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
+Global Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
Proof. intros ???; reflexivity. Qed.
-Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
+Global Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
Proof. intros ???; reflexivity. Qed.
-Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
+Global Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
Proof. intros ?; reflexivity. Qed.
-Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
+Global Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
Proof. intros ?; reflexivity. Qed.
(** ** Lists *)
-Instance list_inhabited {A} : Inhabited (list A) := populate [].
+Global Instance list_inhabited {A} : Inhabited (list A) := populate [].
Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
fix go l1 l2 :=
@@ -603,7 +603,7 @@ Notation "(||)" := orb (only parsing).
Infix "&&*" := (zip_with (&&)) (at level 40).
Infix "||*" := (zip_with (||)) (at level 50).
-Instance bool_inhabated : Inhabited bool := populate true.
+Global Instance bool_inhabated : Inhabited bool := populate true.
Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
Infix "=.>" := bool_le (at level 70).
@@ -621,18 +621,18 @@ Lemma Is_true_false (b : bool) : b = false → ¬b.
Proof. now intros -> ?. Qed.
(** ** Unit *)
-Instance unit_equiv : Equiv unit := λ _ _, True.
-Instance unit_equivalence : Equivalence (≡@{unit}).
+Global Instance unit_equiv : Equiv unit := λ _ _, True.
+Global Instance unit_equivalence : Equivalence (≡@{unit}).
Proof. repeat split. Qed.
-Instance unit_leibniz : LeibnizEquiv unit.
+Global Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
-Instance unit_inhabited: Inhabited unit := populate ().
+Global Instance unit_inhabited: Inhabited unit := populate ().
(** ** Empty *)
-Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
-Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
+Global Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
+Global Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
Proof. repeat split. Qed.
-Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
+Global Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Proof. intros [] []; reflexivity. Qed.
(** ** Products *)
@@ -660,19 +660,19 @@ Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
(f (p.1), g (p.2)).
-Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
+Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'')
(p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)).
-Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
+Global Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
-Instance prod_inhabited {A B} (iA : Inhabited A)
+Global Instance prod_inhabited {A B} (iA : Inhabited A)
(iB : Inhabited B) : Inhabited (A * B) :=
match iA, iB with populate x, populate y => populate (x,y) end.
-Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
+Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
Proof. injection 1; auto. Qed.
-Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
+Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g).
Proof.
intros ?? [??] [??] ?; simpl in *; f_equal;
@@ -706,33 +706,33 @@ Section prod_relation.
Proof. firstorder eauto. Qed.
End prod_relation.
-Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Instance pair_proper `{Equiv A, Equiv B} :
+Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
+Global Instance pair_proper `{Equiv A, Equiv B} :
Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
-Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
-Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
-Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
+Global Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
+Global Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
+Global Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
Typeclasses Opaque prod_equiv.
-Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
+Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
(** ** Sums *)
Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' :=
match xy with inl x => inl (f x) | inr y => inr (g y) end.
-Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
+Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
-Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
+Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
match iA with populate x => populate (inl x) end.
-Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
+Global Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
match iB with populate y => populate (inl y) end.
-Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
+Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
Proof. injection 1; auto. Qed.
-Instance inr_inj {A B} : Inj (=) (=) (@inr A B).
+Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B).
Proof. injection 1; auto. Qed.
-Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
+Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g).
Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed.
@@ -765,24 +765,24 @@ Section sum_relation.
Proof. inversion_clear 1; auto. Qed.
End sum_relation.
-Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
-Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
-Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
-Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
-Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
+Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
+Global Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
+Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
+Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
+Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
Typeclasses Opaque sum_equiv.
(** ** Option *)
-Instance option_inhabited {A} : Inhabited (option A) := populate None.
+Global Instance option_inhabited {A} : Inhabited (option A) := populate None.
(** ** Sigma types *)
-Arguments existT {_ _} _ _ : assert.
-Arguments projT1 {_ _} _ : assert.
-Arguments projT2 {_ _} _ : assert.
+Global Arguments existT {_ _} _ _ : assert.
+Global Arguments projT1 {_ _} _ : assert.
+Global Arguments projT2 {_ _} _ : assert.
-Arguments exist {_} _ _ _ : assert.
-Arguments proj1_sig {_ _} _ : assert.
-Arguments proj2_sig {_ _} _ : assert.
+Global Arguments exist {_} _ _ _ : assert.
+Global Arguments proj1_sig {_ _} _ : assert.
+Global Arguments proj2_sig {_ _} _ : assert.
Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
@@ -800,7 +800,7 @@ Section sig_map.
apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
Qed.
End sig_map.
-Arguments sig_map _ _ _ _ _ _ !_ / : assert.
+Global Arguments sig_map _ _ _ _ _ _ !_ / : assert.
Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P :=
let '(ex_intro _ x _) := p in x.
@@ -816,7 +816,7 @@ Class Empty A := empty: A.
Global Hint Mode Empty ! : typeclass_instances.
Notation "∅" := empty (format "∅") : stdpp_scope.
-Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
Class Union A := union: A → A → A.
Global Hint Mode Union ! : typeclass_instances.
@@ -829,7 +829,7 @@ Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope
Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
-Arguments union_list _ _ _ !_ / : assert.
+Global Arguments union_list _ _ _ !_ / : assert.
Notation "⋃ l" := (union_list l) (at level 20, format "⋃ l") : stdpp_scope.
Class DisjUnion A := disj_union: A → A → A.
@@ -969,19 +969,19 @@ and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
-Arguments mret {_ _ _} _ : assert.
+Global Arguments mret {_ _ _} _ : assert.
Instance: Params (@mret) 3 := {}.
Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
-Arguments mbind {_ _ _ _} _ !_ / : assert.
+Global Arguments mbind {_ _ _ _} _ !_ / : assert.
Instance: Params (@mbind) 4 := {}.
Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
-Arguments mjoin {_ _ _} !_ / : assert.
+Global Arguments mjoin {_ _ _} !_ / : assert.
Instance: Params (@mjoin) 3 := {}.
Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
-Arguments fmap {_ _ _ _} _ !_ / : assert.
+Global Arguments fmap {_ _ _ _} _ !_ / : assert.
Instance: Params (@fmap) 4 := {}.
Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
-Arguments omap {_ _ _ _} _ !_ / : assert.
+Global Arguments omap {_ _ _ _} _ !_ / : assert.
Instance: Params (@omap) 4 := {}.
Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
@@ -1007,7 +1007,7 @@ Notation "ps .*2" := (fmap (M:=list) snd ps)
Class MGuard (M : Type → Type) :=
mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
-Arguments mguard _ _ _ !_ _ _ / : assert.
+Global Arguments mguard _ _ _ !_ _ _ / : assert.
Notation "'guard' P ; z" := (mguard P (λ _, z))
(at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
@@ -1024,7 +1024,7 @@ Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
Notation "(!!)" := lookup (only parsing) : stdpp_scope.
Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
-Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [lookup_total] should be the total over-approximation
of the partial [lookup] function. *)
@@ -1035,7 +1035,7 @@ Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope.
-Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The singleton map *)
Class SingletonM K A M := singletonM: K → A → M.
@@ -1050,7 +1050,7 @@ Global Hint Mode Insert - - ! : typeclass_instances.
Instance: Params (@insert) 5 := {}.
Notation "<[ k := a ]>" := (insert k a)
(at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
-Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
+Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
(** The function delete [delete k m] should delete the value at key [k] in
[m]. If the key [k] is not a member of [m], the original map should be
@@ -1058,14 +1058,14 @@ returned. *)
Class Delete (K M : Type) := delete: K → M → M.
Global Hint Mode Delete - ! : typeclass_instances.
Instance: Params (@delete) 4 := {}.
-Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [alter f k m] should update the value at key [k] using the
function [f], which is called with the original value. *)
Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
Global Hint Mode Alter - - ! : typeclass_instances.
Instance: Params (@alter) 5 := {}.
-Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
(** The function [partial_alter f k m] should update the value at key [k] using the
function [f], which is called with the original value at key [k] or [None]
@@ -1075,15 +1075,15 @@ Class PartialAlter (K A M : Type) :=
partial_alter: (option A → option A) → K → M → M.
Global Hint Mode PartialAlter - - ! : typeclass_instances.
Instance: Params (@partial_alter) 4 := {}.
-Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [dom C m] should yield the domain of [m]. That is a finite
set of type [C] that contains the keys that are a member of [m]. *)
Class Dom (M C : Type) := dom: M → C.
Global Hint Mode Dom ! ! : typeclass_instances.
Instance: Params (@dom) 3 := {}.
-Arguments dom : clear implicits.
-Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
+Global Arguments dom : clear implicits.
+Global Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
@@ -1091,7 +1091,7 @@ Class Merge (M : Type → Type) :=
merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
Global Hint Mode Merge ! : typeclass_instances.
Instance: Params (@merge) 4 := {}.
-Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
and [m2] using the function [f] to combine values of members that are in
@@ -1100,24 +1100,24 @@ Class UnionWith (A M : Type) :=
union_with: (A → A → option A) → M → M → M.
Global Hint Mode UnionWith - ! : typeclass_instances.
Instance: Params (@union_with) 3 := {}.
-Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
(** Similarly for intersection and difference. *)
Class IntersectionWith (A M : Type) :=
intersection_with: (A → A → option A) → M → M → M.
Global Hint Mode IntersectionWith - ! : typeclass_instances.
Instance: Params (@intersection_with) 3 := {}.
-Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
Class DifferenceWith (A M : Type) :=
difference_with: (A → A → option A) → M → M → M.
Global Hint Mode DifferenceWith - ! : typeclass_instances.
Instance: Params (@difference_with) 3 := {}.
-Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
Definition intersection_with_list `{IntersectionWith A M}
(f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
-Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
+Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
(** * Notations for lattices. *)
(** SqSubsetEq registers the "canonical" partial order for a type, and is used
@@ -1133,7 +1133,7 @@ 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 (⊑@{A}) := {}.
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
@@ -1232,7 +1232,7 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
}.
Class Size C := size: C → nat.
Global Hint Mode Size ! : typeclass_instances.
-Arguments size {_ _} !_ / : simpl nomatch, assert.
+Global Arguments size {_ _} !_ / : simpl nomatch, assert.
Instance: Params (@size) 2 := {}.
(** The class [MonadSet M] axiomatizes a type constructor [M] that can be
@@ -1274,14 +1274,14 @@ Instead of instantiating [Infinite] directly, consider using [max_infinite] or
Class Fresh A C := fresh: C → A.
Global Hint Mode Fresh - ! : typeclass_instances.
Instance: Params (@fresh) 3 := {}.
-Arguments fresh : simpl never.
+Global Arguments fresh : simpl never.
Class Infinite A := {
infinite_fresh :> Fresh A (list A);
infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
}.
-Arguments infinite_fresh : simpl never.
+Global Arguments infinite_fresh : simpl never.
(** * Miscellaneous *)
Class Half A := half: A → A.
diff --git a/theories/binders.v b/theories/binders.v
index b2d2f4f942e3144f0eb49e615294535dbd0e901f..0f0744c66d07f08df8da85a343ca2f12884849fa 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -19,10 +19,10 @@ Inductive binder := BAnon | BNamed :> string → binder.
Bind Scope binder_scope with binder.
Notation "<>" := BAnon : binder_scope.
-Instance binder_dec_eq : EqDecision binder.
+Global Instance binder_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
-Instance binder_inhabited : Inhabited binder := populate BAnon.
-Instance binder_countable : Countable binder.
+Global Instance binder_inhabited : Inhabited binder := populate BAnon.
+Global Instance binder_countable : Countable binder.
Proof.
refine (inj_countable'
(λ b, match b with BAnon => None | BNamed s => Some s end)
@@ -40,13 +40,13 @@ Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
Infix "+b+" := app_binder (at level 60, right associativity).
-Instance set_unfold_cons_binder s b ss P :
+Global Instance set_unfold_cons_binder s b ss P :
SetUnfoldElemOf s ss P → SetUnfoldElemOf s (b :b: ss) (BNamed s = b ∨ P).
Proof.
constructor. rewrite <-(set_unfold (s ∈ ss) P).
destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
Qed.
-Instance set_unfold_app_binder s bs ss P Q :
+Global Instance set_unfold_app_binder s bs ss P Q :
SetUnfoldElemOf (BNamed s) bs P → SetUnfoldElemOf s ss Q →
SetUnfoldElemOf s (bs +b+ ss) (P ∨ Q).
Proof.
@@ -62,10 +62,10 @@ Proof. induction ss1; by f_equal/=. Qed.
Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
Proof. induction bs; by f_equal/=. Qed.
-Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
+Global Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
-Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Global Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
Proof.
assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
{ intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
diff --git a/theories/boolset.v b/theories/boolset.v
index 8ffe38973ebad67ccd24de4b4642dda9462300d7..7cddb6afa3c5f7f323cfe574917bb37f67454867 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -3,21 +3,21 @@ From stdpp Require Export prelude.
From stdpp Require Import options.
Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
-Arguments BoolSet {_} _ : assert.
-Arguments boolset_car {_} _ _ : assert.
+Global Arguments BoolSet {_} _ : assert.
+Global Arguments boolset_car {_} _ _ : assert.
-Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
-Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
-Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+Global Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
+Global Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
+Global Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
BoolSet (λ y, bool_decide (y = x)).
-Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
-Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+Global Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
+Global Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
-Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
-Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
-Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
+Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
Proof.
split; [split; [split| |]|].
- by intros x ?.
@@ -28,7 +28,7 @@ Proof.
destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
- done.
Qed.
-Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
Typeclasses Opaque boolset_elem_of.
diff --git a/theories/coGset.v b/theories/coGset.v
index 51cb1c52ccfff1855a5e49f8ea26e73a9dc80fd4..ccd5140492359477aaa9e2fb253e62349ce91263 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -14,11 +14,11 @@ Set Default Proof Using "Type*".
Inductive coGset `{Countable A} :=
| FinGSet (X : gset A)
| CoFinGset (X : gset A).
-Arguments coGset _ {_ _} : assert.
+Global Arguments coGset _ {_ _} : assert.
-Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
+Global Instance coGset_eq_dec `{Countable A} : EqDecision (coGset A).
Proof. solve_decision. Defined.
-Instance coGset_countable `{Countable A} : Countable (coGset A).
+Global Instance coGset_countable `{Countable A} : Countable (coGset A).
Proof.
apply (inj_countable'
(λ X, match X with FinGSet X => inl X | CoFinGset X => inr X end)
@@ -80,7 +80,7 @@ Section coGset.
Qed.
End coGset.
-Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
+Global Instance coGset_elem_of_dec `{Countable A} : RelDecision (∈@{coGset A}) :=
λ x X,
match X with
| FinGSet X => decide_rel elem_of x X
@@ -193,9 +193,9 @@ Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
Proof. destruct X; set_solver. Qed.
(** * Domain of finite maps *)
-Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
+Global Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
gset_to_coGset (dom _ m).
-Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
+Global Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
Proof.
split; try apply _. intros B m i. unfold dom, coGset_dom.
by rewrite elem_of_gset_to_coGset, elem_of_dom.
diff --git a/theories/coPset.v b/theories/coPset.v
index b418dd8cd7f8918eb7a0b1475dbf4140622ba849..d17d7f6b02c8e605593cd1dec4a4f1e80079db57 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -18,7 +18,7 @@ Local Open Scope positive_scope.
Inductive coPset_raw :=
| coPLeaf : bool → coPset_raw
| coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
-Instance coPset_raw_eq_dec : EqDecision coPset_raw.
+Global Instance coPset_raw_eq_dec : EqDecision coPset_raw.
Proof. solve_decision. Defined.
Fixpoint coPset_wf (t : coPset_raw) : bool :=
@@ -28,7 +28,7 @@ Fixpoint coPset_wf (t : coPset_raw) : bool :=
| coPNode false (coPLeaf false) (coPLeaf false) => false
| coPNode _ l r => coPset_wf l && coPset_wf r
end.
-Arguments coPset_wf !_ / : simpl nomatch, assert.
+Global Arguments coPset_wf !_ / : simpl nomatch, assert.
Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
@@ -42,7 +42,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
| false, coPLeaf false, coPLeaf false => coPLeaf false
| _, _, _ => coPNode b l r
end.
-Arguments coPNode' : simpl never.
+Global Arguments coPNode' : simpl never.
Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
Global Hint Resolve coPNode_wf : core.
@@ -55,7 +55,7 @@ Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
| coPNode _ _ r, p~1 => coPset_elem_of_raw p r
end.
Local Notation e_of := coPset_elem_of_raw.
-Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
+Global Arguments coPset_elem_of_raw _ !_ / : simpl nomatch, assert.
Lemma coPset_elem_of_node b l r p :
e_of p (coPNode' b l r) = e_of p (coPNode b l r).
Proof. by destruct p, b, l as [[]|], r as [[]|]. Qed.
@@ -87,7 +87,7 @@ Fixpoint coPset_singleton_raw (p : positive) : coPset_raw :=
| p~0 => coPNode' false (coPset_singleton_raw p) (coPLeaf false)
| p~1 => coPNode' false (coPLeaf false) (coPset_singleton_raw p)
end.
-Instance coPset_union_raw : Union coPset_raw :=
+Global Instance coPset_union_raw : Union coPset_raw :=
fix go t1 t2 := let _ : Union _ := @go in
match t1, t2 with
| coPLeaf false, coPLeaf false => coPLeaf false
@@ -98,7 +98,7 @@ Instance coPset_union_raw : Union coPset_raw :=
| coPNode b1 l1 r1, coPNode b2 l2 r2 => coPNode' (b1||b2) (l1 ∪ l2) (r1 ∪ r2)
end.
Local Arguments union _ _!_ !_ / : assert.
-Instance coPset_intersection_raw : Intersection coPset_raw :=
+Global Instance coPset_intersection_raw : Intersection coPset_raw :=
fix go t1 t2 := let _ : Intersection _ := @go in
match t1, t2 with
| coPLeaf true, coPLeaf true => coPLeaf true
@@ -152,22 +152,22 @@ Qed.
(** * Packed together + set operations *)
Definition coPset := { t | coPset_wf t }.
-Instance coPset_singleton : Singleton positive coPset := λ p,
+Global Instance coPset_singleton : Singleton positive coPset := λ p,
coPset_singleton_raw p ↾ coPset_singleton_wf _.
-Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
-Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
-Instance coPset_top : Top coPset := coPLeaf true ↾ I.
-Instance coPset_union : Union coPset := λ X Y,
+Global Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
+Global Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
+Global Instance coPset_top : Top coPset := coPLeaf true ↾ I.
+Global Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∪ t2) ↾ coPset_union_wf _ _ Ht1 Ht2.
-Instance coPset_intersection : Intersection coPset := λ X Y,
+Global Instance coPset_intersection : Intersection coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∩ t2) ↾ coPset_intersection_wf _ _ Ht1 Ht2.
-Instance coPset_difference : Difference coPset := λ X Y,
+Global Instance coPset_difference : Difference coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 ∩ coPset_opp_raw t2) ↾ coPset_intersection_wf _ _ Ht1 (coPset_opp_wf _).
-Instance coPset_top_set : TopSet positive coPset.
+Global Instance coPset_top_set : TopSet positive coPset.
Proof.
split; [split; [split| |]|].
- by intros ??.
@@ -186,23 +186,23 @@ Qed.
Local Definition coPset_top_subseteq := top_subseteq (C:=coPset).
Global Hint Resolve coPset_top_subseteq : core.
-Instance coPset_leibniz : LeibnizEquiv coPset.
+Global Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
intros X Y; rewrite elem_of_equiv; intros HXY.
apply (sig_eq_pi _), coPset_eq; try apply @proj2_sig.
intros p; apply eq_bool_prop_intro, (HXY p).
Qed.
-Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
+Global Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
Proof. solve_decision. Defined.
-Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
+Global 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 (##@{coPset}).
+Global 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 (⊆@{coPset}).
+Global Instance mapset_subseteq_dec : RelDecision (⊆@{coPset}).
Proof.
refine (λ X Y, cast_if (decide (X ∪ Y = Y))); abstract (by rewrite subseteq_union_L).
Defined.
@@ -232,7 +232,7 @@ Proof.
exists ([1] ++ ((~0) <$> ll) ++ ((~1) <$> rl))%list; intros [i|i|]; simpl;
rewrite elem_of_cons, elem_of_app, !elem_of_list_fmap; naive_solver.
Qed.
-Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
+Global Instance coPset_finite_dec (X : coPset) : Decision (set_finite X).
Proof.
refine (cast_if (decide (coPset_finite (`X)))); by rewrite coPset_finite_spec.
Defined.
@@ -339,15 +339,15 @@ Proof.
Qed.
(** * Domain of finite maps *)
-Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
-Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
+Global Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
+Global Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
Proof.
split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
by rewrite elem_of_Pset_to_coPset, elem_of_dom.
Qed.
-Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
+Global Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
gset_to_coPset (dom _ m).
-Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
+Global Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
Proof.
split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
by rewrite elem_of_gset_to_coPset, elem_of_dom.
diff --git a/theories/countable.v b/theories/countable.v
index aed78406eb4517dac725dae247b888c6b964f861..689ff40a8491961b7a558d085413a781259b9753 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -9,10 +9,10 @@ Class Countable A `{EqDecision A} := {
decode_encode x : decode (encode x) = Some x
}.
Global Hint Mode Countable ! - : typeclass_instances.
-Arguments encode : simpl never.
-Arguments decode : simpl never.
+Global Arguments encode : simpl never.
+Global Arguments decode : simpl never.
-Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
+Global Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
Proof.
intros x y Hxy; apply (inj Some).
by rewrite <-(decode_encode x), Hxy, decode_encode.
@@ -22,7 +22,7 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
pred (Pos.to_nat (encode x)).
Definition decode_nat `{Countable A} (i : nat) : option A :=
decode (Pos.of_nat (S i)).
-Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
+Global Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
Proof.
@@ -35,7 +35,7 @@ Definition encode_Z `{Countable A} (x : A) : Z :=
Zpos (encode x).
Definition decode_Z `{Countable A} (i : Z) : option A :=
match i with Zpos i => decode i | _ => None end.
-Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
+Global Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
Proof. apply decode_encode. Qed.
@@ -238,7 +238,7 @@ Next Obligation.
Qed.
(** ** Numbers *)
-Instance pos_countable : Countable positive :=
+Global Instance pos_countable : Countable positive :=
{| encode := id; decode := Some; decode_encode x := eq_refl |}.
Program Instance N_countable : Countable N := {|
encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
@@ -292,10 +292,10 @@ Local Close Scope positive.
Inductive gen_tree (T : Type) : Type :=
| GenLeaf : T → gen_tree T
| GenNode : nat → list (gen_tree T) → gen_tree T.
-Arguments GenLeaf {_} _ : assert.
-Arguments GenNode {_} _ _ : assert.
+Global Arguments GenLeaf {_} _ : assert.
+Global Arguments GenNode {_} _ _ : assert.
-Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
+Global Instance gen_tree_dec `{EqDecision T} : EqDecision (gen_tree T).
Proof.
refine (
fix go t1 t2 := let _ : EqDecision _ := @go in
diff --git a/theories/decidable.v b/theories/decidable.v
index df16a2edfb23ac92e37e3d40352e076fd869fdbd..310eff9a1803fce53454c1195323f7cf206b0680 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -160,9 +160,9 @@ Proof. apply dsig_eq; reflexivity. Qed.
(** * Instances of [Decision] *)
(** Instances of [Decision] for operators of propositional logic. *)
-Instance True_dec: Decision True := left I.
-Instance False_dec: Decision False := right (False_rect False).
-Instance Is_true_dec b : Decision (Is_true b).
+Global Instance True_dec: Decision True := left I.
+Global Instance False_dec: Decision False := right (False_rect False).
+Global Instance Is_true_dec b : Decision (Is_true b).
Proof. destruct b; simpl; apply _. Defined.
Section prop_dec.
@@ -177,28 +177,28 @@ Section prop_dec.
Global Instance impl_dec: Decision (P → Q).
Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
End prop_dec.
-Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+Global Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
Decision (P ↔ Q) := and_dec _ _.
(** Instances of [Decision] for common data types. *)
-Instance bool_eq_dec : EqDecision bool.
+Global Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
-Instance unit_eq_dec : EqDecision unit.
+Global Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
-Instance Empty_set_eq_dec : EqDecision Empty_set.
+Global Instance Empty_set_eq_dec : EqDecision Empty_set.
Proof. solve_decision. Defined.
-Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
+Global Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
-Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
+Global Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Proof. solve_decision. Defined.
-Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+Global Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
Decision (curry P p) :=
match p as p return Decision (curry P p) with
| (x,y) => P_dec x y
end.
-Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
+Global Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
EqDecision (sig P).
Proof.
refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
diff --git a/theories/fin.v b/theories/fin.v
index b4090fa539a4cff92132d6fed73aa9917225f0f1..0701c7a7aff7c8bb3c7a07d725705af94fa340ca 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -17,7 +17,7 @@ Notation FS := Fin.FS.
Declare Scope fin_scope.
Delimit Scope fin_scope with fin.
-Arguments Fin.FS _ _%fin : assert.
+Global Arguments Fin.FS _ _%fin : assert.
Notation "0" := Fin.F1 : fin_scope. Notation "1" := (FS 0) : fin_scope.
Notation "2" := (FS 1) : fin_scope. Notation "3" := (FS 2) : fin_scope.
@@ -33,7 +33,7 @@ Coercion fin_to_nat : fin >-> nat.
Notation nat_to_fin := Fin.of_nat_lt.
Notation fin_rect2 := Fin.rect2.
-Instance fin_dec {n} : EqDecision (fin n).
+Global Instance fin_dec {n} : EqDecision (fin n).
Proof.
refine (fin_rect2
(λ n (i j : fin n), { i = j } + { i ≠j })
@@ -71,9 +71,9 @@ Ltac inv_fin i :=
end
end.
-Instance FS_inj {n} : Inj (=) (=) (@FS n).
+Global Instance FS_inj {n} : Inj (=) (=) (@FS n).
Proof. intros i j. apply Fin.FS_inj. Qed.
-Instance fin_to_nat_inj {n} : Inj (=) (=) (@fin_to_nat n).
+Global Instance fin_to_nat_inj {n} : Inj (=) (=) (@fin_to_nat n).
Proof.
intros i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
Qed.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 991b01a286c06ad72e93c9aeddb6cf3f1fa0c464..7552879fee5ead5d5aafd3cfcff2a5d6bfcc0947 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -271,6 +271,6 @@ Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
Proof. unfold_leibniz. apply dom_seq. Qed.
-Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) i :
+Global Instance set_unfold_dom_seq `{FinMapDom nat M D} {A} start (xs : list A) i :
SetUnfoldElemOf i (dom D (map_seq start (M:=M A) xs)) (start ≤ i < start + length xs).
Proof. constructor. by rewrite dom_seq, elem_of_set_seq. Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 2b37071339478ef3f662aee63101dbfd02d6ca26..2d23b0967f97a7c94622bb09f735fc7ac3ffe5ab 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -55,19 +55,19 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
finite map implementations. These generic implementations do not cause a
significant performance loss, which justifies including them in the finite map
interface as primitive operations. *)
-Instance map_insert `{PartialAlter K A M} : Insert K A M :=
+Global Instance map_insert `{PartialAlter K A M} : Insert K A M :=
λ i x, partial_alter (λ _, Some x) i.
-Instance map_alter `{PartialAlter K A M} : Alter K A M :=
+Global Instance map_alter `{PartialAlter K A M} : Alter K A M :=
λ f, partial_alter (fmap f).
-Instance map_delete `{PartialAlter K A M} : Delete K M :=
+Global Instance map_delete `{PartialAlter K A M} : Delete K M :=
partial_alter (λ _, None).
-Instance map_singleton `{PartialAlter K A M, Empty M} :
+Global Instance map_singleton `{PartialAlter K A M, Empty M} :
SingletonM K A M := λ i x, <[i:=x]> ∅.
Definition list_to_map `{Insert K A M, Empty M} : list (K * A) → M :=
fold_right (λ p, <[p.1:=p.2]>) ∅.
-Instance map_size `{FinMapToList K A M} : Size M := λ m, length (map_to_list m).
+Global Instance map_size `{FinMapToList K A M} : Size M := λ m, length (map_to_list m).
Definition map_to_set `{FinMapToList K A M,
Singleton B C, Empty C, Union C} (f : K → A → B) (m : M) : C :=
@@ -76,16 +76,16 @@ Definition set_to_map `{Elements B C, Insert K A M, Empty M}
(f : B → K * A) (X : C) : M :=
list_to_map (f <$> elements X).
-Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
+Global Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
λ f, merge (union_with f).
-Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
+Global Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
λ f, merge (intersection_with f).
-Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
+Global Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
λ f, merge (difference_with f).
(** Higher precedence to make sure it's not used for other types with a [Lookup]
instance, such as lists. *)
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
+Global Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 20 :=
λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
@@ -102,20 +102,20 @@ Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
Global Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
-Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
+Global Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_included (=).
(** The union of two finite maps only has a meaningful definition for maps
that are disjoint. However, as working with partial functions is inconvenient
in Coq, we define the union as a total function. In case both finite maps
have a value at the same index, we take the value of the first map. *)
-Instance map_union `{Merge M} {A} : Union (M A) := union_with (λ x _, Some x).
-Instance map_intersection `{Merge M} {A} : Intersection (M A) :=
+Global Instance map_union `{Merge M} {A} : Union (M A) := union_with (λ x _, Some x).
+Global Instance map_intersection `{Merge M} {A} : Intersection (M A) :=
intersection_with (λ x _, Some x).
(** The difference operation removes all values from the first map whose
index contains a value in the second map as well. *)
-Instance map_difference `{Merge M} {A} : Difference (M A) :=
+Global Instance map_difference `{Merge M} {A} : Difference (M A) :=
difference_with (λ _ _, None).
(** A stronger variant of map that allows the mapped function to use the index
@@ -136,7 +136,7 @@ is unspecified. *)
Definition map_fold `{FinMapToList K A M} {B}
(f : K → A → B → B) (b : B) : M → B := foldr (curry f) b ∘ map_to_list.
-Instance map_filter `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
+Global Instance map_filter `{FinMapToList K A M, Insert K A M, Empty M} : Filter (K * A) M :=
λ P _, map_fold (λ k v m, if decide (P (k,v)) then <[k := v]>m else m) ∅.
Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M :=
@@ -145,7 +145,7 @@ Fixpoint map_seq `{Insert nat A M, Empty M} (start : nat) (xs : list A) : M :=
| x :: xs => <[start:=x]> (map_seq (S start) xs)
end.
-Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} :
+Global Instance finmap_lookup_total `{!Lookup K A (M A), !Inhabited A} :
LookupTotal K A (M A) | 20 := λ i m, default inhabitant (m !! i).
Typeclasses Opaque finmap_lookup_total.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index fd7ca4a54f9fde663ef8b607fae5786211111ff5..9f3180ba6384504292c3b69c9168ac424b6cac86 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -9,12 +9,12 @@ From stdpp Require Import options.
Set Default Proof Using "Type*".
(** Operations *)
-Instance set_size `{Elements A C} : Size C := length ∘ elements.
+Global Instance set_size `{Elements A C} : Size C := length ∘ elements.
Definition set_fold `{Elements A C} {B}
(f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
-Instance set_filter
+Global Instance set_filter
`{Elements A C, Empty C, Singleton A C, Union C} : Filter A C := λ P _ X,
list_to_set (filter P (elements X)).
Typeclasses Opaque set_filter.
@@ -24,7 +24,7 @@ Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
list_to_set (f <$> elements X).
Typeclasses Opaque set_map.
-Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
+Global Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
fresh ∘ elements.
Typeclasses Opaque set_filter.
@@ -53,7 +53,7 @@ Implicit Types X Y : C.
Lemma fin_set_finite X : set_finite X.
Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
-Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
+Local Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
Proof.
refine (λ x X, cast_if (decide_rel (∈) x (elements X)));
by rewrite <-(elem_of_elements _).
diff --git a/theories/finite.v b/theories/finite.v
index 7347e1a010824ddcbfbbac820f7dc3b94c0776ec..6bd7d4af78781c5af2c000952d00e492c0864b32 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -8,10 +8,10 @@ Class Finite A `{EqDecision A} := {
elem_of_enum x : x ∈ enum
}.
Global Hint Mode Finite ! - : typeclass_instances.
-Arguments enum : clear implicits.
-Arguments enum _ {_ _} : assert.
-Arguments NoDup_enum : clear implicits.
-Arguments NoDup_enum _ {_ _} : assert.
+Global Arguments enum : clear implicits.
+Global Arguments enum _ {_ _} : assert.
+Global Arguments NoDup_enum : clear implicits.
+Global Arguments NoDup_enum _ {_ _} : assert.
Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {|
@@ -19,7 +19,7 @@ Program Definition finite_countable `{Finite A} : Countable A := {|
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =.) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
-Arguments Pos.of_nat : simpl never.
+Global Arguments Pos.of_nat : simpl never.
Next Obligation.
intros ?? [xs Hxs HA] x; unfold encode, decode; simpl.
destruct (list_find_elem_of (x =.) xs x) as [[i y] Hi]; auto.
diff --git a/theories/gmap.v b/theories/gmap.v
index ada9e445041c1f81b93f2308dcc4f609c64909d3..c8b7199dd68ff10fdb3de22f4a4e16485f38179e 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -26,24 +26,24 @@ Record gmap K `{Countable K} A := GMap {
gmap_car : Pmap A;
gmap_prf : gmap_wf K gmap_car
}.
-Arguments GMap {_ _ _ _} _ _ : assert.
-Arguments gmap_car {_ _ _ _} _ : assert.
+Global Arguments GMap {_ _ _ _} _ _ : assert.
+Global Arguments gmap_car {_ _ _ _} _ : assert.
Lemma gmap_eq `{Countable K} {A} (m1 m2 : gmap K A) :
m1 = m2 ↔ gmap_car m1 = gmap_car m2.
Proof.
split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
f_equal; apply proof_irrel.
Qed.
-Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
+Global Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
Proof.
refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
abstract (by rewrite gmap_eq).
Defined.
(** * Operations on the data structure *)
-Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
+Global Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) :=
λ i '(GMap m _), m !! encode i.
-Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
+Global Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
(** Block reduction, even on concrete [gmap]s.
Marking [gmap_empty] as [simpl never] would not be enough, because of
https://github.com/coq/coq/issues/2972 and
@@ -61,7 +61,7 @@ Proof.
- rewrite lookup_partial_alter_ne by done. by apply Hm.
Qed.
-Instance gmap_partial_alter `{Countable K} {A} :
+Global Instance gmap_partial_alter `{Countable K} {A} :
PartialAlter K A (gmap K A) := λ f i '(GMap m Hm),
GMap (partial_alter f (encode i) m) (gmap_partial_alter_wf f m i Hm).
@@ -71,7 +71,7 @@ Proof.
unfold gmap_wf; rewrite !bool_decide_spec.
intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto.
Qed.
-Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
+Global Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f '(GMap m Hm),
GMap (f <$> m) (gmap_fmap_wf f m Hm).
Lemma gmap_omap_wf `{Countable K} {A B} (f : A → option B) m :
gmap_wf K m → gmap_wf K (omap f m).
@@ -79,7 +79,7 @@ Proof.
unfold gmap_wf; rewrite !bool_decide_spec.
intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto.
Qed.
-Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
+Global Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm),
GMap (omap f m) (gmap_omap_wf f m Hm).
Lemma gmap_merge_wf `{Countable K} {A B C}
(f : option A → option B → option C) m1 m2 :
@@ -90,14 +90,14 @@ Proof.
intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
Qed.
-Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
+Global Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
GMap (merge f' m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
-Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
+Global Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
(** * Instantiation of the finite map interface *)
-Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
+Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
Proof.
split.
- unfold lookup; intros A [m1 Hm1] [m2 Hm2] Hm.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index fbff2e5856b1b15852c0c20936e56742f143df5d..3d164a8e8394e9075b4409ad8ce0a2a9e0e643bb 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -3,10 +3,10 @@ From stdpp Require Import gmap.
From stdpp Require Import options.
Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
-Arguments GMultiSet {_ _ _} _ : assert.
-Arguments gmultiset_car {_ _ _} _ : assert.
+Global Arguments GMultiSet {_ _ _} _ : assert.
+Global Arguments gmultiset_car {_ _ _} _ : assert.
-Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
+Global Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
Proof. solve_decision. Defined.
Program Instance gmultiset_countable `{Countable A} :
@@ -169,7 +169,7 @@ universally quantified hypotheses [H : ∀ x : A, P x] in two ways:
*)
Class MultisetUnfold `{Countable A} (x : A) (X : gmultiset A) (n : nat) :=
{ multiset_unfold : multiplicity x X = n }.
-Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
+Global Arguments multiset_unfold {_ _ _} _ _ _ {_} : assert.
Global Hint Mode MultisetUnfold + + + - + - : typeclass_instances.
Section multiset_unfold.
@@ -470,7 +470,7 @@ Section more_lemmas.
Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
Proof. apply strict_include. Qed.
- Hint Resolve gmultiset_subset_subseteq : core.
+ Local Hint Resolve gmultiset_subset_subseteq : core.
Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
Proof. multiset_solver. Qed.
diff --git a/theories/hashset.v b/theories/hashset.v
index 9588536abfb5a12e1ef405765132518ec3fecf96..a37eb83e267ccae144b3f05c60b6df6b9d324a51 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -10,8 +10,8 @@ Record hashset {A} (hash : A → Z) := Hashset {
hashset_prf :
map_Forall (λ n l, Forall (λ x, hash x = n) l ∧ NoDup l) hashset_car
}.
-Arguments Hashset {_ _} _ _ : assert.
-Arguments hashset_car {_ _} _ : assert.
+Global Arguments Hashset {_ _} _ _ : assert.
+Global Arguments hashset_car {_ _} _ : assert.
Section hashset.
Context `{EqDecision A} (hash : A → Z).
diff --git a/theories/hlist.v b/theories/hlist.v
index d7f0ad921c8b6daf5920a8ad881d74136059713b..51dc2a8cfce870be8aa15cab4e1336a1332cfe97 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -35,7 +35,7 @@ Fixpoint himpl (As : tlist) (B : Type) : Type :=
Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
-Arguments hlam _ _ _ _ _ / : assert.
+Global Arguments hlam _ _ _ _ _ / : assert.
Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
(fix go {As} xs :=
diff --git a/theories/infinite.v b/theories/infinite.v
index 3ca0885127f295fcbf4c9dadb75055589e4fffe6..395756c0dd776e14153b0bea276e9b18bc56933e 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -123,17 +123,17 @@ Program Instance Z_infinite: Infinite Z :=
Solve Obligations with (intros; simpl; lia).
(** Instances for option, sum, products *)
-Instance option_infinite `{Infinite A} : Infinite (option A) :=
+Global Instance option_infinite `{Infinite A} : Infinite (option A) :=
inj_infinite Some id (λ _, eq_refl).
-Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) :=
+Global Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) :=
inj_infinite inl (maybe inl) (λ _, eq_refl).
-Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
+Global Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
inj_infinite inr (maybe inr) (λ _, eq_refl).
-Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
+Global Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
inj_infinite (., inhabitant) (Some ∘ fst) (λ _, eq_refl).
-Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
+Global Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
inj_infinite (inhabitant ,.) (Some ∘ snd) (λ _, eq_refl).
(** Instance for lists *)
diff --git a/theories/lexico.v b/theories/lexico.v
index 7e9be13326487709d6c82ddb691b149c2a469af4..59a387b45738b4673a9fa9790694105f5cb7a076 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -10,17 +10,17 @@ Notation cast_trichotomy T :=
| inright _ => inright _
end.
-Instance prod_lexico `{Lexico A, Lexico B} : Lexico (A * B) := λ p1 p2,
+Global Instance prod_lexico `{Lexico A, Lexico B} : Lexico (A * B) := λ p1 p2,
(**i 1.) *) lexico (p1.1) (p2.1) ∨
(**i 2.) *) p1.1 = p2.1 ∧ lexico (p1.2) (p2.2).
-Instance bool_lexico : Lexico bool := λ b1 b2,
+Global Instance bool_lexico : Lexico bool := λ b1 b2,
match b1, b2 with false, true => True | _, _ => False end.
-Instance nat_lexico : Lexico nat := (<).
-Instance N_lexico : Lexico N := (<)%N.
-Instance Z_lexico : Lexico Z := (<)%Z.
+Global Instance nat_lexico : Lexico nat := (<).
+Global Instance N_lexico : Lexico N := (<)%N.
+Global Instance Z_lexico : Lexico Z := (<)%Z.
Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
-Instance list_lexico `{Lexico A} : Lexico (list A) :=
+Global Instance list_lexico `{Lexico A} : Lexico (list A) :=
fix go l1 l2 :=
let _ : Lexico (list A) := @go in
match l1, l2 with
@@ -28,7 +28,7 @@ Instance list_lexico `{Lexico A} : Lexico (list A) :=
| x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
| _, _ => False
end.
-Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
+Global Instance sig_lexico `{Lexico A} (P : A → Prop) `{∀ x, ProofIrrel (P x)} :
Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).
Lemma prod_lexico_irreflexive `{Lexico A, Lexico B, !Irreflexive (@lexico A _)}
@@ -44,7 +44,7 @@ Proof.
by left; trans x2.
Qed.
-Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
+Global Instance prod_lexico_po `{Lexico A, Lexico B, !StrictOrder (@lexico A _)}
`{!StrictOrder (@lexico B _)} : StrictOrder (@lexico (A * B) _).
Proof.
split.
@@ -53,7 +53,7 @@ Proof.
- intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply transitivity.
Qed.
-Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
+Global Instance prod_lexico_trichotomyT `{Lexico A, tA : !TrichotomyT (@lexico A _)}
`{Lexico B, tB : !TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
Proof.
red; refine (λ p1 p2,
@@ -65,13 +65,13 @@ Proof.
abstract (unfold lexico, prod_lexico; auto using injective_projections).
Defined.
-Instance bool_lexico_po : StrictOrder (@lexico bool _).
+Global Instance bool_lexico_po : StrictOrder (@lexico bool _).
Proof.
split.
- by intros [] ?.
- by intros [] [] [] ??.
Qed.
-Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
+Global Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
red; refine (λ b1 b2,
match b1, b2 with
@@ -82,9 +82,9 @@ Proof.
end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.
-Instance nat_lexico_po : StrictOrder (@lexico nat _).
+Global Instance nat_lexico_po : StrictOrder (@lexico nat _).
Proof. unfold lexico, nat_lexico. apply _. Qed.
-Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
+Global Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
Proof.
red; refine (λ n1 n2,
match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c → _ with
@@ -94,9 +94,9 @@ Proof.
end eq_refl).
Defined.
-Instance N_lexico_po : StrictOrder (@lexico N _).
+Global Instance N_lexico_po : StrictOrder (@lexico N _).
Proof. unfold lexico, N_lexico. apply _. Qed.
-Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
+Global Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
Proof.
red; refine (λ n1 n2,
match N.compare n1 n2 as c return N.compare n1 n2 = c → _ with
@@ -106,9 +106,9 @@ Proof.
end eq_refl).
Defined.
-Instance Z_lexico_po : StrictOrder (@lexico Z _).
+Global Instance Z_lexico_po : StrictOrder (@lexico Z _).
Proof. unfold lexico, Z_lexico. apply _. Qed.
-Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
+Global Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
Proof.
red; refine (λ n1 n2,
match Z.compare n1 n2 as c return Z.compare n1 n2 = c → _ with
@@ -118,7 +118,7 @@ Proof.
end eq_refl).
Defined.
-Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
+Global Instance list_lexico_po `{Lexico A, !StrictOrder (@lexico A _)} :
StrictOrder (@lexico (list A) _).
Proof.
split.
@@ -126,7 +126,7 @@ Proof.
- intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
eapply prod_lexico_transitive; eauto.
Qed.
-Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
+Global Instance list_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)} :
TrichotomyT (@lexico (list A) _).
Proof.
refine (
@@ -141,14 +141,14 @@ Proof.
abstract (repeat (done || constructor || congruence || by inversion 1)).
Defined.
-Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
+Global Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
Proof.
unfold lexico, sig_lexico. split.
- intros [x ?] ?. by apply (irreflexivity lexico x).
- intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
Qed.
-Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
+Global Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
(P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
Proof.
red; refine (λ x1 x2, cast_trichotomy (trichotomyT lexico (`x1) (`x2)));
diff --git a/theories/list.v b/theories/list.v
index 25b5e23e96f5d447b89b5c93dda489b7b474361f..d8faeaf085f458044b8cd1454d23d20c1cf7651c 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -7,9 +7,9 @@ From stdpp Require Import options.
(* Pick up extra assumptions from section parameters. *)
Set Default Proof Using "Type*".
-Arguments length {_} _ : assert.
-Arguments cons {_} _ _ : assert.
-Arguments app {_} _ _ : assert.
+Global Arguments length {_} _ : assert.
+Global Arguments cons {_} _ _ : assert.
+Global Arguments app {_} _ _ : assert.
Instance: Params (@length) 1 := {}.
Instance: Params (@cons) 1 := {}.
@@ -19,18 +19,18 @@ Notation tail := tl.
Notation take := firstn.
Notation drop := skipn.
-Arguments head {_} _ : assert.
-Arguments tail {_} _ : assert.
-Arguments take {_} !_ !_ / : assert.
-Arguments drop {_} !_ !_ / : assert.
+Global Arguments head {_} _ : assert.
+Global Arguments tail {_} _ : assert.
+Global Arguments take {_} !_ !_ / : assert.
+Global Arguments drop {_} !_ !_ / : assert.
Instance: Params (@head) 1 := {}.
Instance: Params (@tail) 1 := {}.
Instance: Params (@take) 1 := {}.
Instance: Params (@drop) 1 := {}.
-Arguments Permutation {_} _ _ : assert.
-Arguments Forall_cons {_} _ _ _ _ _ : assert.
+Global Arguments Permutation {_} _ _ : assert.
+Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : list_scope.
@@ -53,7 +53,7 @@ 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,
+Global Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
match l with x :: l => Some (x,l) | _ => None end.
(** * Definitions *)
@@ -65,7 +65,7 @@ Existing Instance list_equiv.
(** The operation [l !! i] gives the [i]th element of the list [l], or [None]
in case [i] is out of bounds. *)
-Instance list_lookup {A} : Lookup nat A (list A) :=
+Global Instance list_lookup {A} : Lookup nat A (list A) :=
fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
match l with
| [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
@@ -73,7 +73,7 @@ Instance list_lookup {A} : Lookup nat A (list A) :=
(** The operation [l !!! i] is a total version of the lookup operation
[l !! i]. *)
-Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
+Global Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
fix go i l {struct l} : A := let _ : LookupTotal _ _ _ := @go in
match l with
| [] => inhabitant
@@ -82,7 +82,7 @@ Instance list_lookup_total `{!Inhabited A} : LookupTotal nat A (list A) :=
(** The operation [alter f i l] applies the function [f] to the [i]th element
of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_alter {A} : Alter nat A (list A) := λ f,
+Global Instance list_alter {A} : Alter nat A (list A) := λ f,
fix go i l {struct l} :=
match l with
| [] => []
@@ -91,7 +91,7 @@ Instance list_alter {A} : Alter nat A (list A) := λ f,
(** The operation [<[i:=x]> l] overwrites the element at position [i] with the
value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_insert {A} : Insert nat A (list A) :=
+Global Instance list_insert {A} : Insert nat A (list A) :=
fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
match l with
| [] => []
@@ -107,7 +107,7 @@ Instance: Params (@list_inserts) 1 := {}.
(** The operation [delete i l] removes the [i]th element of [l] and moves
all consecutive elements one position ahead. In case [i] is out of bounds,
the list is returned unchanged. *)
-Instance list_delete {A} : Delete nat (list A) :=
+Global Instance list_delete {A} : Delete nat (list A) :=
fix go (i : nat) (l : list A) {struct l} : list A :=
match l with
| [] => []
@@ -118,12 +118,12 @@ Instance list_delete {A} : Delete nat (list A) :=
singleton list [[x]], and [None] into the empty list [[]]. *)
Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
Instance: Params (@option_list) 1 := {}.
-Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
+Global Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
match l with [x] => Some x | _ => None end.
(** The function [filter P l] returns the list of elements of [l] that
satisfies [P]. The order remains unchanged. *)
-Instance list_filter {A} : Filter A (list A) :=
+Global Instance list_filter {A} : Filter A (list A) :=
fix go P _ l := let _ : Filter _ _ := @go in
match l with
| [] => []
@@ -178,7 +178,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
| [] => replicate n y
| x :: l => match n with 0 => [] | S n => x :: resize n y l end
end.
-Arguments resize {_} !_ _ !_ : assert.
+Global Arguments resize {_} !_ _ !_ : assert.
Instance: Params (@resize) 2 := {}.
(** The function [reshape k l] transforms [l] into a list of lists whose sizes
@@ -203,18 +203,18 @@ Definition foldl {A B} (f : A → B → A) : A → list B → A :=
fix go a l := match l with [] => a | x :: l => go (f a x) l end.
(** The monadic operations. *)
-Instance list_ret: MRet list := λ A x, x :: @nil A.
-Instance list_fmap : FMap list := λ A B f,
+Global Instance list_ret: MRet list := λ A x, x :: @nil A.
+Global Instance list_fmap : FMap list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x :: go l end.
-Instance list_omap : OMap list := λ A B f,
+Global Instance list_omap : OMap list := λ A B f,
fix go (l : list A) :=
match l with
| [] => []
| x :: l => match f x with Some y => y :: go l | None => go l end
end.
-Instance list_bind : MBind list := λ A B f,
+Global Instance list_bind : MBind list := λ A B f,
fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
-Instance list_join: MJoin list :=
+Global Instance list_join: MJoin list :=
fix go A (ls : list (list A)) : list A :=
match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) :=
@@ -247,8 +247,8 @@ Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
| zipped_Forall_nil l : zipped_Forall P l []
| zipped_Forall_cons l k x :
P l k x → zipped_Forall P (x :: l) k → zipped_Forall P l (x :: k).
-Arguments zipped_Forall_nil {_ _} _ : assert.
-Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.
+Global Arguments zipped_Forall_nil {_ _} _ : assert.
+Global Arguments zipped_Forall_cons {_ _} _ _ _ _ _ : assert.
(** The function [mask f βs l] applies the function [f] to elements in [l] at
positions that are [true] in [βs]. *)
@@ -337,7 +337,7 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
(** Set operations on lists *)
-Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → x ∈ l2.
+Global Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 → x ∈ l2.
Section list_set.
Context `{dec : EqDecision A}.
@@ -3113,7 +3113,7 @@ End Forall2_proper.
Section Forall3.
Context {A B C} (P : A → B → C → Prop).
- Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
+ Local Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
@@ -3988,7 +3988,7 @@ Lemma foldr_permutation_proper {A B} (R : relation B) `{!PreOrder R}
(Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
Proper ((≡ₚ) ==> R) (foldr f b).
Proof. intros l1 l2 Hl. apply foldr_permutation; auto. Qed.
-Instance foldr_permutation_proper' {A} (R : relation A) `{!PreOrder R}
+Global Instance foldr_permutation_proper' {A} (R : relation A) `{!PreOrder R}
(f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} :
Proper ((≡ₚ) ==> R) (foldr f a).
Proof.
@@ -4261,7 +4261,7 @@ Qed.
Lemma TCForall_Forall {A} (P : A → Prop) xs : TCForall P xs ↔ Forall P xs.
Proof. split; induction 1; constructor; auto. Qed.
-Instance TCForall_app {A} (P : A → Prop) xs ys :
+Global Instance TCForall_app {A} (P : A → Prop) xs ys :
TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
@@ -4385,9 +4385,9 @@ over the type of constants, but later we use [nat]s and a list representing
a corresponding environment. *)
Inductive rlist (A : Type) :=
rnil : rlist A | rnode : A → rlist A | rapp : rlist A → rlist A → rlist A.
-Arguments rnil {_} : assert.
-Arguments rnode {_} _ : assert.
-Arguments rapp {_} _ _ : assert.
+Global Arguments rnil {_} : assert.
+Global Arguments rnode {_} _ : assert.
+Global Arguments rapp {_} _ _ : assert.
Module rlist.
Fixpoint to_list {A} (t : rlist A) : list A :=
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 917b67ce51b7a9adc2291b8de4e2b4b8c761f070..0045b143eac42dd2e9447966b5d15cc26a1f0c39 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -8,7 +8,7 @@ From stdpp Require Import options.
over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
Definition seqZ (m len: Z) : list Z :=
(λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
-Arguments seqZ : simpl never.
+Global Arguments seqZ : simpl never.
Definition sum_list_with {A} (f : A → nat) : list A → nat :=
fix go l :=
diff --git a/theories/listset.v b/theories/listset.v
index 7c3a2f275a742f3945685e3b4ccad96794208314..bb023853d3bf3ef538060d17a98cac72a65ed5ee 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -4,8 +4,8 @@ From stdpp Require Export sets list.
From stdpp Require Import options.
Record listset A := Listset { listset_car: list A }.
-Arguments listset_car {_} _ : assert.
-Arguments Listset {_} _ : assert.
+Global Arguments listset_car {_} _ : assert.
+Global Arguments Listset {_} _ : assert.
Section listset.
Context {A : Type}.
@@ -48,7 +48,7 @@ Global Instance listset_intersection: Intersection (listset A) :=
Global Instance listset_difference: Difference (listset A) :=
λ '(Listset l) '(Listset k), Listset (list_difference l k).
-Instance listset_set: Set_ A (listset A).
+Local Instance listset_set: Set_ A (listset A).
Proof.
split.
- apply _.
@@ -66,14 +66,14 @@ Proof.
Qed.
End listset.
-Instance listset_ret: MRet listset := λ A x, {[ x ]}.
-Instance listset_fmap: FMap listset := λ A B f '(Listset l),
+Global Instance listset_ret: MRet listset := λ A x, {[ x ]}.
+Global Instance listset_fmap: FMap listset := λ A B f '(Listset l),
Listset (f <$> l).
-Instance listset_bind: MBind listset := λ A B f '(Listset l),
+Global Instance listset_bind: MBind listset := λ A B f '(Listset l),
Listset (mbind (listset_car ∘ f) l).
-Instance listset_join: MJoin listset := λ A, mbind id.
+Global Instance listset_join: MJoin listset := λ A, mbind id.
-Instance listset_set_monad : MonadSet listset.
+Global Instance listset_set_monad : MonadSet listset.
Proof.
split.
- intros. apply _.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index 84dc7c519b49531244a2606b598fb5afd269ba19..84f5b476cb8b00c5df4c901dbdf6554c30e0dd48 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -7,9 +7,9 @@ From stdpp Require Import options.
Record listset_nodup A := ListsetNoDup {
listset_nodup_car : list A; listset_nodup_prf : NoDup listset_nodup_car
}.
-Arguments ListsetNoDup {_} _ _ : assert.
-Arguments listset_nodup_car {_} _ : assert.
-Arguments listset_nodup_prf {_} _ : assert.
+Global Arguments ListsetNoDup {_} _ _ : assert.
+Global Arguments listset_nodup_car {_} _ : assert.
+Global Arguments listset_nodup_prf {_} _ : assert.
Section list_set.
Context `{EqDecision A}.
@@ -29,7 +29,7 @@ Global Instance listset_nodup_difference: Difference C :=
λ '(ListsetNoDup l Hl) '(ListsetNoDup k Hk),
ListsetNoDup _ (NoDup_list_difference _ k Hl).
-Instance listset_nodup_set: Set_ A C.
+Local Instance listset_nodup_set: Set_ A C.
Proof.
split; [split | | ].
- by apply not_elem_of_nil.
diff --git a/theories/mapset.v b/theories/mapset.v
index cee12c66f465e76d1d0a4d71b15122d3cb0cd42a..fe0d2c7bae1645bd285b586ee7a76a1f90e55e53 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -10,8 +10,8 @@ Unset Default Proof Using.
Record mapset (M : Type → Type) : Type :=
Mapset { mapset_car: M (unit : Type) }.
-Arguments Mapset {_} _ : assert.
-Arguments mapset_car {_} _ : assert.
+Global Arguments Mapset {_} _ : assert.
+Global Arguments mapset_car {_} _ : assert.
Section mapset.
Context `{FinMap K M}.
@@ -37,7 +37,7 @@ Proof.
f_equal. apply map_eq. intros i. apply option_eq. intros []. by apply E.
Qed.
-Instance mapset_set: Set_ K (mapset M).
+Local Instance mapset_set: Set_ K (mapset M).
Proof.
split; [split | | ].
- unfold empty, elem_of, mapset_empty, mapset_elem_of.
@@ -124,8 +124,8 @@ Proof.
- destruct (Is_true_reflect (f a)); naive_solver.
- naive_solver.
Qed.
-Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
-Instance mapset_dom_spec: FinMapDom K M (mapset M).
+Local Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+Local Instance mapset_dom_spec: FinMapDom K M (mapset M).
Proof.
split; try apply _. intros. unfold dom, mapset_dom, is_Some.
rewrite elem_of_mapset_dom_with; naive_solver.
@@ -136,4 +136,4 @@ End mapset.
not unfold it and try to unify [∈] against goals with [=]. *)
Opaque mapset_elem_of.
-Arguments mapset_eq_dec : simpl never.
+Global Arguments mapset_eq_dec : simpl never.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index dccbca7c650107064cbf94f45137dd2a75add8d9..7065e423dedebffe10685a4c8776b6a4ac53c25d 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -2,8 +2,8 @@ From stdpp Require Export countable coPset.
From stdpp Require Import options.
Definition namespace := list positive.
-Instance namespace_eq_dec : EqDecision namespace := _.
-Instance namespace_countable : Countable namespace := _.
+Global Instance namespace_eq_dec : EqDecision namespace := _.
+Global Instance namespace_countable : Countable namespace := _.
Typeclasses Opaque namespace.
Definition nroot : namespace := nil.
@@ -17,14 +17,14 @@ Definition ndot_eq : @ndot = @ndot_def := seal_eq ndot_aux.
Definition nclose_def (N : namespace) : coPset :=
coPset_suffixes (positives_flatten N).
Definition nclose_aux : seal (@nclose_def). by eexists. Qed.
-Instance nclose : UpClose namespace coPset := unseal nclose_aux.
+Global Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
Notation "N .@ x" := (ndot N x)
(at level 19, left associativity, format "N .@ x") : stdpp_scope.
Notation "(.@)" := ndot (only parsing) : stdpp_scope.
-Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ## nclose N2.
+Global Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ## nclose N2.
Section namespace.
Context `{Countable A}.
diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index 218a21a903c962d48fc61c7eb0f5caff14f108b4..b6cc0ae8f3ece77be94676b1763ef5b95eb3d7c1 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -54,49 +54,49 @@ Module nat_cancel.
https://gitlab.mpi-sws.org/FP/iris-coq/issues/153
we wrap the entire canceler in the [NoBackTrack] class. *)
- Instance nat_cancel_start m n m' n' :
+ Global Instance nat_cancel_start m n m' n' :
TCNoBackTrack (NatCancelL m n m' n') → NatCancel m n m' n'.
Proof. by intros [?]. Qed.
Class MakeNatS (n1 n2 m : nat) := make_nat_S : m = n1 + n2.
- Instance make_nat_S_0_l n : MakeNatS 0 n n.
+ Global Instance make_nat_S_0_l n : MakeNatS 0 n n.
Proof. done. Qed.
- Instance make_nat_S_1 n : MakeNatS 1 n (S n).
+ Global Instance make_nat_S_1 n : MakeNatS 1 n (S n).
Proof. done. Qed.
Class MakeNatPlus (n1 n2 m : nat) := make_nat_plus : m = n1 + n2.
- Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
+ Global Instance make_nat_plus_0_l n : MakeNatPlus 0 n n.
Proof. done. Qed.
- Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
+ Global Instance make_nat_plus_0_r n : MakeNatPlus n 0 n.
Proof. unfold MakeNatPlus. by rewrite Nat.add_0_r. Qed.
- Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
+ Global Instance make_nat_plus_default n1 n2 : MakeNatPlus n1 n2 (n1 + n2) | 100.
Proof. done. Qed.
- Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
+ Global Instance nat_cancel_leaf_here m : NatCancelR m m 0 0 | 0.
Proof. by unfold NatCancelR, NatCancelL. Qed.
- Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
+ Global Instance nat_cancel_leaf_else m n : NatCancelR m n m n | 100.
Proof. by unfold NatCancelR. Qed.
- Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
+ Global Instance nat_cancel_leaf_plus m m' m'' n1 n2 n1' n2' n1'n2' :
NatCancelR m n1 m' n1' → NatCancelR m' n2 m'' n2' →
MakeNatPlus n1' n2' n1'n2' → NatCancelR m (n1 + n2) m'' n1'n2' | 2.
Proof. unfold NatCancelR, NatCancelL, MakeNatPlus. lia. Qed.
- Instance nat_cancel_leaf_S_here m n m' n' :
+ Global Instance nat_cancel_leaf_S_here m n m' n' :
NatCancelR m n m' n' → NatCancelR (S m) (S n) m' n' | 3.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
- Instance nat_cancel_leaf_S_else m n m' n' :
+ Global Instance nat_cancel_leaf_S_else m n m' n' :
NatCancelR m n m' n' → NatCancelR m (S n) m' (S n') | 4.
Proof. unfold NatCancelR, NatCancelL. lia. Qed.
(** The instance [nat_cancel_S_both] is redundant, but may reduce proof search
quite a bit, e.g. when canceling constants in constants. *)
- Instance nat_cancel_S_both m n m' n' :
+ Global Instance nat_cancel_S_both m n m' n' :
NatCancelL m n m' n' → NatCancelL (S m) (S n) m' n' | 1.
Proof. unfold NatCancelL. lia. Qed.
- Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
+ Global Instance nat_cancel_plus m1 m2 m1' m2' m1'm2' n n' n'' :
NatCancelL m1 n m1' n' → NatCancelL m2 n' m2' n'' →
MakeNatPlus m1' m2' m1'm2' → NatCancelL (m1 + m2) n m1'm2' n'' | 2.
Proof. unfold NatCancelL, MakeNatPlus. lia. Qed.
- Instance nat_cancel_S m m' m'' Sm' n n' n'' :
+ Global Instance nat_cancel_S m m' m'' Sm' n n' n'' :
NatCancelL m n m' n' → NatCancelR 1 n' m'' n'' →
MakeNatS m'' m' Sm' → NatCancelL (S m) n Sm' n'' | 3.
Proof. unfold NatCancelR, NatCancelL, MakeNatS. lia. Qed.
diff --git a/theories/natmap.v b/theories/natmap.v
index 8c92083726b6b9371cfd6813968da51449e83272..99c6df31943216b09ce24f4fe28869e1a668cd45 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -7,7 +7,7 @@ From stdpp Require Import options.
Notation natmap_raw A := (list (option A)).
Definition natmap_wf {A} (l : natmap_raw A) :=
match last l with None => True | Some x => is_Some x end.
-Instance natmap_wf_pi {A} (l : natmap_raw A) : ProofIrrel (natmap_wf l).
+Global Instance natmap_wf_pi {A} (l : natmap_raw A) : ProofIrrel (natmap_wf l).
Proof. unfold natmap_wf. case_match; apply _. Qed.
Lemma natmap_wf_inv {A} (o : option A) (l : natmap_raw A) :
@@ -26,9 +26,9 @@ Record natmap (A : Type) : Type := NatMap {
natmap_car : natmap_raw A;
natmap_prf : natmap_wf natmap_car
}.
-Arguments NatMap {_} _ _ : assert.
-Arguments natmap_car {_} _ : assert.
-Arguments natmap_prf {_} _ : assert.
+Global Arguments NatMap {_} _ _ : assert.
+Global Arguments natmap_car {_} _ : assert.
+Global Arguments natmap_prf {_} _ : assert.
Lemma natmap_eq {A} (m1 m2 : natmap A) :
m1 = m2 ↔ natmap_car m1 = natmap_car m2.
Proof.
@@ -41,8 +41,8 @@ Global Instance natmap_eq_dec `{EqDecision A} : EqDecision (natmap A) := λ m1 m
| right H => right (H ∘ proj1 (natmap_eq m1 m2))
end.
-Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
-Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
+Global Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
+Global Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
let (l,_) := m in mjoin (l !! i).
Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
@@ -90,7 +90,7 @@ Proof.
revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
Qed.
-Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
+Global Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
Lemma natmap_lookup_alter_raw {A} (f : option A → option A) i l :
mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
@@ -144,7 +144,7 @@ Proof.
autorewrite with natmap; auto;
match goal with |- context [?o ≫= _] => by destruct o end.
Qed.
-Instance natmap_merge: Merge natmap := λ A B C f m1 m2,
+Global Instance natmap_merge: Merge natmap := λ A B C f m1 m2,
let (l1, Hl1) := m1 in let (l2, Hl2) := m2 in
NatMap (natmap_merge_raw f l1 l2) (natmap_merge_wf _ _ _ Hl1 Hl2).
@@ -186,7 +186,7 @@ Proof.
revert i. induction l as [|[?|] ? IH]; simpl; try constructor; auto.
rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
Qed.
-Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
+Global Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
let (l,_) := m in natmap_to_list_raw 0 l.
Definition natmap_map_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
@@ -202,7 +202,7 @@ Lemma natmap_lookup_map_raw {A B} (f : A → B) i l :
Proof.
unfold natmap_map_raw. rewrite list_lookup_fmap. by destruct (l !! i).
Qed.
-Instance natmap_map: FMap natmap := λ A B f m,
+Global Instance natmap_map: FMap natmap := λ A B f m,
let (l,Hl) := m in NatMap (natmap_map_raw f l) (natmap_map_wf _ _ Hl).
Instance: FinMap nat natmap.
@@ -256,7 +256,7 @@ Qed.
(** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
Notation natset := (mapset natmap).
-Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
+Global Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
Instance: FinMapDom nat natmap natset := mapset_dom_spec.
(* Fixpoint avoids this definition from being unfolded *)
diff --git a/theories/nmap.v b/theories/nmap.v
index 5d0645bff13c3b1a4fb827beee21665114f742d0..6010831824eef396b23622291c4bb36058db7fea 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -7,41 +7,41 @@ From stdpp Require Import options.
Local Open Scope N_scope.
Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
-Arguments Nmap_0 {_} _ : assert.
-Arguments Nmap_pos {_} _ : assert.
-Arguments NMap {_} _ _ : assert.
+Global Arguments Nmap_0 {_} _ : assert.
+Global Arguments Nmap_pos {_} _ : assert.
+Global Arguments NMap {_} _ _ : assert.
-Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
+Global Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
Proof.
refine (λ t1 t2,
match t1, t2 with
| NMap x t1, NMap y t2 => cast_if_and (decide (x = y)) (decide (t1 = t2))
end); abstract congruence.
Defined.
-Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
+Global Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
Global Opaque Nempty.
-Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
+Global Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
match i with
| N0 => Nmap_0 t
| Npos p => Nmap_pos t !! p
end.
-Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
+Global Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
match i, t with
| N0, NMap o t => NMap (f o) t
| Npos p, NMap o t => NMap o (partial_alter f p t)
end.
-Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
+Global Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
match t with
| NMap o t =>
from_option (λ x, [(0,x)]) [] o ++ (prod_map Npos id <$> map_to_list t)
end.
-Instance Nomap: OMap Nmap := λ A B f t,
+Global Instance Nomap: OMap Nmap := λ A B f t,
match t with NMap o t => NMap (o ≫= f) (omap f t) end.
-Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
+Global Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
match t1, t2 with
| NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
end.
-Instance Nfmap: FMap Nmap := λ A B f t,
+Global Instance Nfmap: FMap Nmap := λ A B f t,
match t with NMap o t => NMap (f <$> o) (f <$> t) end.
Instance: FinMap N Nmap.
@@ -80,5 +80,5 @@ Qed.
(** * Finite sets *)
(** We construct sets of [N]s satisfying extensional equality. *)
Notation Nset := (mapset Nmap).
-Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
+Global Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
diff --git a/theories/numbers.v b/theories/numbers.v
index e18ff11a6af322644f3f9057cd8cc2b4e2622f7d..b936f22b7146e9add16028e4fa08446a0f2c1c53 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -8,12 +8,12 @@ From stdpp Require Import options.
Local Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
-Instance comparison_eq_dec : EqDecision comparison.
+Global Instance comparison_eq_dec : EqDecision comparison.
Proof. solve_decision. Defined.
(** * Notations and properties of [nat] *)
-Arguments minus !_ !_ / : assert.
-Arguments Nat.max : simpl nomatch.
+Global Arguments minus !_ !_ / : assert.
+Global Arguments Nat.max : simpl nomatch.
Typeclasses Opaque lt.
@@ -37,18 +37,18 @@ Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
-Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
-Instance nat_le_dec: RelDecision le := le_dec.
-Instance nat_lt_dec: RelDecision lt := lt_dec.
-Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Instance S_inj: Inj (=) (=) S.
+Global Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
+Global Instance nat_le_dec: RelDecision le := le_dec.
+Global Instance nat_lt_dec: RelDecision lt := lt_dec.
+Global Instance nat_inhabited: Inhabited nat := populate 0%nat.
+Global Instance S_inj: Inj (=) (=) S.
Proof. by injection 1. Qed.
-Instance nat_le_po: PartialOrder (≤).
+Global Instance nat_le_po: PartialOrder (≤).
Proof. repeat split; repeat intro; auto with lia. Qed.
-Instance nat_le_total: Total (≤).
+Global Instance nat_le_total: Total (≤).
Proof. repeat intro; lia. Qed.
-Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
+Global Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
Proof.
assert (∀ x y (p : x ≤ y) y' (q : x ≤ y'),
y = y' → eq_dep nat (le x) y p y' q) as aux.
@@ -60,7 +60,7 @@ Proof.
intros x y p q.
by apply (Eqdep_dec.eq_dep_eq_dec (λ x y, decide (x = y))), aux.
Qed.
-Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
+Global Instance nat_lt_pi: ∀ x y : nat, ProofIrrel (x < y).
Proof. unfold lt. apply _. Qed.
Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z.
@@ -81,7 +81,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
-Instance Nat_divide_dec : RelDecision Nat.divide.
+Global Instance Nat_divide_dec : RelDecision Nat.divide.
Proof.
refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
Defined.
@@ -122,24 +122,24 @@ Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.
-Arguments Pos.of_nat : simpl never.
-Arguments Pmult : simpl never.
+Global Arguments Pos.of_nat : simpl never.
+Global Arguments Pmult : simpl never.
-Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
-Instance positive_le_dec: RelDecision Pos.le.
+Global Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
+Global Instance positive_le_dec: RelDecision Pos.le.
Proof. refine (λ x y, decide ((x ?= y) ≠Gt)). Defined.
-Instance positive_lt_dec: RelDecision Pos.lt.
+Global Instance positive_lt_dec: RelDecision Pos.lt.
Proof. refine (λ x y, decide ((x ?= y) = Lt)). Defined.
-Instance positive_le_total: Total Pos.le.
+Global Instance positive_le_total: Total Pos.le.
Proof. repeat intro; lia. Qed.
-Instance positive_inhabited: Inhabited positive := populate 1.
+Global Instance positive_inhabited: Inhabited positive := populate 1.
-Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
-Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
-Instance xO_inj : Inj (=) (=) (~0).
+Global Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
+Global Instance maybe_xI : Maybe xI := λ p, match p with p~1 => Some p | _ => None end.
+Global Instance xO_inj : Inj (=) (=) (~0).
Proof. by injection 1. Qed.
-Instance xI_inj : Inj (=) (=) (~1).
+Global Instance xI_inj : Inj (=) (=) (~1).
Proof. by injection 1. Qed.
(** Since [positive] represents lists of bits, we define list operations
@@ -199,7 +199,7 @@ Proof.
- reflexivity.
Qed.
-Instance Preverse_inj : Inj (=) (=) Preverse.
+Global Instance Preverse_inj : Inj (=) (=) Preverse.
Proof.
intros p q eq.
rewrite <- (Preverse_involutive p).
@@ -248,7 +248,7 @@ Proof.
- reflexivity.
Qed.
-Instance Pdup_inj : Inj (=) (=) Pdup.
+Global Instance Pdup_inj : Inj (=) (=) Pdup.
Proof.
intros p q eq.
apply (Pdup_suffix_eq _ _ 1 1).
@@ -291,27 +291,27 @@ Infix "`mod`" := N.modulo (at level 35) : N_scope.
Infix "`max`" := N.max (at level 35) : N_scope.
Infix "`min`" := N.min (at level 35) : N_scope.
-Arguments N.add : simpl never.
+Global Arguments N.add : simpl never.
-Instance Npos_inj : Inj (=) (=) Npos.
+Global Instance Npos_inj : Inj (=) (=) Npos.
Proof. by injection 1. Qed.
-Instance N_eq_dec: EqDecision N := N.eq_dec.
+Global Instance N_eq_dec: EqDecision N := N.eq_dec.
Program Instance N_le_dec : RelDecision N.le := λ x y,
match N.compare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
Program Instance N_lt_dec : RelDecision N.lt := λ x y,
match N.compare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
-Instance N_inhabited: Inhabited N := populate 1%N.
-Instance N_lt_pi x y : ProofIrrel (x < y)%N.
+Global Instance N_inhabited: Inhabited N := populate 1%N.
+Global Instance N_lt_pi x y : ProofIrrel (x < y)%N.
Proof. unfold N.lt. apply _. Qed.
-Instance N_le_po: PartialOrder (≤)%N.
+Global Instance N_le_po: PartialOrder (≤)%N.
Proof.
repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
Qed.
-Instance N_le_total: Total (≤)%N.
+Global Instance N_le_total: Total (≤)%N.
Proof. repeat intro; lia. Qed.
Global Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
@@ -340,28 +340,28 @@ Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Infix "`max`" := Z.max (at level 35) : Z_scope.
Infix "`min`" := Z.min (at level 35) : Z_scope.
-Instance Zpos_inj : Inj (=) (=) Zpos.
+Global Instance Zpos_inj : Inj (=) (=) Zpos.
Proof. by injection 1. Qed.
-Instance Zneg_inj : Inj (=) (=) Zneg.
+Global Instance Zneg_inj : Inj (=) (=) Zneg.
Proof. by injection 1. Qed.
-Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
+Global Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.
-Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
-Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
-Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
-Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
-Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
-Instance Z_inhabited: Inhabited Z := populate 1.
-Instance Z_lt_pi x y : ProofIrrel (x < y).
+Global Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
+Global Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
+Global Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
+Global Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
+Global Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
+Global Instance Z_inhabited: Inhabited Z := populate 1.
+Global Instance Z_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Z.lt. apply _. Qed.
-Instance Z_le_po : PartialOrder (≤).
+Global Instance Z_le_po : PartialOrder (≤).
Proof.
repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
Qed.
-Instance Z_le_total: Total Z.le.
+Global Instance Z_le_total: Total Z.le.
Proof. repeat intro; lia. Qed.
Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
@@ -377,31 +377,31 @@ Proof.
trans x; auto. apply Z.quot_lt; lia.
Qed.
-Arguments Z.pred : simpl never.
-Arguments Z.succ : simpl never.
-Arguments Z.of_nat : simpl never.
-Arguments Z.to_nat : simpl never.
-Arguments Z.mul : simpl never.
-Arguments Z.add : simpl never.
-Arguments Z.sub : simpl never.
-Arguments Z.opp : simpl never.
-Arguments Z.pow : simpl never.
-Arguments Z.div : simpl never.
-Arguments Z.modulo : simpl never.
-Arguments Z.quot : simpl never.
-Arguments Z.rem : simpl never.
-Arguments Z.shiftl : simpl never.
-Arguments Z.shiftr : simpl never.
-Arguments Z.gcd : simpl never.
-Arguments Z.lcm : simpl never.
-Arguments Z.min : simpl never.
-Arguments Z.max : simpl never.
-Arguments Z.lor : simpl never.
-Arguments Z.land : simpl never.
-Arguments Z.lxor : simpl never.
-Arguments Z.lnot : simpl never.
-Arguments Z.square : simpl never.
-Arguments Z.abs : simpl never.
+Global Arguments Z.pred : simpl never.
+Global Arguments Z.succ : simpl never.
+Global Arguments Z.of_nat : simpl never.
+Global Arguments Z.to_nat : simpl never.
+Global Arguments Z.mul : simpl never.
+Global Arguments Z.add : simpl never.
+Global Arguments Z.sub : simpl never.
+Global Arguments Z.opp : simpl never.
+Global Arguments Z.pow : simpl never.
+Global Arguments Z.div : simpl never.
+Global Arguments Z.modulo : simpl never.
+Global Arguments Z.quot : simpl never.
+Global Arguments Z.rem : simpl never.
+Global Arguments Z.shiftl : simpl never.
+Global Arguments Z.shiftr : simpl never.
+Global Arguments Z.gcd : simpl never.
+Global Arguments Z.lcm : simpl never.
+Global Arguments Z.min : simpl never.
+Global Arguments Z.max : simpl never.
+Global Arguments Z.lor : simpl never.
+Global Arguments Z.land : simpl never.
+Global Arguments Z.lxor : simpl never.
+Global Arguments Z.lnot : simpl never.
+Global Arguments Z.square : simpl never.
+Global Arguments Z.abs : simpl never.
Lemma Z_to_nat_neq_0_pos x : Z.to_nat x ≠0%nat → 0 < x.
Proof. by destruct x. Qed.
@@ -483,11 +483,11 @@ Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
Local Close Scope Z_scope.
(** * Injectivity of casts *)
-Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
-Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
-Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
-Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
-Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
+Global Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
+Global Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
+Global Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
+Global Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
+Global Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
(* Add others here. *)
(** * Notations and properties of [Qc] *)
@@ -510,9 +510,9 @@ Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.
Global Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core.
-Arguments Qred : simpl never.
+Global Arguments Qred : simpl never.
-Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
+Global Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
if Qclt_le_dec y x then right _ else left _.
Next Obligation. intros x y; apply Qclt_not_le. Qed.
@@ -521,19 +521,19 @@ Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
if Qclt_le_dec x y then left _ else right _.
Next Obligation. done. Qed.
Next Obligation. intros x y; apply Qcle_not_lt. Qed.
-Instance Qc_lt_pi x y : ProofIrrel (x < y).
+Global Instance Qc_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Qclt. apply _. Qed.
-Instance Qc_le_po: PartialOrder (≤).
+Global Instance Qc_le_po: PartialOrder (≤).
Proof.
repeat split; red; [apply Qcle_refl | apply Qcle_trans | apply Qcle_antisym].
Qed.
-Instance Qc_lt_strict: StrictOrder (<).
+Global Instance Qc_lt_strict: StrictOrder (<).
Proof.
split; red; [|apply Qclt_trans].
intros x Hx. by destruct (Qclt_not_eq x x).
Qed.
-Instance Qc_le_total: Total Qcle.
+Global Instance Qc_le_total: Total Qcle.
Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.
Lemma Qcmult_0_l x : 0 * x = 0.
@@ -560,15 +560,15 @@ Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
-Instance Qcopp_inj : Inj (=) (=) Qcopp.
+Global Instance Qcopp_inj : Inj (=) (=) Qcopp.
Proof.
intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
-Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
+Global Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
Proof.
intros x y H. by apply (anti_symm (≤));rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
-Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
+Global Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
Proof.
intros x y H. by apply (anti_symm (≤)); rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
@@ -670,7 +670,7 @@ Delimit Scope Qp_scope with Qp.
Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
Add Printing Constructor Qp.
Bind Scope Qp_scope with Qp.
-Arguments Qp_to_Qc _%Qp : assert.
+Global Arguments Qp_to_Qc _%Qp : assert.
Local Open Scope Qp_scope.
@@ -679,7 +679,7 @@ Proof.
split; [|by intros ->].
destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
Qed.
-Instance Qp_eq_dec : EqDecision Qp.
+Global Instance Qp_eq_dec : EqDecision Qp.
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
by rewrite <-Qp_to_Qc_inj_iff.
@@ -688,27 +688,27 @@ Defined.
Definition Qp_add (p q : Qp) : Qp :=
let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
-Arguments Qp_add : simpl never.
+Global Arguments Qp_add : simpl never.
Definition Qp_sub (p q : Qp) : option Qp :=
let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
let pq := (p - q)%Qc in
guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq).
-Arguments Qp_sub : simpl never.
+Global Arguments Qp_sub : simpl never.
Definition Qp_mul (p q : Qp) : Qp :=
let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
-Arguments Qp_mul : simpl never.
+Global Arguments Qp_mul : simpl never.
Definition Qp_inv (q : Qp) : Qp :=
let 'mk_Qp q Hq := q return _ in
mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
-Arguments Qp_inv : simpl never.
+Global Arguments Qp_inv : simpl never.
Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q).
Typeclasses Opaque Qp_div.
-Arguments Qp_div : simpl never.
+Global Arguments Qp_div : simpl never.
Infix "+" := Qp_add : Qp_scope.
Infix "-" := Qp_sub : Qp_scope.
@@ -718,7 +718,7 @@ Infix "/" := Qp_div : Qp_scope.
Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Z.pos n) _.
Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
-Arguments pos_to_Qp : simpl never.
+Global Arguments pos_to_Qp : simpl never.
Notation "1" := (pos_to_Qp 1) : Qp_scope.
Notation "2" := (pos_to_Qp 2) : Qp_scope.
@@ -747,17 +747,17 @@ Proof. by destruct p, q. Qed.
Lemma Qp_to_Qc_inj_lt p q : p < q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
Proof. by destruct p, q. Qed.
-Instance Qp_le_dec : RelDecision (≤).
+Global Instance Qp_le_dec : RelDecision (≤).
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
by rewrite Qp_to_Qc_inj_le.
Qed.
-Instance Qp_lt_dec : RelDecision (<).
+Global Instance Qp_lt_dec : RelDecision (<).
Proof.
refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
by rewrite Qp_to_Qc_inj_lt.
Qed.
-Instance Qp_lt_pi p q : ProofIrrel (p < q).
+Global Instance Qp_lt_pi p q : ProofIrrel (p < q).
Proof. destruct p, q; apply _. Qed.
Definition Qp_max (q p : Qp) : Qp := if decide (q ≤ p) then p else q.
@@ -766,34 +766,34 @@ Definition Qp_min (q p : Qp) : Qp := if decide (q ≤ p) then q else p.
Infix "`max`" := Qp_max : Qp_scope.
Infix "`min`" := Qp_min : Qp_scope.
-Instance Qp_inhabited : Inhabited Qp := populate 1.
+Global Instance Qp_inhabited : Inhabited Qp := populate 1.
-Instance Qp_add_assoc : Assoc (=) Qp_add.
+Global Instance Qp_add_assoc : Assoc (=) Qp_add.
Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed.
-Instance Qp_add_comm : Comm (=) Qp_add.
+Global Instance Qp_add_comm : Comm (=) Qp_add.
Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed.
-Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p).
+Global Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p).
Proof.
destruct p as [p ?].
intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
Qed.
-Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p).
+Global Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p).
Proof.
destruct p as [p ?].
intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
Qed.
-Instance Qp_mul_assoc : Assoc (=) Qp_mul.
+Global Instance Qp_mul_assoc : Assoc (=) Qp_mul.
Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed.
-Instance Qp_mul_comm : Comm (=) Qp_mul.
+Global Instance Qp_mul_comm : Comm (=) Qp_mul.
Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed.
-Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
+Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p).
Proof.
destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl.
intros Hpq.
apply (anti_symm _); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
Qed.
-Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
+Global Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p).
Proof.
intros q1 q2 Hpq. apply (inj (Qp_mul p)). by rewrite !(comm_L Qp_mul p).
Qed.
@@ -830,7 +830,7 @@ Proof.
rewrite <-(Qp_mul_1_l (/ /p)), <-(Qp_mul_inv_r p), <-(assoc_L _).
by rewrite Qp_mul_inv_r, Qp_mul_1_r.
Qed.
-Instance Qp_inv_inj : Inj (=) (=) Qp_inv.
+Global Instance Qp_inv_inj : Inj (=) (=) Qp_inv.
Proof.
intros p1 p2 Hp. apply (inj (Qp_mul (/p1))).
by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l.
@@ -876,25 +876,25 @@ Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed.
Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
Proof. apply (bool_decide_unpack _); by compute. Qed.
-Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
+Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p).
Proof. unfold Qp_div; apply _. Qed.
-Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
+Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
Proof. unfold Qp_div; apply _. Qed.
-Instance Qp_le_po : PartialOrder (≤)%Qp.
+Global Instance Qp_le_po : PartialOrder (≤)%Qp.
Proof.
split; [split|].
- intros p. by apply Qp_to_Qc_inj_le.
- intros p q r. rewrite !Qp_to_Qc_inj_le. by etrans.
- intros p q. rewrite !Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. apply Qcle_antisym.
Qed.
-Instance Qp_lt_strict : StrictOrder (<)%Qp.
+Global Instance Qp_lt_strict : StrictOrder (<)%Qp.
Proof.
split.
- intros p ?%Qp_to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)).
- intros p q r. rewrite !Qp_to_Qc_inj_lt. by etrans.
Qed.
-Instance Qp_le_total: Total (≤)%Qp.
+Global Instance Qp_le_total: Total (≤)%Qp.
Proof. intros p q. rewrite !Qp_to_Qc_inj_le. apply (total Qcle). Qed.
Lemma Qp_lt_le_incl p q : p < q → p ≤ q.
@@ -1096,14 +1096,14 @@ Qed.
Lemma Qp_max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_incl?]|]; [left|right]; done. Qed.
-Instance Qp_max_assoc : Assoc (=) Qp_max.
+Global Instance Qp_max_assoc : Assoc (=) Qp_max.
Proof.
intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o));
try by rewrite ?decide_True by (by etrans).
rewrite decide_False by done.
by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
Qed.
-Instance Qp_max_comm : Comm (=) Qp_max.
+Global Instance Qp_max_comm : Comm (=) Qp_max.
Proof.
intros q p.
destruct (Qp_max_spec_le q p) as [[?->]|[?->]],
@@ -1139,14 +1139,14 @@ Qed.
Lemma Qp_min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_incl ?]|]; [left|right]; done. Qed.
-Instance Qp_min_assoc : Assoc (=) Qp_min.
+Global Instance Qp_min_assoc : Assoc (=) Qp_min.
Proof.
intros q p o. unfold Qp_min.
destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
- by rewrite !decide_True by (by etrans).
- by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge).
Qed.
-Instance Qp_min_comm : Comm (=) Qp_min.
+Global Instance Qp_min_comm : Comm (=) Qp_min.
Proof.
intros q p.
destruct (Qp_min_spec_le q p) as [[?->]|[?->]],
diff --git a/theories/option.v b/theories/option.v
index f2eed50fc86ad65a0e92354119a4fe1899398afc..13de994cee7ef9cc060e4084ea8b4d7a27b75a22 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -15,14 +15,14 @@ Lemma Some_ne_None {A} (x : A) : Some x ≠None.
Proof. congruence. Qed.
Lemma eq_None_ne_Some {A} (mx : option A) x : mx = None → mx ≠Some x.
Proof. congruence. Qed.
-Instance Some_inj {A} : Inj (=) (=) (@Some A).
+Global Instance Some_inj {A} : Inj (=) (=) (@Some A).
Proof. congruence. Qed.
(** The [from_option] is the eliminator for option. *)
Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end.
Instance: Params (@from_option) 3 := {}.
-Arguments from_option {_ _} _ _ !_ / : assert.
+Global Arguments from_option {_ _} _ _ !_ / : assert.
(** The eliminator with the identity function. *)
Notation default := (from_option id).
@@ -56,7 +56,7 @@ Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
Lemma not_eq_None_Some {A} (mx : option A) : mx ≠None ↔ is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
-Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
+Global Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
Proof.
set (P (mx : option A) := match mx with Some _ => True | _ => False end).
set (f mx := match mx return P mx → is_Some mx with
@@ -67,7 +67,7 @@ Proof.
intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Qed.
-Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
+Global Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx) :=
match mx with
| Some x => left (ex_intro _ x eq_refl)
| None => right is_Some_None
@@ -109,7 +109,7 @@ Section Forall2.
End Forall2.
(** Setoids *)
-Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡).
+Global Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡).
Section setoids.
Context `{Equiv A}.
@@ -152,11 +152,11 @@ End setoids.
Typeclasses Opaque option_equiv.
(** Equality on [option] is decidable. *)
-Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
+Global Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
-Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
+Global Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
-Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
+Global Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
Proof.
refine (λ mx my,
match mx, my with
@@ -166,13 +166,13 @@ Proof.
Defined.
(** * Monadic operations *)
-Instance option_ret: MRet option := @Some.
-Instance option_bind: MBind option := λ A B f mx,
+Global Instance option_ret: MRet option := @Some.
+Global Instance option_bind: MBind option := λ A B f mx,
match mx with Some x => f x | None => None end.
-Instance option_join: MJoin option := λ A mmx,
+Global Instance option_join: MJoin option := λ A mmx,
match mmx with Some mx => mx | None => None end.
-Instance option_fmap: FMap option := @option_map.
-Instance option_guard: MGuard option := λ P dec A f,
+Global Instance option_fmap: FMap option := @option_map.
+Global Instance option_guard: MGuard option := λ P dec A f,
match dec with left H => f H | _ => None end.
Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
@@ -234,13 +234,13 @@ Proof. destruct mx; naive_solver. Qed.
Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
Proof. by destruct mx. Qed.
-Instance option_fmap_proper `{Equiv A, Equiv B} :
+Global Instance option_fmap_proper `{Equiv A, Equiv B} :
Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) fmap.
Proof. destruct 2; constructor; auto. Qed.
-Instance option_mbind_proper `{Equiv A, Equiv B} :
+Global Instance option_mbind_proper `{Equiv A, Equiv B} :
Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) mbind.
Proof. destruct 2; simpl; try constructor; auto. Qed.
-Instance option_mjoin_proper `{Equiv A} :
+Global Instance option_mjoin_proper `{Equiv A} :
Proper ((≡) ==> (≡@{option (option A)})) mjoin.
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
@@ -249,45 +249,45 @@ Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
not particularly like type level reductions. *)
Class Maybe {A B : Type} (c : A → B) :=
maybe : B → option A.
-Arguments maybe {_ _} _ {_} !_ / : assert.
+Global Arguments maybe {_ _} _ {_} !_ / : assert.
Class Maybe2 {A1 A2 B : Type} (c : A1 → A2 → B) :=
maybe2 : B → option (A1 * A2).
-Arguments maybe2 {_ _ _} _ {_} !_ / : assert.
+Global Arguments maybe2 {_ _ _} _ {_} !_ / : assert.
Class Maybe3 {A1 A2 A3 B : Type} (c : A1 → A2 → A3 → B) :=
maybe3 : B → option (A1 * A2 * A3).
-Arguments maybe3 {_ _ _ _} _ {_} !_ / : assert.
+Global Arguments maybe3 {_ _ _ _} _ {_} !_ / : assert.
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 → A2 → A3 → A4 → B) :=
maybe4 : B → option (A1 * A2 * A3 * A4).
-Arguments maybe4 {_ _ _ _ _} _ {_} !_ / : assert.
+Global Arguments maybe4 {_ _ _ _ _} _ {_} !_ / : assert.
-Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 ∘ c2) := λ x,
+Global Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 ∘ c2) := λ x,
maybe c1 x ≫= maybe c2.
-Arguments maybe_comp _ _ _ _ _ _ _ !_ / : assert.
+Global Arguments maybe_comp _ _ _ _ _ _ _ !_ / : assert.
-Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
+Global Instance maybe_inl {A B} : Maybe (@inl A B) := λ xy,
match xy with inl x => Some x | _ => None end.
-Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
+Global Instance maybe_inr {A B} : Maybe (@inr A B) := λ xy,
match xy with inr y => Some y | _ => None end.
-Instance maybe_Some {A} : Maybe (@Some A) := id.
-Arguments maybe_Some _ !_ / : assert.
+Global Instance maybe_Some {A} : Maybe (@Some A) := id.
+Global Arguments maybe_Some _ !_ / : assert.
(** * Union, intersection and difference *)
-Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
+Global Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
match mx, my with
| Some x, Some y => f x y
| Some x, None => Some x
| None, Some y => Some y
| None, None => None
end.
-Instance option_intersection_with {A} : IntersectionWith A (option A) :=
+Global Instance option_intersection_with {A} : IntersectionWith A (option A) :=
λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
-Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
+Global Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
match mx, my with
| Some x, Some y => f x y
| Some x, None => Some x
| None, _ => None
end.
-Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
+Global Instance option_union {A} : Union (option A) := union_with (λ x _, Some x).
Lemma option_union_Some {A} (mx my : option A) z :
mx ∪ my = Some z → mx = Some z ∨ my = Some z.
diff --git a/theories/pmap.v b/theories/pmap.v
index d89ef60b3f0e5f77cedf9c7bb492bf6aff2525a6..f4a185a52bacce7e19687c9d42ed189a46b5f096 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -22,10 +22,10 @@ all nodes. *)
Inductive Pmap_raw (A : Type) : Type :=
| PLeaf: Pmap_raw A
| PNode: option A → Pmap_raw A → Pmap_raw A → Pmap_raw A.
-Arguments PLeaf {_} : assert.
-Arguments PNode {_} _ _ _ : assert.
+Global Arguments PLeaf {_} : assert.
+Global Arguments PNode {_} _ _ _ : assert.
-Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
+Global Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
Proof. solve_decision. Defined.
Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
@@ -34,7 +34,7 @@ Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
| PNode None PLeaf PLeaf => false
| PNode _ l r => Pmap_wf l && Pmap_wf r
end.
-Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
+Global Arguments Pmap_wf _ !_ / : simpl nomatch, assert.
Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf l.
Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf r.
@@ -42,15 +42,15 @@ Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
Local Hint Immediate Pmap_wf_l Pmap_wf_r : core.
Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
-Arguments PNode' : simpl never.
+Global Arguments PNode' : simpl never.
Lemma PNode_wf {A} o (l r : Pmap_raw A) :
Pmap_wf l → Pmap_wf r → Pmap_wf (PNode' o l r).
Proof. destruct o, l, r; simpl; auto. Qed.
Local Hint Resolve PNode_wf : core.
(** Operations *)
-Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
+Global Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
+Global Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
let _ : Lookup _ _ _ := @go in
match t with
@@ -256,33 +256,33 @@ Qed.
(** Packed version and instance of the finite map type class *)
Inductive Pmap (A : Type) : Type :=
PMap { pmap_car : Pmap_raw A; pmap_prf : Pmap_wf pmap_car }.
-Arguments PMap {_} _ _ : assert.
-Arguments pmap_car {_} _ : assert.
-Arguments pmap_prf {_} _ : assert.
+Global Arguments PMap {_} _ _ : assert.
+Global Arguments pmap_car {_} _ : assert.
+Global Arguments pmap_prf {_} _ : assert.
Lemma Pmap_eq {A} (m1 m2 : Pmap A) : m1 = m2 ↔ pmap_car m1 = pmap_car m2.
Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
simplify_eq/=; f_equal; apply proof_irrel.
Qed.
-Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
+Global Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
| left H => left (proj2 (Pmap_eq m1 m2) H)
| right H => right (H ∘ proj1 (Pmap_eq m1 m2))
end.
-Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
-Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
-Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
+Global Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
+Global Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
+Global Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
-Instance Pfmap : FMap Pmap := λ A B f m,
+Global Instance Pfmap : FMap Pmap := λ A B f m,
let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
let (t,Ht) := m in Pto_list_raw 1 t [].
-Instance Pomap : OMap Pmap := λ A B f m,
+Global Instance Pomap : OMap Pmap := λ A B f m,
let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
-Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
+Global Instance Pmerge : Merge Pmap := λ A B C f m1 m2,
let (t1,Ht1) := m1 in let (t2,Ht2) := m2 in PMap _ (Pmerge_wf f _ _ Ht1 Ht2).
-Instance Pmap_finmap : FinMap positive Pmap.
+Global Instance Pmap_finmap : FinMap positive Pmap.
Proof.
split.
- by intros ? [t1 ?] [t2 ?] ?; apply Pmap_eq, Pmap_wf_eq.
@@ -312,5 +312,5 @@ Qed.
(** * Finite sets *)
(** We construct sets of [positives]s satisfying extensional equality. *)
Notation Pset := (mapset Pmap).
-Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
-Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
+Global Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
+Global Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
diff --git a/theories/pretty.v b/theories/pretty.v
index d23c7b4bdb7d90eee4fa173718c77cbc54b2d00b..7ba38b338b0d71004c7944b7fe69a25f9ab6ddaa 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -24,7 +24,7 @@ Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
end.
Definition pretty_N_go (x : N) : string → string :=
pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
-Instance pretty_N : Pretty N := λ x,
+Global Instance pretty_N : Pretty N := λ x,
if decide (x = 0)%N then "0" else pretty_N_go x "".
Lemma pretty_N_go_0 s : pretty_N_go 0 s = s.
@@ -70,7 +70,7 @@ Proof.
unfold pretty_N_char. by repeat case_match.
Qed.
-Instance pretty_N_inj : Inj (=@{N}) (=) pretty.
+Global Instance pretty_N_inj : Inj (=@{N}) (=) pretty.
Proof.
cut (∀ x y s s', pretty_N_go x s = pretty_N_go y s' →
String.length s = String.length s' → x = y ∧ s = s').
@@ -99,19 +99,19 @@ Proof.
rewrite (N.div_mod x 10), (N.div_mod y 10) by done. lia.
Qed.
-Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
-Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
+Global Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
+Global Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
Proof. apply _. Qed.
-Instance pretty_positive : Pretty positive := λ x, pretty (Npos x).
-Instance pretty_positive_inj : Inj (=@{positive}) (=) pretty.
+Global Instance pretty_positive : Pretty positive := λ x, pretty (Npos x).
+Global Instance pretty_positive_inj : Inj (=@{positive}) (=) pretty.
Proof. apply _. Qed.
-Instance pretty_Z : Pretty Z := λ x,
+Global Instance pretty_Z : Pretty Z := λ x,
match x with
| Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
end%string.
-Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
+Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
Proof.
unfold pretty, pretty_Z.
intros [|x|x] [|y|y] Hpretty; simplify_eq/=; try done.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index b972df7448d670c57da014577ac78dd19f8b1436..1f6074424bd4f0312d997eb2ab90860bfcb5184d 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -4,19 +4,19 @@ From stdpp Require Import options.
Global Hint Extern 200 (ProofIrrel _) => progress (lazy beta) : typeclass_instances.
-Instance True_pi: ProofIrrel True.
+Global Instance True_pi: ProofIrrel True.
Proof. intros [] []; reflexivity. Qed.
-Instance False_pi: ProofIrrel False.
+Global Instance False_pi: ProofIrrel False.
Proof. intros []. Qed.
-Instance unit_pi: ProofIrrel ().
+Global Instance unit_pi: ProofIrrel ().
Proof. intros [] []; reflexivity. Qed.
-Instance and_pi (A B : Prop) :
+Global Instance and_pi (A B : Prop) :
ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
-Instance prod_pi (A B : Type) :
+Global Instance prod_pi (A B : Type) :
ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
Proof. intros ?? [??] [??]. f_equal; trivial. Qed.
-Instance eq_pi {A} (x : A) `{∀ z, Decision (x = z)} (y : A) :
+Global Instance eq_pi {A} (x : A) `{∀ z, Decision (x = z)} (y : A) :
ProofIrrel (x = y).
Proof.
set (f z (H : x = z) :=
@@ -29,7 +29,7 @@ Proof.
intros p q. rewrite <-(help _ p), <-(help _ q).
unfold f at 2 4. destruct (decide _); [reflexivity|]. exfalso; tauto.
Qed.
-Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
+Global Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
Proof. destruct b; simpl; apply _. Qed.
Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
(x y : sig P) : x = y ↔ `x = `y.
@@ -38,7 +38,7 @@ Proof.
destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
f_equal. apply proof_irrel.
Qed.
-Instance proj1_sig_inj `(P : A → Prop) `{∀ x, ProofIrrel (P x)} :
+Global Instance proj1_sig_inj `(P : A → Prop) `{∀ x, ProofIrrel (P x)} :
Inj (=) (=) (proj1_sig (P:=P)).
Proof. intros ??. apply (sig_eq_pi P). Qed.
Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
diff --git a/theories/propset.v b/theories/propset.v
index 84367c5691d1e6eb9cb63fa24d5d779d96836094..1ed3af52c216d25065133279d39c7b2481216f68 100644
--- a/theories/propset.v
+++ b/theories/propset.v
@@ -4,22 +4,22 @@ From stdpp Require Import options.
Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
Add Printing Constructor propset.
-Arguments PropSet {_} _ : assert.
-Arguments propset_car {_} _ _ : assert.
+Global Arguments PropSet {_} _ : assert.
+Global Arguments propset_car {_} _ _ : assert.
Notation "{[ x | P ]}" := (PropSet (λ x, P))
(at level 1, format "{[ x | P ]}") : stdpp_scope.
-Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
+Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
-Instance propset_top {A} : Top (propset A) := {[ _ | True ]}.
-Instance propset_empty {A} : Empty (propset A) := {[ _ | False ]}.
-Instance propset_singleton {A} : Singleton A (propset A) := λ y, {[ x | y = x ]}.
-Instance propset_union {A} : Union (propset A) := λ X1 X2, {[ x | x ∈ X1 ∨ x ∈ X2 ]}.
-Instance propset_intersection {A} : Intersection (propset A) := λ X1 X2,
+Global Instance propset_top {A} : Top (propset A) := {[ _ | True ]}.
+Global Instance propset_empty {A} : Empty (propset A) := {[ _ | False ]}.
+Global Instance propset_singleton {A} : Singleton A (propset A) := λ y, {[ x | y = x ]}.
+Global Instance propset_union {A} : Union (propset A) := λ X1 X2, {[ x | x ∈ X1 ∨ x ∈ X2 ]}.
+Global Instance propset_intersection {A} : Intersection (propset A) := λ X1 X2,
{[ x | x ∈ X1 ∧ x ∈ X2 ]}.
-Instance propset_difference {A} : Difference (propset A) := λ X1 X2,
+Global Instance propset_difference {A} : Difference (propset A) := λ X1 X2,
{[ x | x ∈ X1 ∧ x ∉ X2 ]}.
-Instance propset_top_set {A} : TopSet A (propset A).
+Global Instance propset_top_set {A} : TopSet A (propset A).
Proof. split; [split; [split| |]|]; by repeat intro. Qed.
Lemma elem_of_PropSet {A} (P : A → Prop) x : x ∈ {[ x | P x ]} ↔ P x.
@@ -33,17 +33,17 @@ Lemma elem_of_set_to_propset `{SemiSet A C} x (X : C) :
x ∈ set_to_propset X ↔ x ∈ X.
Proof. done. Qed.
-Instance propset_ret : MRet propset := λ A (x : A), {[ x ]}.
-Instance propset_bind : MBind propset := λ A B (f : A → propset B) (X : propset A),
+Global Instance propset_ret : MRet propset := λ A (x : A), {[ x ]}.
+Global Instance propset_bind : MBind propset := λ A B (f : A → propset B) (X : propset A),
PropSet (λ b, ∃ a, b ∈ f a ∧ a ∈ X).
-Instance propset_fmap : FMap propset := λ A B (f : A → B) (X : propset A),
+Global Instance propset_fmap : FMap propset := λ A B (f : A → B) (X : propset A),
{[ b | ∃ a, b = f a ∧ a ∈ X ]}.
-Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
+Global Instance propset_join : MJoin propset := λ A (XX : propset (propset A)),
{[ a | ∃ X : propset A, a ∈ X ∧ X ∈ XX ]}.
-Instance propset_monad_set : MonadSet propset.
+Global Instance propset_monad_set : MonadSet propset.
Proof. by split; try apply _. Qed.
-Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
+Global Instance set_unfold_PropSet {A} (P : A → Prop) x Q :
SetUnfoldSimpl (P x) Q → SetUnfoldElemOf x (PropSet P) Q.
Proof. intros HPQ. constructor. apply HPQ. Qed.
diff --git a/theories/relations.v b/theories/relations.v
index 81737ed495012993dd8bd1764db78ef5637ed3a1..46b8d580bdc4f7941afe92a8697e7e7ab9dcb1bc 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -81,7 +81,7 @@ Global Hint Unfold nf red : core.
Section closure.
Context `{R : relation A}.
- Hint Constructors rtc nsteps bsteps tc : core.
+ Local Hint Constructors rtc nsteps bsteps tc : core.
Lemma rtc_transitive x y z : rtc R x y → rtc R y z → rtc R x z.
Proof. induction 1; eauto. Qed.
@@ -271,7 +271,7 @@ End more_closure.
Section properties.
Context `{R : relation A}.
- Hint Constructors rtc nsteps bsteps tc : core.
+ Local Hint Constructors rtc nsteps bsteps tc : core.
Lemma nf_wn x : nf R x → wn R x.
Proof. intros. exists x; eauto. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index e16de487227d8b0a4d9a4274784cfd31f9f89350..7b820ee7d1adb8f2b5421a9c0e9cea77416d0c72 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -11,11 +11,11 @@ Unset Default Proof Using.
(* Higher precedence to make sure these instances are not used for other types
with an [ElemOf] instance, such as lists. *)
-Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
+Global Instance set_equiv `{ElemOf A C} : Equiv C | 20 := λ X Y,
∀ x, x ∈ X ↔ x ∈ Y.
-Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
+Global Instance set_subseteq `{ElemOf A C} : SubsetEq C | 20 := λ X Y,
∀ x, x ∈ X → x ∈ Y.
-Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
+Global Instance set_disjoint `{ElemOf A C} : Disjoint C | 20 := λ X Y,
∀ x, x ∈ X → x ∈ Y → False.
Typeclasses Opaque set_equiv set_subseteq set_disjoint.
@@ -95,27 +95,27 @@ This transformation is implemented using type classes instead of setoid
rewriting to ensure that we traverse each term at most once and to be able to
deal with occurences of the set operations under binders. *)
Class SetUnfold (P Q : Prop) := { set_unfold : P ↔ Q }.
-Arguments set_unfold _ _ {_} : assert.
+Global Arguments set_unfold _ _ {_} : assert.
Global Hint Mode SetUnfold + - : typeclass_instances.
(** The class [SetUnfoldElemOf] is a more specialized version of [SetUnfold]
for propositions of the shape [x ∈ X] to improve performance. *)
Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
{ set_unfold_elem_of : x ∈ X ↔ Q }.
-Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
+Global Arguments set_unfold_elem_of {_ _ _} _ _ _ {_} : assert.
Global Hint Mode SetUnfoldElemOf + + + - + - : typeclass_instances.
-Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
+Global Instance set_unfold_elem_of_default `{ElemOf A C} (x : A) (X : C) :
SetUnfoldElemOf x X (x ∈ X) | 1000.
Proof. done. Qed.
-Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
+Global Instance set_unfold_elem_of_set_unfold `{ElemOf A C} (x : A) (X : C) Q :
SetUnfoldElemOf x X Q → SetUnfold (x ∈ X) Q.
Proof. by destruct 1; constructor. Qed.
Class SetUnfoldSimpl (P Q : Prop) := { set_unfold_simpl : SetUnfold P Q }.
Global Hint Extern 0 (SetUnfoldSimpl _ _) => csimpl; constructor : typeclass_instances.
-Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
+Global Instance set_unfold_default P : SetUnfold P P | 1000. done. Qed.
Definition set_unfold_1 `{SetUnfold P Q} : P → Q := proj1 (set_unfold P Q).
Definition set_unfold_2 `{SetUnfold P Q} : Q → P := proj2 (set_unfold P Q).
@@ -244,7 +244,7 @@ Section set_unfold.
Qed.
End set_unfold.
-Instance set_unfold_top `{TopSet A C} (x : A) :
+Global Instance set_unfold_top `{TopSet A C} (x : A) :
SetUnfoldElemOf x (⊤ : C) True.
Proof. constructor. split; [done|intros; apply elem_of_top']. Qed.
diff --git a/theories/streams.v b/theories/streams.v
index 50c219c85d0b751459afbd4a124428eea21d131c..3c2736a2df09337e5c29f5cc6ddf6a48a31b7dc7 100644
--- a/theories/streams.v
+++ b/theories/streams.v
@@ -6,7 +6,7 @@ Delimit Scope stream_scope with stream.
Open Scope stream_scope.
CoInductive stream (A : Type) : Type := scons : A → stream A → stream A.
-Arguments scons {_} _ _ : assert.
+Global Arguments scons {_} _ _ : assert.
Infix ":.:" := scons (at level 60, right associativity) : stream_scope.
Bind Scope stream_scope with stream.
@@ -17,7 +17,7 @@ CoInductive stream_equiv' {A} (s1 s2 : stream A) : Prop :=
scons_equiv' :
shead s1 = shead s2 → stream_equiv' (stail s1) (stail s2) →
stream_equiv' s1 s2.
-Instance stream_equiv {A} : Equiv (stream A) := stream_equiv'.
+Global Instance stream_equiv {A} : Equiv (stream A) := stream_equiv'.
Reserved Infix "!.!" (at level 20).
Fixpoint slookup {A} (i : nat) (s : stream A) : A :=
diff --git a/theories/strings.v b/theories/strings.v
index dcf2673ce76b0940fc58d217393b1522e4b28b7b..f41aa1fbf11d57377610fe87acdf5ad31e91ce43 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -14,16 +14,16 @@ Open Scope string_scope.
the "++" notation designates list concatenation. *)
Open Scope list_scope.
Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
-Arguments String.append : simpl never.
+Global Arguments String.append : simpl never.
(** * Decision of equality *)
-Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
-Instance string_eq_dec : EqDecision string.
+Global Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
+Global Instance string_eq_dec : EqDecision string.
Proof. solve_decision. Defined.
-Instance string_app_inj s1 : Inj (=) (=) (String.append s1).
+Global Instance string_app_inj s1 : Inj (=) (=) (String.append s1).
Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
-Instance string_inhabited : Inhabited string := populate "".
+Global Instance string_inhabited : Inhabited string := populate "".
(* Reverse *)
Fixpoint string_rev_app (s1 s2 : string) : string :=
@@ -117,5 +117,5 @@ Program Instance string_countable : Countable string := {|
Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
Lemma ascii_of_to_digits a : ascii_of_digits (ascii_to_digits a) = a.
Proof. by destruct a as [[][][][][][][][]]. Qed.
-Instance ascii_countable : Countable ascii :=
+Global Instance ascii_countable : Countable ascii :=
inj_countable' ascii_to_digits ascii_of_digits ascii_of_to_digits.
diff --git a/theories/telescopes.v b/theories/telescopes.v
index 55beb892060fbd9a090ba651ee09ed90dd7104ad..c02e9c5ecccc6af21c91ab7ad84e683e027cfdfd 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -8,7 +8,7 @@ Inductive tele : Type :=
| TeleO : tele
| TeleS {X} (binder : X → tele) : tele.
-Arguments TeleS {_} _.
+Global Arguments TeleS {_} _.
(** The telescope version of Coq's function type *)
Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
@@ -30,7 +30,7 @@ Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y)
| TeleO => λ x : X, base x
| TeleS b => λ f, step (λ x, rec (f x))
end) TT.
-Arguments tele_fold {_ _ !_} _ _ _ /.
+Global Arguments tele_fold {_ _ !_} _ _ _ /.
(** A sigma-like type for an "element" of a telescope, i.e. the data it
takes to get a [T] from a [TT -t> T]. *)
@@ -45,7 +45,7 @@ Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
| TargO => λ t : T, t
| TargS x a => λ f, rec a (f x)
end) TT a f.
-Arguments tele_app {!_ _} _ !_ /.
+Global Arguments tele_app {!_ _} _ !_ /.
Coercion tele_arg : tele >-> Sortclass.
(* This is a local coercion because otherwise, the "λ.." notation stops working. *)
@@ -71,7 +71,7 @@ Fixpoint tele_map {T U} {TT : tele} : (T → U) → (TT -t> T) → TT -t> U :=
| @TeleS X b => λ (F : T → U) (f : TeleS b -t> T) (x : X),
tele_map F (f x)
end.
-Arguments tele_map {_ _ !_} _ _ /.
+Global Arguments tele_map {_ _ !_} _ _ /.
Lemma tele_map_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) :
(tele_map F t) x = F (t x).
@@ -95,7 +95,7 @@ Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
| @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
tele_bind (λ a, F (TargS x a))
end.
-Arguments tele_bind {_ !_} _ /.
+Global Arguments tele_bind {_ !_} _ /.
(* Show that tele_app ∘ tele_bind is the identity. *)
Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
@@ -148,10 +148,10 @@ Notation "'λ..' x .. y , e" :=
(** Telescopic quantifiers *)
Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop :=
tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ).
-Arguments tforall {!_} _ /.
+Global Arguments tforall {!_} _ /.
Definition texist {TT : tele} (Ψ : TT → Prop) : Prop :=
tele_fold ex (λ x, x) (tele_bind Ψ).
-Arguments texist {!_} _ /.
+Global Arguments texist {!_} _ /.
Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. ))
(at level 200, x binder, y binder, right associativity,
diff --git a/theories/vector.v b/theories/vector.v
index d64538e839f4f0ae2214462c2650b43932fe19f1..6cff743f2a285fd61bde6c4ff69f7e9c9a43e811 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -13,10 +13,10 @@ used for lists, we use slightly different notations so it becomes easier to use
lists and vectors together. *)
Notation vec := Vector.t.
Notation vnil := Vector.nil.
-Arguments vnil {_}.
+Global Arguments vnil {_}.
Notation vcons := Vector.cons.
Notation vapp := Vector.append.
-Arguments vcons {_} _ {_} _.
+Global Arguments vcons {_} _ {_} _.
Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
Notation "(:::)" := vcons (only parsing) : vector_scope.
@@ -41,7 +41,7 @@ Proof.
refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
Defined.
-Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
+Global Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
match i in fin m return vec A m → A with
| 0%fin => vec_S_inv (λ _, A) (λ x _, x)
@@ -74,7 +74,7 @@ Proof.
- apply IH. intros i. apply (Hi (FS i)).
Qed.
-Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
+Global Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
Proof.
refine (vec_rect2
(λ n (v w : vec A n), { v = w } + { v ≠w })
@@ -330,7 +330,7 @@ Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=
populate (vreplicate n inhabitant).
-Instance vec_countable `{Countable A} n : Countable (vec A n).
+Global Instance vec_countable `{Countable A} n : Countable (vec A n).
Proof.
apply (inj_countable vec_to_list (λ l,
guard (n = length l) as H; Some (eq_rect _ _ (list_to_vec l) _ (eq_sym H)))).
diff --git a/theories/zmap.v b/theories/zmap.v
index 47190f8db6fde3235f95180873e281fa4272052b..e53aeb74bdccb9d9df8d47338783ef78fba2c163 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -7,12 +7,12 @@ Local Open Scope Z_scope.
Record Zmap (A : Type) : Type :=
ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
-Arguments Zmap_0 {_} _ : assert.
-Arguments Zmap_pos {_} _ : assert.
-Arguments Zmap_neg {_} _ : assert.
-Arguments ZMap {_} _ _ _ : assert.
+Global Arguments Zmap_0 {_} _ : assert.
+Global Arguments Zmap_pos {_} _ : assert.
+Global Arguments Zmap_neg {_} _ : assert.
+Global Arguments ZMap {_} _ _ _ : assert.
-Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
+Global Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
Proof.
refine (λ t1 t2,
match t1, t2 with
@@ -20,31 +20,31 @@ Proof.
cast_if_and3 (decide (x = y)) (decide (t1 = t2)) (decide (t1' = t2'))
end); abstract congruence.
Defined.
-Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
-Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
+Global Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
+Global Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
match i with
| Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
end.
-Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
+Global Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
match i, t with
| Z0, ZMap o t t' => ZMap (f o) t t'
| Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
| Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
end.
-Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
+Global Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
match t with
| ZMap o t t' => from_option (λ x, [(0,x)]) [] o ++
(prod_map Zpos id <$> map_to_list t) ++
(prod_map Zneg id <$> map_to_list t')
end.
-Instance Zomap: OMap Zmap := λ A B f t,
+Global Instance Zomap: OMap Zmap := λ A B f t,
match t with ZMap o t t' => ZMap (o ≫= f) (omap f t) (omap f t') end.
-Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
+Global Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
match t1, t2 with
| ZMap o1 t1 t1', ZMap o2 t2 t2' =>
ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
end.
-Instance Nfmap: FMap Zmap := λ A B f t,
+Global Instance Nfmap: FMap Zmap := λ A B f t,
match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
Instance: FinMap Z Zmap.
@@ -91,5 +91,5 @@ Qed.
(** * Finite sets *)
(** We construct sets of [Z]s satisfying extensional equality. *)
Notation Zset := (mapset Zmap).
-Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
+Global Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.