Split prettification from proof mode reduction

pm_reduce just reduces away proof mode terms using cbv; pm_prettify just prettifies user-visible connectors using cbn.
Most uses of pm_default are converted to default to keep the desired reduction behavior.

tests/proofmode.ref

@@ -197,7 +197,7 @@ Tactic failure: iFrame: cannot frame Q.
   ============================
   "HPQ" : mP -∗? Q
   "HQR" : Q -∗ R
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
   --------------------------------------∗
   R
   
@@ -207,9 +207,25 @@ Tactic failure: iFrame: cannot frame Q.
   mP : option PROP
   Q, R : PROP
   ============================
-  "HP" : pm_default emp mP
+  "HP" : default emp mP
   --------------------------------------∗
-  pm_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))
+  --------------------------------------∗
+  |={E2,E1}=> True
   
 1 subgoal
   

tests/proofmode.v

@@ -544,6 +544,12 @@ Section wandM.
   Qed.
 End wandM.
 
+Definition big_op_singleton_def (P : nat → PROP) (l : list nat) :=
+  ([∗ list] n ∈ l, P n)%I.
+Lemma test_iApply_big_op_singleton (P : nat → PROP) :
+  P 1 -∗ big_op_singleton_def P [1].
+Proof. iIntros "?". iApply big_sepL_singleton. iAssumption. Qed.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)
@@ -551,6 +557,11 @@ 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) :

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. *)
 Global Instance elim_inv_acc_with_close {X : Type}
        φ1 φ2 Pinv Pin
        M1 M2 α β mγ Q Q' :

theories/proofmode/classes.v

@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
     instances to recognize the [emp] case and make it look nicer. *)
 Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
-  M1 (∃ x, α x ∗ (β x -∗ M2 (pm_default emp (mγ x))))%I.
+  M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
 
 (* Typeclass for assertions around which accessors can be elliminated.
    Inputs: [Q], [E1], [E2], [α], [β], [γ]
@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
       (Q : PROP) (Q' : X → PROP) :=
-  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (pm_default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
+  elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
 Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
 Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
 Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.

theories/proofmode/ltac_tactics.v

@@ -1108,7 +1108,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
     lazymatch pats with
     | [] =>
       lazymatch found with
-      | true => idtac
+      | true => pm_prettify (* post-tactic prettification *)
       | false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
       end
     | ISimpl :: ?pats => simpl; find_pat found pats

theories/proofmode/reduction.v

@@ -11,13 +11,13 @@ Declare Reduction pm_cbv := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
+  (* PM option combinators *)
+  pm_option_bind pm_from_option pm_option_fun
 ].
 (* Some things should only be unfolded according to cbn rules, when
    certain arguments are constructors. This is because they can appear in
    the user side of proofs as well. *)
 Declare Reduction pm_cbn := cbn [
-  (* PM option combinators *)
-  pm_option_bind pm_from_option pm_option_fun
   (* telescope combinators *)
   tele_fold tele_bind tele_app
   (* BI connectives *)
@@ -25,15 +25,17 @@ Declare Reduction pm_cbn := cbn [
   bi_wandM sbi_laterN
   bi_tforall bi_texist
 ].
+
+(** Called by all tactics to perform computation to lookup items in the
+    context.  We avoid reducing anything user-visible here to make sure we
+    do not reduce e.g. before unification happens in [iApply].*)
 Ltac pm_eval t :=
-  let u := eval pm_cbv in t in
-  let v := eval pm_cbn in u in
-  v.
+  eval pm_cbv in t.
 Ltac pm_reduce :=
   match goal with |- ?u => let v := pm_eval u in change v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
 
-(** Called e.g. by iApply for redexes that are created by instantiation.
-    This cannot create any envs redexes so we just to the cbn part. *)
+(** Called by many tactics for redexes that are created by instantiation.
+    This cannot create any envs redexes so we just do the cbn part. *)
 Ltac pm_prettify :=
   match goal with |- ?u => let v := eval pm_cbn in u in change v end.