Hacky way of dealing with `iSpecialize ("H" !$ x)` where `x` contains TC holes.

theories/heap_lang/lib/barrier/proof.v

@@ -138,7 +138,7 @@ Proof.
   iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
   wp_load. destruct p.
-  - iMod ("Hclose" $! (State Low I) with "[Hl Hr]") as "Hγ".
+  - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
     { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
     iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
@@ -150,7 +150,7 @@ Proof.
     iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
     iAssert (▷ Ψ i ∗ ▷ [∗ set] j ∈ I ∖ {[i]}, Ψ j)%I with "[HΨ]" as "[HΨ HΨ']".
     { iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
-    iMod ("Hclose" $! (State High (I ∖ {[ i ]})) (∅ : set token) with "[HΨ' Hl Hsp]").
+    iMod ("Hclose" $! (State High (I ∖ {[ i ]})) ∅ with "[HΨ' Hl Hsp]").
     { iSplit; [iPureIntro; by eauto using wait_step|].
       rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
     iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
@@ -169,7 +169,8 @@ Proof.
   iMod (saved_prop_alloc_strong (R2: ∙%CF (iProp Σ)) (I ∪ {[i1]}))
     as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
   rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
-  iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]})) with "[-]") as "Hγ".
+  iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
+                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
   { iSplit; first by eauto using split_step.
     rewrite /barrier_inv /=. iNext. iFrame "Hl".
     by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }

theories/proofmode/tactics.v

@@ -17,7 +17,7 @@ Declare Reduction env_cbv := cbv [
     envs_split_go envs_split].
 Ltac env_cbv :=
   match goal with |- ?u => let v := eval env_cbv in u in change v end.
-Ltac env_reflexivity := env_cbv; reflexivity.
+Ltac env_reflexivity := env_cbv; exact eq_refl.
 
 (** * Misc *)
 (* Tactic Notation tactics cannot return terms *)
@@ -364,21 +364,34 @@ Notation "( H $! x1 .. xn 'with' pat )" :=
   (ITrm H (hcons x1 .. (hcons xn hnil) ..) pat) (at level 0, x1, xn at level 9).
 Notation "( H 'with' pat )" := (ITrm H hnil pat) (at level 0).
 
+(*
+There is some hacky stuff going on here (most probably there is a Coq bug).
+Holes -- like unresolved type class instances -- in the argument `xs` are
+resolved at arbitrary moments. It seems that tactics like `apply`, `split` and
+`eexists` trigger type class search to resolve these holes. To avoid TC being
+triggered too eagerly, this tactic uses `refine` at various places instead of
+`apply`.
+
+TODO: Investigate what really is going on. Is there a related to Cog bug #5752?
+When should holes in an `open_constr` be resolved?
+*)
 Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
   let rec go xs :=
     lazymatch xs with
-    | hnil => idtac
+    | hnil => apply id (* Finally, trigger TC *)
     | hcons ?x ?xs =>
        eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *)
-         [env_reflexivity || fail 1 "iSpecialize:" H "not found"
-         |apply _ ||
+         [env_reflexivity || fail "iSpecialize:" H "not found"
+         |typeclasses eauto ||
           let P := match goal with |- IntoForall ?P _ => P end in
-          fail 1 "iSpecialize: cannot instantiate" P "with" x
-         |exists x; split; [env_reflexivity|go xs]]
+          fail "iSpecialize: cannot instantiate" P "with" x
+         |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
+          | |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _))
+          end; [env_reflexivity|go xs]]
     end in
   go xs.
 
-Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
+Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
   let solve_to_wand H1 :=
     apply _ ||
     let P := match goal with |- IntoWand _ ?P _ _ => P end in

theories/tests/proofmode.v

 From iris.proofmode Require Import tactics.
 From iris.base_logic.lib Require Import invariants.
+From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
 Section tests.
@@ -117,6 +118,12 @@ Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
 Lemma test_iExist_coercion (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
 Proof. iIntros "HP". iExists (0:nat). iApply ("HP" $! (0:nat)). Qed.
 
+Lemma test_iExist_tc `{Collection A C} P : (∃ x1 x2 : gset positive, P -∗ P)%I.
+Proof. iExists {[ 1%positive ]}, ∅. auto. Qed.
+
+Lemma test_iSpecialize_tc P : (∀ x y z : gset positive, P) -∗ P.
+Proof. iIntros "H". iSpecialize ("H" $! ∅ {[ 1%positive ]} ∅). done. Qed.
+
 Lemma test_iAssert_modality P : (|==> False) -∗ |==> P.
 Proof. iIntros. iAssert False%I with "[> - //]" as %[]. Qed.