From ffa05e8ac2d0c754d3bd09f91e617ac73e0945e2 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 5 Apr 2020 12:04:44 +0200
Subject: [PATCH] Switch `inj _` to `inj f`, part 2

Code not affected by a00d9bd814bc97622b2e9cf86c0a78e300680f70.

All occurrences are gone, except for one in `base.v` where you'd need different
functions.

However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" higher-order
unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
g args`.
---
 theories/gmultiset.v | 2 +-
 theories/list.v      | 2 +-
 theories/numbers.v   | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index f0fa7ffb..6940ba8e 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -222,7 +222,7 @@ Proof.
   rewrite !multiplicity_disj_union. lia.
 Qed.
 Global Instance gmultiset_disj_union_inj_2 X : Inj (=) (=) (.⊎ X).
-Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj _). Qed.
+Proof. intros Y1 Y2. rewrite <-!(comm_L _ X). apply (inj (X ⊎.)). Qed.
 
 Lemma gmultiset_disj_union_intersection_l X Y Z : X ⊎ (Y ∩ Z) = (X ⊎ Y) ∩ (X ⊎ Z).
 Proof.
diff --git a/theories/list.v b/theories/list.v
index 1203a5db..825b2f09 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2232,7 +2232,7 @@ Qed.
 Lemma submseteq_app_inv_l l1 l2 k : k ++ l1 ⊆+ k ++ l2 → l1 ⊆+ l2.
 Proof.
   induction k as [|y k IH]; simpl; [done |]. rewrite submseteq_cons_l.
-  intros (?&E%(inj _)&?). apply IH. by rewrite E.
+  intros (?&E%(inj (cons y))&?). apply IH. by rewrite E.
 Qed.
 Lemma submseteq_app_inv_r l1 l2 k : l1 ++ k ⊆+ l2 ++ k → l1 ⊆+ l2.
 Proof.
diff --git a/theories/numbers.v b/theories/numbers.v
index 8f291435..6f03dd23 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -710,7 +710,7 @@ Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed.
 Instance Qp_plus_comm : Comm (=) Qp_plus.
 Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed.
 Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p).
-Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj _). Qed.
+Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed.
 Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp.
 Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed.
 
@@ -794,9 +794,9 @@ Proof.
     destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq].
     - auto.
     - destruct (help c d a b); [done..|]. naive_solver.
-    - apply (inj _) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
+    - apply (inj (Qp_plus a)) in H as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
       eauto 10 using (comm_L Qp_plus). }
-  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj _).
+  intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)).
   destruct (Qp_lower_bound a d) as (q&a'&d'&->&->).
   eexists a', q, (q + e)%Qp, d'; split_and?; auto using (comm_L Qp_plus).
   - by rewrite (assoc_L _), (comm_L Qp_plus e).
-- 
GitLab