Merge branch 'inj-typeclass-2' into 'master'

Revise uses of `inj` from !408 as discussed

See merge request iris/iris!412

theories/algebra/agree.v

@@ -184,7 +184,7 @@ Proof.
   move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
 Qed.
 Global Instance to_agree_inj : Inj (≡) (≡) (to_agree).
-Proof. intros a b ?. apply equiv_dist=>n. by apply (inj _), equiv_dist. Qed.
+Proof. intros a b ?. apply equiv_dist=>n. by apply (inj to_agree), equiv_dist. Qed.
 
 Lemma to_agree_uninjN n x : ✓{n} x → ∃ a, to_agree a ≡{n}≡ x.
 Proof.
@@ -232,7 +232,7 @@ Proof.
   intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
 Qed.
 Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
-Proof. by intros ?%agree_op_inv%(inj _). Qed.
+Proof. by intros ?%agree_op_inv%(inj to_agree). Qed.
 Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
 Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
 
@@ -240,7 +240,7 @@ Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
 Lemma agree_equivI {M} a b : to_agree a ≡ to_agree b ⊣⊢@{uPredI M} (a ≡ b).
 Proof.
   uPred.unseal. do 2 split.
-  - intros Hx. exact: inj.
+  - intros Hx. exact: (inj to_agree).
   - intros Hx. exact: to_agree_ne.
 Qed.
 Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢@{uPredI M} x ≡ y.

theories/algebra/auth.v

@@ -156,7 +156,7 @@ Lemma auth_auth_frac_validN n q a :
   ✓{n} (●{q} a) ↔ ✓{n} q ∧ ✓{n} a.
 Proof.
   rewrite auth_validN_eq /=. apply and_iff_compat_l. split.
-  - by intros [?[->%(inj _) []]].
+  - by intros [?[->%(inj to_agree) []]].
   - naive_solver eauto using ucmra_unit_leastN.
 Qed.
 Lemma auth_auth_validN n a : ✓{n} a ↔ ✓{n} (● a).
@@ -168,7 +168,7 @@ Lemma auth_both_frac_validN n q a b :
 Proof.
   rewrite auth_validN_eq /=. apply and_iff_compat_l.
   setoid_rewrite (left_id _ _ b). split.
-  - by intros [?[->%(inj _)]].
+  - by intros [?[->%(inj to_agree)]].
   - naive_solver.
 Qed.
 Lemma auth_both_validN n a b : ✓{n} (● a ⋅ ◯ b) ↔ b ≼{n} a ∧ ✓{n} a.
@@ -182,7 +182,7 @@ Lemma auth_auth_frac_valid q a : ✓ (●{q} a) ↔ ✓ q ∧ ✓ a.
 Proof.
   rewrite auth_valid_eq /=. apply and_iff_compat_l. split.
   - intros H'. apply cmra_valid_validN. intros n.
-    by destruct (H' n) as [? [->%(inj _) [??]]].
+    by destruct (H' n) as [? [->%(inj to_agree) [??]]].
   - intros. exists a. split; [done|].
     split; by [apply ucmra_unit_leastN|apply cmra_valid_validN].
 Qed.
@@ -216,7 +216,7 @@ Lemma auth_both_frac_valid `{!CmraDiscrete A} q a b :
 Proof.
   rewrite auth_valid_discrete /=. apply and_iff_compat_l.
   setoid_rewrite (left_id _ _ b). split.
-  - by intros [?[->%(inj _)]].
+  - by intros [?[->%(inj to_agree)]].
   - naive_solver.
 Qed.
 Lemma auth_both_valid `{!CmraDiscrete A} a b : ✓ (● a ⋅ ◯ b) ↔ b ≼ a ∧ ✓ a.
@@ -304,7 +304,7 @@ Qed.
 Lemma auth_auth_frac_op_invN n p a q b : ✓{n} (●{p} a ⋅ ●{q} b) → a ≡{n}≡ b.
 Proof.
   rewrite /op /auth_op /= left_id -Some_op -pair_op auth_validN_eq /=.
-  intros (?&?& Eq &?&?). apply (inj _), agree_op_invN. by rewrite Eq.
+  intros (?&?& Eq &?&?). apply (inj to_agree), agree_op_invN. by rewrite Eq.
 Qed.
 Lemma auth_auth_frac_op_inv p a q b : ✓ (●{p} a ⋅ ●{q} b) → a ≡ b.
 Proof.
@@ -356,7 +356,7 @@ Proof.
   move=> n [[[??]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
   + exfalso. move : VL => /frac_valid'.
     rewrite frac_op'. by apply Qp_not_plus_q_ge_1.
-  + split; [done|]. apply (inj _) in Eq.
+  + split; [done|]. apply (inj to_agree) in Eq.
     move: Ha; rewrite !left_id -assoc => Ha.
     destruct (Hup n (Some (bf1 ⋅ bf2))); [by rewrite Eq..|]. simpl in *.
     exists a'. split; [done|]. split; [|done]. exists bf2.
@@ -389,7 +389,7 @@ Proof.
   rewrite !local_update_unital=> Hup ? ? n /=.
     move=> [[[qc ac]|] bc] /auth_both_validN [Le Val] [] /=.
   - move => Ha. exfalso. move : Ha. rewrite right_id -Some_op -pair_op frac_op'.
-    move => /(inj _ _ _) [/= Eq _].
+    move => /Some_dist_inj [/= Eq _].
     apply (Qp_not_plus_q_ge_1 qc). by rewrite -Eq.
   - move => _. rewrite !left_id=> ?.
     destruct (Hup n bc) as [Hval' Heq]; eauto using cmra_validN_includedN.

theories/heap_lang/lang.v

@@ -574,7 +574,7 @@ Proof.
   - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=.
     { rewrite loc_add_0; eauto. }
     right. split.
-    { rewrite -{1}(loc_add_0 l). intros ?%(inj _); lia. }
+    { rewrite -{1}(loc_add_0 l). intros ?%(inj (loc_add _)); lia. }
     assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj.
     { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. }
     rewrite Hj /= in Hil.