Strong framing by default for persistent hypotheses.

theories/proofmode/tactics.v

@@ -182,14 +182,19 @@ Local Ltac iFramePure t :=
     |iFrameFinish].
 
 Local Ltac iFrameHyp strong H :=
-  eapply tac_frame with _ H _ _ _;
-    [env_cbv; reflexivity || fail "iFrame:" H "not found"
+  (* Create an evar so we can remember whether the hypothesis is persistent. If
+  it is, we won't drop the hypothesis anyway, so we can use strong framing
+  safely. *)
+  let q := fresh in evar (q : bool);
+  eapply tac_frame with _ H q _ _;
+    [env_cbv; apply: reflexivity (* reflexivity fails because of the evar *)
+      || fail "iFrame:" H "not found"
     |let R := match goal with |- Frame ?R _ _ => R end in
-     lazymatch strong with
+     lazymatch eval compute in (q || strong) with
      | false => apply _
      | true => typeclasses eauto with typeclass_instances strong_frame
      end || fail "iFrame: cannot frame" R
-    |iFrameFinish].
+    |unfold q; clear q; iFrameFinish].
 
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.

theories/tests/proofmode.v

@@ -147,10 +147,10 @@ Lemma demo_17 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
 Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
 
-Lemma demo_18 (M : ucmraT) (P Q R : uPred M) :
-  P -∗ Q -∗ R -∗ (P ∗ Q ∨ R ∗ False).
+Lemma demo_18 (M : ucmraT) (P Q Q2 R : uPred M) `{!PersistentP Q2}:
+  P -∗ Q -∗ Q2 -∗ R -∗ (P ∗ Q ∗ Q2 ∨ R ∗ False).
 Proof.
-  iIntros "^$ HQ HR {^$HR}".
-  iAssert (Q ∨ False)%I with "[^$HQ]" as "[HQ|[]]".
-  iFrame "^HQ".
+  iIntros "^$ HQ1 #HQ2 HR {^$HR}".
+  iAssert (Q ∨ False)%I with "[^$HQ1]" as "[HQ1|[]]".
+  iFrame "^HQ1 HQ2".
 Qed.