More comments about iInv tactics.

ProofMode.md

@@ -170,8 +170,11 @@ Rewriting / simplification
 Iris
 ----
 
-- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
-  for closing the invariant is put in a hypothesis named `Hclose`.
+- `iInv (N with "selpat") as (x1 ... xn) "ipat" "Hclose"` : open the invariant
+  `N`. The selection pattern `selpat` is used for any auxiliary assertions
+  needed to open the invariant (e.g. for cancelable or non-atomic
+  invariants). The update for closing the invariant is put in a hypothesis named
+  `Hclose`.
 
 Miscellaneous
 -------------

theories/proofmode/classes.v

@@ -468,18 +468,19 @@ Proof. by apply as_valid. Qed.
 Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P → φ.
 Proof. by apply as_valid. Qed.
 
-(* Input: `P`; Outputs: `N`,
-   Extracts the namespace associated with an invariant assertion. Used for `iInv`. *)
+(* Input: [P]; Outputs: [N],
+   Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
 Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
 Arguments IntoInv {_} _%I _.
 Hint Mode IntoInv + ! - : typeclass_instances.
 
-(* Input: `Pinv`;
-   - `Pinv`, an invariant assertion
-   - `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.
+(* Input: [Pinv]
+   Arguments:
+   - [Pinv] is an invariant assertion
+   - [Pin] is an additional assertion 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.
 
    There are similarities to the definition of ElimModal, however we
    want to be general enough to support uses in settings where there

theories/proofmode/tactics.v

@@ -1865,6 +1865,11 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
 
+(** * Assert *)
+
+(* Finds a hypothesis in the context that is an invariant with
+   namespace [N].  To do so, we check whether for each hypothesis
+   ["H":P] we can find an instance of [IntoInv P N] *)
 Tactic Notation "iAssumptionInv" constr(N) :=
   let rec find Γ i P :=
     lazymatch Γ with