diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index 71b5cacf90095fd7a9e35f999feea7d6fc012f25..4b51254982f5c837112fc41674b780faad7ca139 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/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"). }
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 0e2e17af520703019260ccc515f0cb903f6866c0..7bc3426de86dd5ee96378c7c4f050f28ddb25ce1 100644
--- a/theories/proofmode/tactics.v
+++ b/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
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 7d12d2e27b2d6b1ea644f5a36ea1a2e382c40b2c..a44213e29f0fe5629185493be7347522ffaf7478 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -1,5 +1,6 @@
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.