Uniform syntax for selecting hypotheses.

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.

ProofMode.md

@@ -14,8 +14,8 @@ Applying hypotheses and lemmas
 - `iExact "H"`  : finish the goal if the conclusion matches the hypothesis `H`
 - `iAssumption` : finish the goal if the conclusion matches any hypothesis
 - `iApply pm_trm` : match the conclusion of the current goal against the
-   conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
-   proof mode terms below.
+  conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
+  proof mode terms below.
 
 Context management
 ------------------
@@ -23,13 +23,12 @@ Context management
 - `iIntros (x1 ... xn) "ipat1 ... ipatn"` : introduce universal quantifiers
   using Coq introduction patterns `x1 ... xn` and implications/wands using proof
   mode introduction patterns `ipat1 ... ipatn`.
-- `iClear (x1 ... xn) "H1 ... Hn"` : clear the hypothesis `H1 ... Hn` as well as
-  the Coq level hypotheses/variables `x1 ... xn`. The symbol `★` can be used to
-  clear entire spatial context.
-- `iRevert (x1 ... xn) "H1 ... Hn"` : revert the proof mode hypotheses
-  `H1 ... Hn` into wands, as well as the Coq level hypotheses/variables
-  `x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
-  the entire spatial context.
+- `iClear (x1 ... xn) "selpat"` : clear the hypotheses given by the selection
+  pattern `selpat` and the Coq level hypotheses/variables `x1 ... xn`.
+- `iRevert (x1 ... xn) "selpat"` : revert the hypotheses given by the selection
+  pattern `selpat` into wands, and the Coq level hypotheses/variables
+  `x1 ... xn` into universal quantifiers. Persistent hypotheses are wrapped into
+  the always modality.
 - `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
 - `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
   implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
@@ -83,9 +82,9 @@ Elimination of logical connectives
 Separating logic specific tactics
 ---------------------------------
 
-- `iFrame (t1 .. tn) "H0 ... Hn"` : cancel the Coq terms (or Coq hypotheses)
-  `t1 ... tn` and Iris hypotheses `H0 ... Hn` in the goal. Apart from
-  hypotheses, the following symbols can be used:
+- `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
+  `t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
+  of the selection pattern have the following meaning:
 
   + `%` : repeatedly frame hypotheses from the Coq context.
   + `#` : repeatedly frame hypotheses from the persistent context.
@@ -102,16 +101,19 @@ Separating logic specific tactics
 The later modality
 ------------------
 - `iNext` : introduce a later by stripping laters from all hypotheses.
-- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction while generalizing
-  over the Coq level variables `x1 ... xn` and the entire spatial context.
+- `iLöb as "IH" forall (x1 ... xn)` : perform Löb induction by generating a
+  hypothesis `IH : ▷ goal`. The tactic generalizes over the Coq level variables
+  `x1 ... xn`, the hypotheses given by the selection pattern `selpat`, and the
+  spatial context.
 
 Induction
 ---------
-- `iInduction x as cpat "IH" forall (x1 ... xn)` : perform induction on the Coq
-  term `x`. The Coq introduction pattern is used to name the introduced
+- `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction on
+  the Coq term `x`. The Coq introduction pattern is used to name the introduced
   variables. The induction hypotheses are inserted into the persistent context
   and given fresh names prefixed `IH`. The tactic generalizes over the Coq level
-  variables `x1 ... xn` and the entire spatial context.
+  variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
+  and the spatial context.
 
 Rewriting
 ---------
@@ -125,11 +127,11 @@ Iris
 - `iVsIntro` : introduction of a raw or primitive view shift.
 - `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift
   `pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or
-   a weakest precondition).
+  a weakest precondition).
 - `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
 - `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
-   permits, i.e. it is a later, True now, raw or primitive view shift, or a
-   weakest precondition).
+  permits, i.e. it is a later, True now, raw or primitive view shift, or a
+  weakest precondition).
 
 Miscellaneous
 -------------
@@ -141,14 +143,26 @@ Miscellaneous
   existential quantifiers, implications and wand, always and later modalities,
   primitive view shifts, and pure connectives.
 
+Selection patterns
+==================
+
+Selection patterns are used to select hypotheses in the tactics `iRevert`,
+`iClear`, `iFrame`, `iLöb` and `iInduction`. The proof mode supports the
+following _selection patterns_:
+
+- `H` : select the hypothesis named `H`.
+- `%` : select the entire pure/Coq context.
+- `#` : select the entire persistent context.
+- `★` : select the entire spatial context.
+
 Introduction patterns
 =====================
 
 Introduction patterns are used to perform introductions and eliminations of
 multiple connectives on the fly. The proof mode supports the following
-introduction patterns:
+_introduction patterns_:
 
-- `H` : create a hypothesis named H.
+- `H` : create a hypothesis named `H`.
 - `?` : create an anonymous hypothesis.
 - `_` : remove the hypothesis.
 - `$` : frame the hypothesis in the goal.
@@ -197,9 +211,9 @@ Specialization patterns
 =======================
 
 Since we are reasoning in a spatial logic, when eliminating a lemma or
-hypotheses of type ``P_0 -★ ... -★ P_n -★ R`` one has to specify how the
+hypothesis of type ``P_0 -★ ... -★ P_n -★ R``, one has to specify how the
 hypotheses are split between the premises. The proof mode supports the following
-so called specification patterns to express this splitting:
+_specification patterns_ to express splitting of hypotheses:
 
 - `H` : use the hypothesis `H` (it should match the premise exactly). If `H` is
   spatial, it will be consumed.

_CoqProject

@@ -120,6 +120,7 @@ proofmode/pviewshifts.v
 proofmode/environments.v
 proofmode/intro_patterns.v
 proofmode/spec_patterns.v
+proofmode/sel_patterns.v
 proofmode/tactics.v
 proofmode/notation.v
 proofmode/invariants.v

program_logic/counter_examples.v

@@ -152,7 +152,7 @@ Module inv. Section inv.
     iDestruct (finished_dup with "Hf") as "[Hf Hf']".
     iApply pvs_intro. iSplitL "Hf'"; first by eauto.
     (* Step 2: Open the Q-invariant. *)
-    iClear "HiP". clear i. iDestruct "HsQ" as (i) "HiQ".
+    iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
     iApply (inv_open' i). iSplit; first done.
     iIntros "[HaQ | [_ #HQ]]".
     { iExFalso. iApply finished_not_start. by iFrame. }

proofmode/coq_tactics.v

@@ -82,6 +82,9 @@ Definition env_spatial_is_nil {M} (Δ : envs M) :=
 Definition envs_clear_spatial {M} (Δ : envs M) : envs M :=
   Envs (env_persistent Δ) Enil.
 
+Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
+  Envs Enil (env_spatial Δ).
+
 Fixpoint envs_split_go {M}
     (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
   match js with
@@ -272,12 +275,6 @@ Proof.
   destruct Hwf; constructor; simpl; auto using Enil_wf.
 Qed.
 
-Lemma env_fold_wand Γ Q : env_fold uPred_wand Q Γ ⊣⊢ ([★] Γ -★ Q).
-Proof.
-  revert Q; induction Γ as [|Γ IH i P]=> Q /=; [by rewrite wand_True|].
-  by rewrite IH wand_curry (comm uPred_sep).
-Qed.
-
 Lemma env_spatial_is_nil_persistent Δ :
   env_spatial_is_nil Δ = true → PersistentP Δ.
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
@@ -385,9 +382,6 @@ Qed.
 Lemma tac_clear Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') → (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
-Lemma tac_clear_spatial Δ Δ' Q :
-  envs_clear_spatial Δ = Δ' → (Δ' ⊢ Q) → Δ ⊢ Q.
-Proof. intros <- ?. by rewrite envs_clear_spatial_sound // sep_elim_l. Qed.
 
 (** * False *)
 Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
@@ -612,12 +606,6 @@ Proof.
   - by rewrite HQ wand_elim_r.
 Qed.
 
-Lemma tac_revert_spatial Δ Q :
-  (envs_clear_spatial Δ ⊢ env_fold uPred_wand Q (env_spatial Δ)) → Δ ⊢ Q.
-Proof.
-  intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
-Qed.
-
 Lemma tac_revert_ih Δ P Q :
   env_spatial_is_nil Δ = true →
   (of_envs Δ ⊢ P) →

proofmode/environments.v

@@ -38,12 +38,6 @@ Instance: Params (@env_to_list) 1.
 Fixpoint env_dom {A} (Γ : env A) : list string :=
   match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
 
-Fixpoint env_fold {A B} (f : B → A → A) (x : A) (Γ : env B) : A :=
-  match Γ with
-  | Enil => x
-  | Esnoc Γ _ y => env_fold f (f y x) Γ
-  end.
-
 Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
   match Γapp with
   | Enil => Some Γ

proofmode/sel_patterns.v

+From iris.prelude Require Export strings.
+
+Inductive sel_pat :=
+  | SelPure
+  | SelPersistent
+  | SelSpatial
+  | SelName : string → sel_pat.
+
+Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
+  match ps with
+  | [] => false
+  | SelPure :: ps => true
+  | _ :: ps => sel_pat_pure ps
+  end.
+
+Module sel_pat.
+Fixpoint cons_name (kn : string) (k : list sel_pat) : list sel_pat :=
+  match kn with "" => k | _ => SelName (string_rev kn) :: k end.
+
+Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat :=
+  match s with
+  | "" => rev (cons_name kn k)
+  | String " " s => parse_go s (cons_name kn k) ""
+  | String "%" s => parse_go s (SelPure :: cons_name kn k) ""
+  | String "#" s => parse_go s (SelPersistent :: cons_name kn k) ""
+  | String (Ascii.Ascii false true false false false true true true) (* unicode ★ *)
+      (String (Ascii.Ascii false false false true true false false true)
+      (String (Ascii.Ascii true false true false false false false true) s)) =>
+     parse_go s (SelSpatial :: cons_name kn k) ""
+  | String a s => parse_go s k (String a kn)
+  end.
+Definition parse (s : string) : list sel_pat := parse_go s [] "".
+
+Ltac parse s :=
+  lazymatch type of s with
+  | list sel_pat => s
+  | list string => eval vm_compute in (SelName <$> s)
+  | string => eval vm_compute in (parse s)
+  end.
+End sel_pat.

[Janno]

I think this line is missing "selpat".

[Robbert]

Fixed in af80361b, thanks!