From 0832d21f1cf7e044da85a5eeee0bf21634f59cb6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 24 Oct 2017 00:11:57 +0200
Subject: [PATCH] Proofmode support for introducing the plain modality.

---
 ProofMode.md                         |  4 ++-
 theories/proofmode/class_instances.v |  6 ++++
 theories/proofmode/classes.v         |  5 +++
 theories/proofmode/coq_tactics.v     | 54 +++++++++++++++++++++++++---
 theories/proofmode/environments.v    | 15 ++++++++
 theories/proofmode/tactics.v         |  7 ++--
 6 files changed, 84 insertions(+), 7 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 2eaab453a..6830f61ef 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -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 always or plain modality and clear the spatial context.
+  In case of a plain modality, it will prune all persistent hypotheses that are
+  not plain.
 - `!>` : introduce a modality.
 - `/=` : perform `simpl`.
 - `//` : perform `try done` on all goals.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 1203e90a4..7c2e77980 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -156,6 +156,12 @@ Global Instance into_persistentP_persistent P :
   PersistentP P → IntoPersistentP false P P | 100.
 Proof. done. Qed.
 
+(* FromPersistentP *)
+Global Instance from_persistentP_always P : FromPersistentP false (â–¡ P) P.
+Proof. by rewrite /FromPersistentP. Qed.
+Global Instance from_persistentP_plainly P : FromPersistentP true (☃ P) P.
+Proof. by rewrite /FromPersistentP. Qed.
+
 (* IntoLater *)
 Global Instance into_laterN_later n P Q :
   IntoLaterN n P Q → IntoLaterN' (S n) (▷ P) Q.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index ebdb8144e..80a5bc024 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -32,6 +32,11 @@ Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
 Arguments into_persistentP {_} _ _ _ {_}.
 Hint Mode IntoPersistentP + + ! - : typeclass_instances.
 
+Class FromPersistentP {M} (p : bool) (P Q : uPred M) :=
+  from_persistentP : (if p then ☃ Q else □ Q) ⊢ P.
+Arguments from_persistentP {_} _ _ _ {_}.
+Hint Mode FromPersistentP + - ! - : typeclass_instances.
+
 (* The class [IntoLaterN] has only two instances:
 
 - The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index f52984b25..bd1a3962c 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -474,11 +474,57 @@ Proof.
 Qed.
 
 (** * Always *)
-Lemma tac_always_intro Δ Q :
-  (envs_clear_spatial Δ ⊢ Q) → Δ ⊢ □ Q.
+Class IntoPlainEnv (Γ1 Γ2 : env (uPred M)) := {
+  into_plain_env_subenv : env_subenv Γ2 Γ1;
+  into_plain_env_plain : PlainP ([∗] Γ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 :
+  PlainP 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 always_elim plainly_always plainly_plainly.
+      by apply big_sepL_submseteq, sublist_submseteq, env_to_list_subenv_proper.
+  - rewrite right_id always_sep always_pure.
+    apply sep_intro_True_l; [apply pure_intro|by rewrite always_always].
+    destruct Hwf; constructor; simpl; eauto using Enil_wf.
+Qed.
+
+Lemma tac_always_intro Δ Δ' p Q Q' :
+  FromPersistentP p Q' Q →
+  IntoPersistentEnvs p Δ Δ' →
+  (Δ' ⊢ Q) → Δ ⊢ Q'.
 Proof.
-  intros <-. rewrite envs_clear_spatial_sound sep_elim_l.
-  by apply (always_intro _ _).
+  intros ?? HQ. rewrite into_persistent_envs_sound -(from_persistentP _ Q').
+  destruct p; auto using always_mono, plainly_mono.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 8ed1a9bf6..a96b0c84e 100644
--- a/theories/proofmode/environments.v
+++ b/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.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7d01214b8..ded603032 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -808,8 +808,10 @@ Local Tactic Notation "iExistDestruct" constr(H)
 (** * Always *)
 Tactic Notation "iAlways":=
   iStartProof;
-  apply tac_always_intro; env_cbv
-    || fail "iAlways: the goal is not an always modality".
+  eapply tac_always_intro;
+    [apply _ || fail "iAlways: the goal is not an always modality"
+    |env_cbv; apply _
+    |].
 
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
@@ -1721,6 +1723,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.
-- 
GitLab