More consistent behavior of `#H` when the source is already in the

persistent context.

Given the source does not contain a box:

- Before: no-op if there is a Persistent instance.
- Now: no-op in all cases.

theories/proofmode/class_instances.v

@@ -140,13 +140,13 @@ Proof.
 Qed.
 
 (* IntoPersistentP *)
-Global Instance into_persistentP_always_trans P Q :
-  IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP (□ P) P | 1.
+Global Instance into_persistentP_always_trans p P Q :
+  IntoPersistentP true P Q → IntoPersistentP p (□ P) Q | 0.
+Proof. rewrite /IntoPersistentP /==> ->. by rewrite always_if_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP true P P | 1.
 Proof. done. Qed.
 Global Instance into_persistentP_persistent P :
-  PersistentP P → IntoPersistentP P P | 100.
+  PersistentP P → IntoPersistentP false P P | 100.
 Proof. done. Qed.
 
 (* IntoLater *)

theories/proofmode/classes.v

@@ -27,9 +27,10 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
-Class IntoPersistentP {M} (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
-Arguments into_persistentP {_} _ _ {_}.
-Hint Mode IntoPersistentP + ! - : typeclass_instances.
+Class IntoPersistentP {M} (p : bool) (P Q : uPred M) :=
+  into_persistentP : □?p P ⊢ □ Q.
+Arguments into_persistentP {_} _ _ _ {_}.
+Hint Mode IntoPersistentP + + ! - : typeclass_instances.
 
 (* The class [IntoLaterN] has only two instances:
 

theories/proofmode/coq_tactics.v

@@ -482,12 +482,13 @@ Proof.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
-  envs_lookup i Δ = Some (p, P) → IntoPersistentP P P' →
+  envs_lookup i Δ = Some (p, P) →
+  IntoPersistentP p P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ??? <-. rewrite envs_replace_sound //; simpl.
-  by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
+  intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
+  by rewrite right_id (into_persistentP _ P) wand_elim_r.
 Qed.
 
 (** * Implication and wand *)
@@ -503,12 +504,13 @@ Proof.
     by rewrite always_and_sep_l right_id wand_elim_r.
 Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP P P' →
+  IntoPersistentP false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P → Q.
 Proof.
-  intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
-  by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
+  intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
+  rewrite (_ : P = □?false P) // (into_persistentP false P).
+  by rewrite right_id always_and_sep_l wand_elim_r.
 Qed.
 Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
   (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
@@ -526,7 +528,7 @@ Proof.
   intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
-  IntoPersistentP P P' →
+  IntoPersistentP false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.

theories/proofmode/tactics.v

@@ -160,7 +160,7 @@ Local Tactic Notation "iPersistent" constr(H) :=
   eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
     [env_reflexivity || fail "iPersistent:" H "not found"
     |apply _ ||
-     let Q := match goal with |- IntoPersistentP ?Q _ => Q end in
+     let Q := match goal with |- IntoPersistentP _ ?Q _ => Q end in
      fail "iPersistent:" Q "not persistent"
     |env_reflexivity|].
 
@@ -317,14 +317,14 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   [ (* (?P → _) *)
     eapply tac_impl_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP ?P _ => P end in
+       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
   | (* (?P -∗ _) *)
     eapply tac_wand_intro_persistent with _ H _; (* (i:=H) *)
       [apply _ || 
-       let P := match goal with |- IntoPersistentP ?P _ => P end in
+       let P := match goal with |- IntoPersistentP _ ?P _ => P end in
        fail 1 "iIntro: " P " not persistent"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]

theories/tests/proofmode.v

@@ -8,9 +8,9 @@ Implicit Types P Q R : uPred M.
 
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
-  iIntros "#H #H2".
+  iIntros "###H #H2".
   (* should remove the disjunction "H" *)
-  iDestruct "H" as "[?|?]"; last by iLeft.
+  iDestruct "H" as "[#?|#?]"; last by iLeft.
   (* should keep the disjunction "H" because it is instantiated *)
   iDestruct ("H2" $! 10) as "[%|%]". done. done.
 Qed.