From c8bb51b2dae2fb03ace3d35c95b406cbb7a53aa6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Oct 2020 17:19:00 +0200
Subject: [PATCH] Avoid relying on implicit instance generalization, and name
 some instances.

Fix in preparation for https://github.com/coq/coq/pull/13188
---
 theories/base.v        | 44 +++++++++++++++++++++---------------------
 theories/fin.v         |  8 ++++----
 theories/fin_map_dom.v |  4 ++--
 theories/fin_maps.v    | 30 ++++++++++++++--------------
 theories/fin_sets.v    | 10 +++++-----
 theories/list.v        | 26 ++++++++++++-------------
 theories/sets.v        | 22 ++++++++++-----------
 theories/strings.v     |  4 ++--
 8 files changed, 74 insertions(+), 74 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index ceb16eef..265be492 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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: Comm (↔) (=@{A}).
+Instance eq_comm {A} : Comm (↔) (=@{A}).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (λ x y, y =@{A} x).
+Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (↔).
+Instance iff_comm : Comm (↔) (↔).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (∧).
+Instance and_comm : Comm (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: Assoc (↔) (∧).
+Instance and_assoc : Assoc (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: IdemP (↔) (∧).
+Instance and_idemp : IdemP (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (∨).
+Instance or_comm : Comm (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: Assoc (↔) (∨).
+Instance or_assoc : Assoc (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: IdemP (↔) (∨).
+Instance or_idemp : IdemP (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) True (∧).
+Instance True_and : LeftId (↔) True (∧).
 Proof. red; intuition. Qed.
-Instance: RightId (↔) True (∧).
+Instance and_True : RightId (↔) True (∧).
 Proof. red; intuition. Qed.
-Instance: LeftAbsorb (↔) False (∧).
+Instance False_and : LeftAbsorb (↔) False (∧).
 Proof. red; intuition. Qed.
-Instance: RightAbsorb (↔) False (∧).
+Instance and_False : RightAbsorb (↔) False (∧).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) False (∨).
+Instance False_or : LeftId (↔) False (∨).
 Proof. red; intuition. Qed.
-Instance: RightId (↔) False (∨).
+Instance or_False : RightId (↔) False (∨).
 Proof. red; intuition. Qed.
-Instance: LeftAbsorb (↔) True (∨).
+Instance True_or : LeftAbsorb (↔) True (∨).
 Proof. red; intuition. Qed.
-Instance: RightAbsorb (↔) True (∨).
+Instance or_True : RightAbsorb (↔) True (∨).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) True impl.
+Instance True_impl : LeftId (↔) True impl.
 Proof. unfold impl. red; intuition. Qed.
-Instance: RightAbsorb (↔) True impl.
+Instance impl_True : RightAbsorb (↔) True impl.
 Proof. unfold impl. red; intuition. Qed.
 
 
@@ -670,7 +670,7 @@ 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 : Inj2 (=) (=) (=) (@pair A B).
+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') :
   Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g).
@@ -727,9 +727,9 @@ Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
 Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
   match iB with populate y => populate (inl y) end.
 
-Instance inl_inj : Inj (=) (=) (@inl A B).
+Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
 Proof. injection 1; auto. Qed.
-Instance inr_inj : Inj (=) (=) (@inr A B).
+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') :
diff --git a/theories/fin.v b/theories/fin.v
index 5e72506b..b4090fa5 100644
--- a/theories/fin.v
+++ b/theories/fin.v
@@ -71,11 +71,11 @@ Ltac inv_fin i :=
     end
   end.
 
-Instance FS_inj: Inj (=) (=) (@FS n).
-Proof. intros n i j. apply Fin.FS_inj. Qed.
-Instance fin_to_nat_inj : Inj (=) (=) (@fin_to_nat n).
+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).
 Proof.
-  intros n i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
+  intros i. induction i; intros j; inv_fin j; intros; f_equal/=; auto with lia.
 Qed.
 
 Lemma fin_to_nat_lt {n} (i : fin n) : fin_to_nat i < n.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index cd60364d..c42a4911 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -211,7 +211,7 @@ Proof.
   constructor. by rewrite dom_delete, elem_of_difference,
     (set_unfold_elem_of _ (dom _ _) _), elem_of_singleton.
 Qed.
-Global Instance set_unfold_dom_singleton {A} i j :
+Global Instance set_unfold_dom_singleton {A} i j x :
   SetUnfoldElemOf i (dom D ({[ j := x ]} : M A)) (i = j).
 Proof. constructor. by rewrite dom_singleton, elem_of_singleton. Qed.
 Global Instance set_unfold_dom_union {A} i (m1 m2 : M A) Q1 Q2 :
@@ -252,6 +252,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) :
+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 9d4ce12c..c162e80d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -252,7 +252,7 @@ Proof.
   destruct (m1 !! i), (m2 !! i), (m3 !! i); simplify_eq/=;
     done || etrans; eauto.
 Qed.
-Global Instance map_subseteq_po : PartialOrder (⊆@{M A}).
+Global Instance map_subseteq_po {A} : PartialOrder (⊆@{M A}).
 Proof.
   split; [apply _|].
   intros m1 m2; rewrite !map_subseteq_spec.
@@ -1600,8 +1600,8 @@ Proof.
   split; [|naive_solver].
   intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver.
 Qed.
-Global Instance map_disjoint_sym : Symmetric (map_disjoint : relation (M A)).
-Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
+Global Instance map_disjoint_sym {A} : Symmetric (map_disjoint : relation (M A)).
+Proof. intros m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
 Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ##ₘ m.
 Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
 Lemma map_disjoint_empty_r {A} (m : M A) : m ##ₘ ∅.
@@ -1739,16 +1739,16 @@ Qed.
 End union_with.
 
 (** ** Properties of the [union] operation *)
-Global Instance: LeftId (=@{M A}) ∅ (∪) := _.
-Global Instance: RightId (=@{M A}) ∅ (∪) := _.
-Global Instance: Assoc (=@{M A}) (∪).
+Global Instance map_empty_union {A} : LeftId (=@{M A}) ∅ (∪) := _.
+Global Instance map_union_empty {A} : RightId (=@{M A}) ∅ (∪) := _.
+Global Instance map_union_assoc {A} : Assoc (=@{M A}) (∪).
 Proof.
-  intros A m1 m2 m3. unfold union, map_union, union_with, map_union_with.
+  intros m1 m2 m3. unfold union, map_union, union_with, map_union_with.
   apply (merge_assoc _). intros i.
   by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
-Global Instance: IdemP (=@{M A}) (∪).
-Proof. intros A ?. by apply union_with_idemp. Qed.
+Global Instance map_union_idemp {A} : IdemP (=@{M A}) (∪).
+Proof. intros ?. by apply union_with_idemp. Qed.
 Lemma lookup_union {A} (m1 m2 : M A) i :
   (m1 ∪ m2) !! i = union_with (λ x _, Some x) (m1 !! i) (m2 !! i).
 Proof. apply lookup_union_with. Qed.
@@ -2089,17 +2089,17 @@ Proof. by intros; apply (partial_alter_merge _). Qed.
 End intersection_with.
 
 (** ** Properties of the [intersection] operation *)
-Global Instance: LeftAbsorb (=@{M A}) ∅ (∩) := _.
-Global Instance: RightAbsorb (=@{M A}) ∅ (∩) := _.
-Global Instance: Assoc (=@{M A}) (∩).
+Global Instance map_empty_interaction {A} : LeftAbsorb (=@{M A}) ∅ (∩) := _.
+Global Instance map_interaction_empty {A} : RightAbsorb (=@{M A}) ∅ (∩) := _.
+Global Instance map_interaction_assoc {A} : Assoc (=@{M A}) (∩).
 Proof.
-  intros A m1 m2 m3.
+  intros m1 m2 m3.
   unfold intersection, map_intersection, intersection_with, map_intersection_with.
   apply (merge_assoc _). intros i.
   by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
-Global Instance: IdemP (=@{M A}) (∩).
-Proof. intros A ?. by apply intersection_with_idemp. Qed.
+Global Instance map_intersection_idemp {A} : IdemP (=@{M A}) (∩).
+Proof. intros ?. by apply intersection_with_idemp. Qed.
 
 Lemma lookup_intersection_Some {A} (m1 m2 : M A) i x :
   (m1 ∩ m2) !! i = Some x ↔ m1 !! i = Some x ∧ is_Some (m2 !! i).
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 6473a4cb..fd7ca4a5 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -283,10 +283,10 @@ Section filter.
     unfold filter, set_filter.
     by rewrite elem_of_list_to_set, elem_of_list_filter, elem_of_elements.
   Qed.
-  Global Instance set_unfold_filter X Q :
+  Global Instance set_unfold_filter X Q x :
     SetUnfoldElemOf x X Q → SetUnfoldElemOf x (filter P X) (P x ∧ Q).
   Proof.
-    intros x ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
+    intros ?; constructor. by rewrite elem_of_filter, (set_unfold_elem_of x X Q).
   Qed.
 
   Lemma filter_empty : filter P (∅:C) ≡ ∅.
@@ -321,9 +321,9 @@ Section map.
     unfold set_map. rewrite elem_of_list_to_set, elem_of_list_fmap.
     by setoid_rewrite elem_of_elements.
   Qed.
-  Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) :
-    (∀ y, SetUnfoldElemOf y X (P y)) →
-    SetUnfoldElemOf x (set_map (D:=D) f X) (∃ y, x = f y ∧ P y).
+  Global Instance set_unfold_map (f : A → B) (X : C) (P : A → Prop) y :
+    (∀ x, SetUnfoldElemOf x X (P x)) →
+    SetUnfoldElemOf y (set_map (D:=D) f X) (∃ x, y = f x ∧ P x).
   Proof. constructor. rewrite elem_of_map; naive_solver. Qed.
 
   Global Instance set_map_proper :
diff --git a/theories/list.v b/theories/list.v
index cddaea30..25ee5576 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1660,7 +1660,7 @@ Definition Permutation_skip := @perm_skip A.
 Definition Permutation_swap := @perm_swap A.
 Definition Permutation_singleton_inj := @Permutation_length_1 A.
 
-Global Instance Permutation_cons : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
+Global Instance Permutation_cons x : Proper ((≡ₚ) ==> (≡ₚ)) (@cons A x).
 Proof. by constructor. Qed.
 Global Existing Instance Permutation_app'.
 
@@ -3073,22 +3073,22 @@ Section Forall2_proper.
   Proof. repeat intro. eauto using Forall2_length. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R) tail.
   Proof. repeat intro. eauto using Forall2_tail. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (take n).
+  Global Instance: ∀ n, Proper (Forall2 R ==> Forall2 R) (take n).
   Proof. repeat intro. eauto using Forall2_take. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (drop n).
+  Global Instance: ∀ n, Proper (Forall2 R ==> Forall2 R) (drop n).
   Proof. repeat intro. eauto using Forall2_drop. Qed.
 
-  Global Instance: Proper (Forall2 R ==> option_Forall2 R) (lookup i).
+  Global Instance: ∀ i, Proper (Forall2 R ==> option_Forall2 R) (lookup i).
   Proof. repeat intro. by apply Forall2_lookup. Qed.
-  Global Instance:
+  Global Instance: ∀ f i,
     Proper (R ==> R) f → Proper (Forall2 R ==> Forall2 R) (alter f i).
   Proof. repeat intro. eauto using Forall2_alter. Qed.
-  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
+  Global Instance: ∀ i, Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
   Proof. repeat intro. eauto using Forall2_insert. Qed.
-  Global Instance:
+  Global Instance: ∀ i,
     Proper (Forall2 R ==> Forall2 R ==> Forall2 R) (list_inserts i).
   Proof. repeat intro. eauto using Forall2_inserts. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (delete i).
+  Global Instance: ∀ i, Proper (Forall2 R ==> Forall2 R) (delete i).
   Proof. repeat intro. eauto using Forall2_delete. Qed.
 
   Global Instance: Proper (option_Forall2 R ==> Forall2 R) option_list.
@@ -3097,17 +3097,17 @@ Section Forall2_proper.
     Proper (R ==> iff) P → Proper (Forall2 R ==> Forall2 R) (filter P).
   Proof. repeat intro; eauto using Forall2_filter. Qed.
 
-  Global Instance: Proper (R ==> Forall2 R) (replicate n).
+  Global Instance: ∀ n, Proper (R ==> Forall2 R) (replicate n).
   Proof. repeat intro. eauto using Forall2_replicate. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (rotate n).
+  Global Instance: ∀ n, Proper (Forall2 R ==> Forall2 R) (rotate n).
   Proof. repeat intro. eauto using Forall2_rotate. Qed.
-  Global Instance: Proper (Forall2 R ==> Forall2 R) (rotate_take s e).
+  Global Instance: ∀ s e, Proper (Forall2 R ==> Forall2 R) (rotate_take s e).
   Proof. repeat intro. eauto using Forall2_rotate_take. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R) reverse.
   Proof. repeat intro. eauto using Forall2_reverse. Qed.
   Global Instance: Proper (Forall2 R ==> option_Forall2 R) last.
   Proof. repeat intro. eauto using Forall2_last. Qed.
-  Global Instance: Proper (R ==> Forall2 R ==> Forall2 R) (resize n).
+  Global Instance: ∀ n, Proper (R ==> Forall2 R ==> Forall2 R) (resize n).
   Proof. repeat intro. eauto using Forall2_resize. Qed.
 End Forall2_proper.
 
@@ -4420,7 +4420,7 @@ End quote_lookup.
 Section quote.
   Context {A : Type}.
   Class Quote (E1 E2 : env A) (l : list A) (t : rlist nat) := {}.
-  Global Instance quote_nil: Quote E1 E1 [] rnil := {}.
+  Global Instance quote_nil E1 : Quote E1 E1 [] rnil := {}.
   Global Instance quote_node E1 E2 l i:
     QuoteLookup E1 E2 l i → Quote E1 E2 l (rnode i) | 1000 := {}.
   Global Instance quote_cons E1 E2 E3 x l i t :
diff --git a/theories/sets.v b/theories/sets.v
index 2f53d4d7..251f9898 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -187,7 +187,7 @@ Section set_unfold_simple.
     intros ?; constructor. unfold equiv, set_equiv.
     pose proof (not_elem_of_empty (C:=C)); naive_solver.
   Qed.
-  Global Instance set_unfold_equiv (P Q : A → Prop) X :
+  Global Instance set_unfold_equiv (P Q : A → Prop) X Y :
     (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
     SetUnfold (X ≡ Y) (∀ x, P x ↔ Q x) | 10.
   Proof. constructor. apply forall_proper; naive_solver. Qed.
@@ -195,7 +195,7 @@ Section set_unfold_simple.
     (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
     SetUnfold (X ⊆ Y) (∀ x, P x → Q x).
   Proof. constructor. apply forall_proper; naive_solver. Qed.
-  Global Instance set_unfold_subset (P Q : A → Prop) X :
+  Global Instance set_unfold_subset (P Q : A → Prop) X Y :
     (∀ x, SetUnfoldElemOf x X (P x)) → (∀ x, SetUnfoldElemOf x Y (Q x)) →
     SetUnfold (X ⊂ Y) ((∀ x, P x → Q x) ∧ ¬∀ x, Q x → P x).
   Proof.
@@ -253,15 +253,15 @@ Section set_unfold_monad.
   Global Instance set_unfold_ret {A} (x y : A) :
     SetUnfoldElemOf x (mret (M:=M) y) (x = y).
   Proof. constructor; apply elem_of_ret. Qed.
-  Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) :
+  Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) x :
     (∀ y, SetUnfoldElemOf y X (P y)) → (∀ y, SetUnfoldElemOf x (f y) (Q y)) →
     SetUnfoldElemOf x (X ≫= f) (∃ y, Q y ∧ P y).
   Proof. constructor. rewrite elem_of_bind; naive_solver. Qed.
-  Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) :
+  Global Instance set_unfold_fmap {A B} (f : A → B) (X : M A) (P : A → Prop) x :
     (∀ y, SetUnfoldElemOf y X (P y)) →
     SetUnfoldElemOf x (f <$> X) (∃ y, x = f y ∧ P y).
   Proof. constructor. rewrite elem_of_fmap; naive_solver. Qed.
-  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) :
+  Global Instance set_unfold_join {A} (X : M (M A)) (P : M A → Prop) x :
     (∀ Y, SetUnfoldElemOf Y X (P Y)) →
     SetUnfoldElemOf x (mjoin X) (∃ Y, x ∈ Y ∧ P Y).
   Proof. constructor. rewrite elem_of_join; naive_solver. Qed.
@@ -296,12 +296,12 @@ Section set_unfold_list.
     SetUnfoldElemOf x l P → SetUnfoldElemOf x (reverse l) P.
   Proof. constructor. by rewrite elem_of_reverse, (set_unfold_elem_of x l P). Qed.
 
-  Global Instance set_unfold_list_fmap {B} (f : A → B) l P :
-    (∀ y, SetUnfoldElemOf y l (P y)) →
-    SetUnfoldElemOf x (f <$> l) (∃ y, x = f y ∧ P y).
+  Global Instance set_unfold_list_fmap {B} (f : A → B) l P y :
+    (∀ x, SetUnfoldElemOf x l (P x)) →
+    SetUnfoldElemOf y (f <$> l) (∃ x, y = f x ∧ P x).
   Proof.
-    constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
-    by rewrite (set_unfold_elem_of y l (P y)).
+    constructor. rewrite elem_of_list_fmap. f_equiv; intros x.
+    by rewrite (set_unfold_elem_of x l (P x)).
   Qed.
   Global Instance set_unfold_rotate x l P n:
     SetUnfoldElemOf x l P → SetUnfoldElemOf x (rotate n l) P.
@@ -1131,7 +1131,7 @@ Section set_seq.
     - rewrite elem_of_empty. lia.
     - rewrite elem_of_union, elem_of_singleton, IH. lia.
   Qed.
-  Global Instance set_unfold_seq start len :
+  Global Instance set_unfold_seq start len x :
     SetUnfoldElemOf x (set_seq (C:=C) start len) (start ≤ x < start + len).
   Proof. constructor; apply elem_of_set_seq. Qed.
 
diff --git a/theories/strings.v b/theories/strings.v
index 0e694d54..dcf2673c 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -20,8 +20,8 @@ Arguments String.append : simpl never.
 Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
 Instance string_eq_dec : EqDecision string.
 Proof. solve_decision. Defined.
-Instance string_app_inj : Inj (=) (=) (String.append s1).
-Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
+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 "".
 
-- 
GitLab