Proofmode support for introducing the plainness modality.

ProofMode.md

@@ -31,7 +31,7 @@ Context management
 - `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.
+  the persistence 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.
@@ -162,8 +162,8 @@ Miscellaneous
   introduces pure connectives.
 - The proof mode adds hints to the core `eauto` database so that `eauto`
   automatically introduces: conjunctions and disjunctions, universal and
-  existential quantifiers, implications and wand, always, later and update
-  modalities, and pure connectives.
+  existential quantifiers, implications and wand, plainness, persistence, later
+  and update modalities, and pure connectives.
 
 Selection patterns
 ==================
@@ -207,7 +207,9 @@ appear at the top level:
   Items of the selection pattern can be prefixed with `$`, which cause them to
   be framed instead of cleared.
 - `!%` : introduce a pure goal (and leave the proof mode).
-- `!#` : introduce an always modality and clear the spatial context.
+- `!#` : introduce an persistence or plainness modality and clear the spatial
+  context. In case of a plainness modality, it will prune all persistent
+  hypotheses that are not plain.
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.

theories/proofmode/class_instances.v

@@ -152,6 +152,12 @@ Global Instance into_persistent_persistent P :
   Persistent P → IntoPersistent false P P | 100.
 Proof. done. Qed.
 
+(* FromAlways *)
+Global Instance from_always_persistently P : FromAlways false (□ P) P.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_plainly P : FromAlways true (■ P) P.
+Proof. by rewrite /FromAlways. Qed.
+
 (* IntoLater *)
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.

theories/proofmode/classes.v

@@ -59,6 +59,11 @@ Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
 Arguments into_persistent {_} _ _ _ {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
+Class FromAlways {M} (p : bool) (P Q : uPred M) :=
+  from_always : (if p then ■ Q else □ Q) ⊢ P.
+Arguments from_always {_} _ _ _ {_}.
+Hint Mode FromAlways + - ! - : typeclass_instances.
+
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
@@ -252,7 +257,7 @@ with the exception of:
 - [FromAssumption] used by [iAssumption]
 - [Frame] used by [iFrame]
 - [IntoLaterN] and [FromLaterN] used by [iNext]
-- [IntoPersistentP] used by [iPersistent]
+- [IntoPersistent] used by [iPersistent]
 *)
 Instance into_pure_tc_opaque {M} (P : uPred M) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.

theories/proofmode/coq_tactics.v

@@ -473,12 +473,58 @@ Proof.
   by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
 Qed.
 
-(** * Always *)
-Lemma tac_persistently_intro Δ Q :
-  (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
+(** * Persistence and plainness modality *)
+Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
+  into_plain_env_subenv : env_subenv Γ2 Γ1;
+  into_plain_env_plain : Plain ([∗] Γ2);
+}.
+Class IntoPersistentEnvs (p : bool) (Δ1 Δ2 : envs M) := {
+  into_persistent_envs_persistent :
+    if p then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
+    else env_persistent Δ1 = env_persistent Δ2;
+  into_persistent_envs_spatial : env_spatial Δ2 = Enil
+}.
+
+Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
+Proof. constructor. constructor. simpl; apply _. Qed.
+Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
+  Plain P → IntoPlainEnv Γ1 Γ2 →
+  IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
+Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
+Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
+  IntoPlainEnv Γ1 Γ2 → IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
+Proof. intros [??]; constructor. by constructor. done. Qed.
+
+Global Instance into_persistent_envs_false Γp Γs :
+  IntoPersistentEnvs false (Envs Γp Γs) (Envs Γp Enil).
+Proof. by split. Qed.
+Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
+  IntoPlainEnv Γp1 Γp2 →
+  IntoPersistentEnvs true (Envs Γp1 Γs1) (Envs Γp2 Enil).
+Proof. by split. Qed.
+
+Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
+  IntoPersistentEnvs p Δ1 Δ2 → Δ1 ⊢ (if p then ■ Δ2 else □ Δ2).
+Proof.
+  rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
+  apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
+  - destruct Hp. rewrite right_id plainly_sep plainly_pure.
+    apply sep_intro_True_l; [apply pure_intro|].
+    + destruct Hwf; constructor; eauto using Enil_wf, env_subenv_wf.
+    + rewrite persistently_elim plainly_persistently plainly_plainly.
+      by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
+  - rewrite right_id persistently_sep persistently_pure.
+    apply sep_intro_True_l; [apply pure_intro|by rewrite persistent_persistently].
+    destruct Hwf; constructor; simpl; eauto using Enil_wf.
+Qed.
+
+Lemma tac_always_intro Δ Δ' p Q Q' :
+  FromAlways p Q' Q →
+  IntoPersistentEnvs p Δ Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q'.
 Proof.
-  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
-  by apply (persistently_intro _ _).
+  intros ?? HQ. rewrite into_persistent_envs_sound -(from_always _ Q').
+  destruct p; auto using persistently_mono, plainly_mono.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :

theories/proofmode/environments.v

@@ -78,6 +78,13 @@ Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
   | env_Forall2_snoc Γ1 Γ2 i x y :
      env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y).
 
+Inductive env_subenv {A} : relation (env A) :=
+  | env_subenv_nil : env_subenv Enil Enil
+  | env_subenv_snoc Γ1 Γ2 i x :
+     env_subenv Γ1 Γ2 → env_subenv (Esnoc Γ1 i x) (Esnoc Γ2 i x)
+  | env_subenv_skip Γ1 Γ2 i y :
+     env_subenv Γ1 Γ2 → env_subenv Γ1 (Esnoc Γ2 i y).
+
 Section env.
 Context {A : Type}.
 Implicit Types Γ : env A.
@@ -191,4 +198,12 @@ Proof. by induction 1; simplify. Qed.
 Lemma env_Forall2_wf {B} (P : A → B → Prop) Γ Σ :
   env_Forall2 P Γ Σ → env_wf Γ → env_wf Σ.
 Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed.
+
+Lemma env_subenv_fresh Γ Σ i : env_subenv Γ Σ → Σ !! i = None → Γ !! i = None.
+Proof. by induction 1; simplify. Qed.
+Lemma env_subenv_wf Γ Σ : env_subenv Γ Σ → env_wf Σ → env_wf Γ.
+Proof. induction 1; inversion_clear 1; eauto using env_subenv_fresh. Qed.
+Global Instance env_to_list_subenv_proper :
+  Proper (env_subenv ==> sublist) (@env_to_list A).
+Proof. induction 1; simpl; constructor; auto. Qed.
 End env.

theories/proofmode/tactics.v

@@ -802,8 +802,10 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_persistently_intro; env_cbv
-    || fail "iAlways: the goal is not an persistently modality".
+  eapply tac_always_intro;
+    [apply _ || fail "iAlways: the goal is not a persistence/plainness modality"
+    |env_cbv; apply _
+    |].
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1715,6 +1717,7 @@ Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
 Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
 Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
+Hint Extern 1 (of_envs _ ⊢ ■ _) => iAlways.
 Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
 Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
 Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.