Support arbitrary specialization patterns in `iInv`.

theories/base_logic/lib/cancelable_invariants.v

@@ -94,10 +94,9 @@ Section proofs.
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
   Global Instance elim_inv_cinv p γ E N P P' Q Q' :
     ElimModal True (|={E,E∖↑N}=> (▷ P ∗ cinv_own γ p) ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
-    ElimInv (↑N ⊆ E) N (cinv N γ P) [cinv_own γ p] P' Q Q'.
+    ElimInv (↑N ⊆ E) N (cinv N γ P) (cinv_own γ p) P' Q Q'.
   Proof.
-    rewrite /ElimInv/ElimModal.
-    iIntros (Helim ?) "(#H1&(Hown&_)&H2)".
+    rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
     iApply Helim; auto. iFrame "H2".
     iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
     by iFrame.

theories/base_logic/lib/invariants.v

@@ -98,13 +98,11 @@ Global Instance into_inv_inv N P : IntoInv (inv N P) N.
 
 Global Instance elim_inv_inv E N P P' Q Q' :
   ElimModal True (|={E,E∖↑N}=> ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True))%I P' Q Q' →
-  ElimInv (↑N ⊆ E) N (inv N P) [] P' Q Q'.
+  ElimInv (↑N ⊆ E) N (inv N P) True P' Q Q'.
 Proof.
-  rewrite /ElimInv/ElimModal.
-  iIntros (Helim ?) "(#H1&_&H2)".
+  rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
   iApply Helim; auto; iFrame.
-  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto. 
-  iFrame. by iModIntro.
+  iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :

theories/base_logic/lib/na_invariants.v

@@ -115,10 +115,9 @@ Section proofs.
   Global Instance elim_inv_na p F E N P P' Q Q':
     ElimModal True (|={E}=> (▷ P ∗ na_own p (F∖↑N)) ∗ (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F))%I
               P' Q Q' →
-    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) N (na_inv p N P) [na_own p F] P' Q Q'.
+    ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) N (na_inv p N P) (na_own p F) P' Q Q'.
   Proof.
-    rewrite /ElimInv/ElimModal.
-    iIntros (Helim (?&?)) "(#H1&(Hown&_)&H2)".
+    rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
     iApply Helim; auto. iFrame "H2".
     iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto. 
     by iFrame.

theories/proofmode/classes.v

@@ -476,7 +476,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
 
 (* Input: `Pinv`;
    - `Pinv`, an invariant assertion
-   - `Ps_aux` is a list of additional assertions needed for opening an invariant;
+   - `Pin` the additional assertions needed for opening an invariant;
    - `Pout` is the assertion obtained by opening the invariant;
    - `Q` is a goal on which iInv may be invoked;
    - `Q'` is the transformed goal that must be proved after opening the invariant.
@@ -486,9 +486,8 @@ Hint Mode IntoInv + ! - : typeclass_instances.
    is not a clearly associated instance of ElimModal of the right form
    (e.g. to handle Iris 2.0 usage of iInv).
 *)
-Class ElimInv {PROP : bi} (φ: Prop) (N: namespace)
-      (Pinv : PROP) (Ps_aux: list PROP) (Pout Q Q': PROP) :=
-  elim_inv : φ → Pinv ∗ [∗] Ps_aux ∗ (Pout -∗ Q') ⊢ Q.
+Class ElimInv {PROP : bi} (φ : Prop) (N : namespace) (Pinv Pin Pout Q Q' : PROP) :=
+  elim_inv : φ → Pinv ∗ Pin ∗ (Pout -∗ Q') ⊢ Q.
 Arguments ElimInv {_} _ _ _  _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I _%I.
 Hint Mode ElimInv + - - ! - - - - : typeclass_instances.

theories/proofmode/coq_tactics.v

@@ -1171,17 +1171,19 @@ Proof.
 Qed.
 
 (** * Invariants *)
-Lemma tac_inv_elim Δ1 Δ2 Δ3 js j p φ N P' P Ps Q Q' :
-  envs_lookup_delete_list false js Δ1 = Some (p, P :: Ps, Δ2) →
-  ElimInv φ N P Ps P' Q Q' →
+Lemma tac_inv_elim Δ Δ' i j φ N p P Pin Pout Q Q' :
+  envs_lookup_delete false i Δ = Some (p, P, Δ') →
+  ElimInv φ N P Pin Pout Q Q' →
   φ →
-  envs_app false (Esnoc Enil j P') Δ2 = Some Δ3 →
-  envs_entails Δ3 Q' → envs_entails Δ1 Q.
+  (∀ R, ∃ Δ'',
+    envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
+    envs_entails Δ'' R) →
+  envs_entails Δ Q.
 Proof.
-  rewrite envs_entails_eq => ???? HΔ. rewrite envs_lookup_delete_list_sound //.
-  rewrite envs_app_singleton_sound //=.
-  rewrite HΔ //= affinely_persistently_if_elim //=.
-  rewrite -sep_assoc. by eapply elim_inv.
+  rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
+  rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
+  apply wand_elim_r', wand_mono; last done.
+  apply wand_intro_r, wand_intro_r. rewrite affinely_persistently_if_elim -assoc. auto.
 Qed.
 End bi_tactics.
 

theories/proofmode/tactics.v

@@ -215,14 +215,6 @@ Tactic Notation "iAssumption" :=
            |fail "iAssumption:" Q "not found"]
   end.
 
-Tactic Notation "iAssumptionListCore" :=
-  repeat match goal with
-  | |- envs_lookup_delete_list _ ?ils ?p = Some (_, ?P :: ?Ps, _) =>
-    eapply envs_lookup_delete_list_cons; [by iAssumptionCore |]
-  | |- envs_lookup_delete_list _ ?ils ?p = Some (_, [], _) =>
-    eapply envs_lookup_delete_list_nil
-  end.
-
 (** * False *)
 Tactic Notation "iExFalso" := apply tac_ex_falso.
 
@@ -1886,33 +1878,27 @@ Tactic Notation "iAssumptionInv" constr(N) :=
      is_evar i; first [find Γp i P | find Γs i P]; env_reflexivity
   end.
 
-Tactic Notation "iInvCore" constr(N) "with" constr(Hs) "as" tactic(tac) constr(Hclose) :=
-  let hd_id := fresh "hd_id" in evar (hd_id: ident);
-  let hd_id := eval unfold hd_id in hd_id in
-  let Htmp1 := iFresh in
-  let Htmp2 := iFresh in
-  let patback := intro_pat.parse_one Hclose in
-  eapply tac_inv_elim with _ _ (hd_id :: Hs) Htmp1 _ _ N _  _ _ _;
-  first eapply envs_lookup_delete_list_cons; swap 2 3;
-    [ iAssumptionInv N || fail "iInv: invariant" N "not found"
-    | apply _ ||
+Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) constr(Hclose) :=
+  iStartProof;
+  let H := iFresh in
+  eapply tac_inv_elim with _ _ H _ N _ _ _ _ _;
+    [iAssumptionInv N || fail "iInv: invariant" N "not found"
+    |apply _ ||
      let I := match goal with |- ElimInv _ ?N ?I  _ _ _ _ => I end in
      fail "iInv: cannot eliminate invariant " I " with namespace " N
-    | iAssumptionListCore || fail "iInv: other assumptions not found"
-    | try (split_and?; solve [ fast_done | solve_ndisj ])
-    | env_reflexivity |];
-  let pat := constr:(IList [[IIdent Htmp2; patback]]) in
-  iDestruct Htmp1 as pat;
-  tac Htmp2.
+    |try (split_and?; solve [ fast_done | solve_ndisj ])
+    |let R := fresh in intros R; eexists; split; [env_reflexivity|];
+     iSpecializePat H pats; last (
+       iApplyHyp H; clear R;
+       iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
+       let patclose := intro_pat.parse_one Hclose in
+       let patintro := constr:(IList [[IIdent H; patclose]]) in
+       iDestructHyp H as patintro;
+       tac H
+     )].
 
 Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
-  let tl_ids := fresh "tl_ids" in evar (tl_ids: list ident);
-  let tl_ids := eval unfold tl_ids in tl_ids in
-  iInvCore N with tl_ids as (fun H => tac H) Hclose.
-Tactic Notation "iInvCoreParse" constr(N) "with" constr(Hs) "as" tactic(tac) constr(Hclose) :=
-  let Hs := words Hs in
-  let Hs := eval vm_compute in (INamed <$> Hs) in
-  iInvCore N with Hs as (fun H => tac H) Hclose.
+  iInvCore N with "[$]" as ltac:(tac) Hclose.
 
 Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
    iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
@@ -1931,21 +1917,21 @@ Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
     constr(pat) constr(Hclose) :=
    iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
-   iInvCoreParse N with Hs as (fun H => iDestructHyp H as pat) Hclose.
+   iInvCore N with Hs as (fun H => iDestructHyp H as pat) Hclose.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
     constr(pat) constr(Hclose) :=
-   iInvCoreParse N with Hs as (fun H => iDestructHyp H as (x1) pat) Hclose.
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) Hclose.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
-   iInvCoreParse N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) Hclose.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) ")"
     constr(pat) constr(Hclose) :=
-   iInvCoreParse N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
 Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
     simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
     constr(pat) constr(Hclose) :=
-   iInvCoreParse N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
+   iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
 
 Hint Extern 0 (_ ⊢ _) => iStartProof.
 

theories/tests/proofmode_iris.v

@@ -82,7 +82,7 @@ Section iris_tests.
       ={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2  ∗ ▷ P.
   Proof.
     iIntros "(#?&Hown1&Hown2)".
-    iInv N as "(#HP&Hown2)" "Hclose".
+    iInv N with "[Hown2 //]" as "(#HP&Hown2)" "Hclose".
     iMod ("Hclose" with "HP").
     iModIntro. iFrame. by iNext.
   Qed.