Merge branch 'ralf/pm' into 'gen_proofmode'

Split prettification from proof mode reduction

See merge request FP/iris-coq!170

tests/proofmode.ref

+"demo_0"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -19,6 +21,8 @@
   --------------------------------------□
   Q ∨ P
   
+"test_iDestruct_and_emp"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -59,6 +63,8 @@ In nested Ltac calls to "iSpecialize (open_constr)",
 "iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
 failed.
 Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
+"test_iNext_plus_3"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -68,6 +74,8 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ▷^(S n + S m) emp
   
+"test_iFrame_later_1"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -76,6 +84,8 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
   --------------------------------------∗
   ▷ emp
   
+"test_iFrame_later_2"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -89,6 +99,8 @@ In nested Ltac calls to "iFrame (constr)",
 "<iris.proofmode.ltac_tactics.iFrame_go>" and
 "<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
 Tactic failure: iFrame: cannot frame Q.
+"test_and_sep_affine_bi"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -100,6 +112,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   □ P
   
+"test_big_sepL_simpl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -126,6 +140,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P
   
+"test_big_sepL2_simpl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -153,6 +169,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
   
+"test_big_sepL2_iDestruct"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -165,6 +183,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   <absorb> Φ x1 x2
   
+"test_reducing_after_iDestruct"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -173,6 +193,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"test_reducing_after_iApply"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -181,6 +203,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------□
   □ emp
   
+"test_reducing_after_iApply_late_evar"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -189,6 +213,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------□
   □ emp
   
+"test_wandM"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -197,7 +223,7 @@ Tactic failure: iFrame: cannot frame Q.
   ============================
   "HPQ" : mP -∗? Q
   "HQR" : Q -∗ R
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
   --------------------------------------∗
   R
   
@@ -207,10 +233,28 @@ Tactic failure: iFrame: cannot frame Q.
   mP : option PROP
   Q, R : PROP
   ============================
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
+  --------------------------------------∗
+  default emp mP
+  
+"elim_mod_accessor"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : Type
+  E1, E2 : coPset.coPset
+  α : X → PROP
+  β : X → PROP
+  γ : X → option PROP
+  ============================
+  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
   --------------------------------------∗
-  pm_default emp mP
+  |={E2,E1}=> True
   
+"print_long_line_1"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -233,6 +277,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"print_long_line_2"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -255,6 +301,8 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   True
   
+"long_impl"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -265,6 +313,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_impl_nested"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -276,6 +326,8 @@ Tactic failure: iFrame: cannot frame Q.
   → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
     → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_wand"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -286,6 +338,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_wand_nested"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -297,6 +351,8 @@ Tactic failure: iFrame: cannot frame Q.
   -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
      -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_fupd"
+     : string
 1 subgoal
   
   PROP : sbi
@@ -308,6 +364,8 @@ Tactic failure: iFrame: cannot frame Q.
   PPPPPPPPPPPPPPPPP
   ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"long_fupd_nested"
+     : string
 1 subgoal
   
   PROP : sbi

tests/proofmode.v

@@ -6,6 +6,7 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Check "demo_0".
 Lemma demo_0 P Q : □ (P ∨ Q) -∗ (∀ x, ⌜x = 0⌝ ∨ ⌜x = 1⌝) → (Q ∨ P).
 Proof.
   iIntros "H #H2". Show. iDestruct "H" as "###H".
@@ -52,6 +53,7 @@ Proof.
   auto.
 Qed.
 
+Check "test_iDestruct_and_emp".
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
 Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
@@ -365,6 +367,7 @@ Lemma test_iNext_plus_1 P n1 n2 : ▷ ▷^n1 ▷^n2 P -∗ ▷^n1 ▷^n2 ▷ P.
 Proof. iIntros "H". iNext. iNext. by iNext. Qed.
 Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
 Proof. iIntros "H". iNext. done. Qed.
+Check "test_iNext_plus_3".
 Lemma test_iNext_plus_3 P Q n m k :
   ▷^m ▷^(2 + S n + k) P -∗ ▷^m ▷ ▷^(2 + S n) Q -∗ ▷^k ▷ ▷^(S (S n + S m)) (P ∗ Q).
 Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
@@ -408,9 +411,11 @@ Lemma test_iPureIntro_absorbing (φ : Prop) :
   φ → sbi_emp_valid (PROP:=PROP) (<absorb> ⌜φ⌝)%I.
 Proof. intros ?. iPureIntro. done. Qed.
 
+Check "test_iFrame_later_1".
 Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
+Check "test_iFrame_later_2".
 Lemma test_iFrame_later_2 P Q : ▷ P ∗ ▷ Q -∗ ▷ (▷ P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". Show. auto. Qed.
 
@@ -480,11 +485,13 @@ Proof.
   - iDestruct "H" as "[_ [_ #$]]".
 Qed.
 
+Check "test_and_sep_affine_bi".
 Lemma test_and_sep_affine_bi `{BiAffine PROP} P Q : □ P ∧ Q ⊢ □ P ∗ Q.
 Proof.
   iIntros "[??]". iSplit; last done. Show. done.
 Qed.
 
+Check "test_big_sepL_simpl".
 Lemma test_big_sepL_simpl x (l : list nat) P :
    P -∗
   ([∗ list] k↦y ∈ l, <affine> ⌜ y = y ⌝) -∗
@@ -492,6 +499,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
   P.
 Proof. iIntros "HP ??". Show. simpl. Show. done. Qed.
 
+Check "test_big_sepL2_simpl".
 Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P -∗
   ([∗ list] k↦y1;y2 ∈ []; l2, <affine> ⌜ y1 = y2 ⌝) -∗
@@ -499,6 +507,7 @@ Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
   P ∨ ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, True).
 Proof. iIntros "HP ??". Show. simpl. Show. by iLeft. Qed.
 
+Check "test_big_sepL2_iDestruct".
 Lemma test_big_sepL2_iDestruct (Φ : nat → nat → PROP) x1 x2 (l1 l2 : list nat) :
   ([∗ list] y1;y2 ∈ x1 :: l1; x2 :: l2, Φ y1 y2) -∗
   <absorb> Φ x1 x2.
@@ -512,6 +521,7 @@ Proof. iIntros "$ ?". iFrame. Qed.
 Lemma test_lemma_1 (b : bool) :
   emp ⊢@{PROP} □?b True.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iDestruct".
 Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True.
 Proof.
   iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
@@ -520,6 +530,7 @@ Qed.
 Lemma test_lemma_2 (b : bool) :
   □?b emp ⊢@{PROP} emp.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iApply".
 Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp.
 Proof.
   iIntros "#H". iApply (test_lemma_2 true). Show. auto.
@@ -528,6 +539,7 @@ Qed.
 Lemma test_lemma_3 (b : bool) :
   □?b emp ⊢@{PROP} ⌜b = b⌝.
 Proof. destruct b; simpl; eauto. Qed.
+Check "test_reducing_after_iApply_late_evar".
 Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝.
 Proof.
   iIntros "#H". iApply (test_lemma_3). Show. auto.
@@ -535,6 +547,7 @@ Qed.
 
 Section wandM.
   Import proofmode.base.
+  Check "test_wandM".
   Lemma test_wandM mP Q R :
     (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
   Proof.
@@ -544,6 +557,27 @@ Section wandM.
   Qed.
 End wandM.
 
+Definition modal_if_def b (P : PROP) :=
+  (□?b P)%I.
+Lemma modal_if_lemma1 b P :
+  False -∗ □?b P.
+Proof. iIntros "?". by iExFalso. Qed.
+Lemma test_iApply_prettification1 (P : PROP) :
+  False -∗ modal_if_def true P.
+Proof.
+  (* Make sure the goal is not prettified before [iApply] unifies. *)
+  iIntros "?". rewrite /modal_if_def. iApply modal_if_lemma1. iAssumption.
+Qed.
+Lemma modal_if_lemma2 P :
+  False -∗ □?false P.
+Proof. iIntros "?". by iExFalso. Qed.
+Lemma test_iApply_prettification2 (P  : PROP) :
+  False -∗ ∃ b, □?b P.
+Proof.
+  (* Make sure the conclusion of the lemma is not prettified too early. *)
+  iIntros "?". iExists _. iApply modal_if_lemma2. done.
+Qed.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)
@@ -551,9 +585,15 @@ Section printing_tests.
 Context {PROP : sbi} `{!BiFUpd PROP}.
 Implicit Types P Q R : PROP.
 
+Check "elim_mod_accessor".
+Lemma elim_mod_accessor {X : Type} E1 E2 α (β : X → PROP) γ :
+  accessor (fupd E1 E2) (fupd E2 E1) α β γ -∗ |={E1}=> True.
+Proof. iIntros ">Hacc". Show. Abort.
+
 (* Test line breaking of long assumptions. *)
 Section linebreaks.
-Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
+Check "print_long_line_1".
+Lemma print_long_line_1 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
   P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
   -∗ True.
@@ -565,38 +605,45 @@ Abort.
    the proofmode notation breaks the output. *)
 Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I
   (format "'TESTNOTATION'  '{{'  P  '|'  '/' Q  '}' '}'") : bi_scope.
-Lemma print_long_line (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
+Check "print_long_line_2".
+Lemma print_long_line_2 (P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP) :
   TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P | P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
   -∗ True.
 Proof.
   iIntros "HP". Show. Undo. iIntros "?". Show.
 Abort.
 
+Check "long_impl".
 Lemma long_impl (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_impl_nested".
 Lemma long_impl_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) → (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_wand".
 Lemma long_wand (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_wand_nested".
 Lemma long_wand_nested (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   (PPPPPPPPPPPPPPPPP -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ) -∗ (QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ))%I.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_fupd".
 Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
 Proof.
   iStartProof. Show.
 Abort.
+Check "long_fupd_nested".
 Lemma long_fupd_nested E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
   PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.

theories/proofmode/class_instances_bi.v

@@ -385,7 +385,7 @@ Proof.
 Qed.
 
 Global Instance into_wand_wandM p q mP' P Q :
-  FromAssumption q P (pm_default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
+  FromAssumption q P (default emp%I mP') → IntoWand p q (mP' -∗? Q) P Q.
 Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.
 
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
@@ -510,7 +510,7 @@ Qed.
 Global Instance from_wand_wand P1 P2 : FromWand (P1 -∗ P2) P1 P2.
 Proof. by rewrite /FromWand. Qed.
 Global Instance from_wand_wandM mP1 P2 :
-  FromWand (mP1 -∗? P2) (pm_default emp mP1)%I P2.
+  FromWand (mP1 -∗? P2) (default emp mP1)%I P2.
 Proof. by rewrite /FromWand wandM_sound. Qed.
 Global Instance from_wand_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
   FromWand P Q1 Q2 → FromWand ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
@@ -1079,6 +1079,9 @@ Proof.
   - iApply (Hacc with "Hinv Hin"). done.
 Qed.
 
+(* This uses [pm_default] because, after inference, all accessors will have
+[None] or [Some _] there, so we want to reduce the combinator before showing the
+goal to the user. *)