make pm_maybe_wand a BI connective; reduce BI connectives and option...

make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn

tests/proofmode.ref

@@ -114,6 +114,52 @@ Tactic failure: iFrame: cannot frame Q.
   --------------------------------------∗
   <absorb> Φ x1 x2
   
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : □ True
+  --------------------------------------∗
+  True
+  
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : emp
+  --------------------------------------□
+  □ emp
+  
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : emp
+  --------------------------------------□
+  □ emp
+  
+1 subgoal
+  
+  PROP : sbi
+  mP : option PROP
+  Q, R : PROP
+  ============================
+  "HPQ" : mP -∗? Q
+  "HQR" : Q -∗ R
+  "HP" : pm_default emp mP
+  --------------------------------------∗
+  R
+  
+1 subgoal
+  
+  PROP : sbi
+  mP : option PROP
+  Q, R : PROP
+  ============================
+  "HP" : pm_default emp mP
+  --------------------------------------∗
+  pm_default emp mP
+  
 1 subgoal
   
   PROP : sbi

tests/proofmode.v

@@ -508,6 +508,43 @@ Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
   Φ 0 10 -∗ ([∗ list] y1;y2 ∈ l1;l2, Φ y1 y2) -∗
   ([∗ list] y1;y2 ∈ (0 :: l1);(10 :: l2), Φ y1 y2).
 Proof. iIntros "$ ?". iFrame. Qed.
+
+Lemma test_lemma_1 (b : bool) :
+  emp ⊢@{PROP} □?b True.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iDestruct : emp ⊢@{PROP} True.
+Proof.
+  iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
+Qed.
+
+Lemma test_lemma_2 (b : bool) :
+  □?b emp ⊢@{PROP} emp.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iApply : emp ⊢@{PROP} emp.
+Proof.
+  iIntros "#H". iApply (test_lemma_2 true). Show. auto.
+Qed.
+
+Lemma test_lemma_3 (b : bool) :
+  □?b emp ⊢@{PROP} ⌜b = b⌝.
+Proof. destruct b; simpl; eauto. Qed.
+Lemma test_reducing_after_iApply_late_evar : emp ⊢@{PROP} ⌜true = true⌝.
+Proof.
+  iIntros "#H". iApply (test_lemma_3). Show. auto.
+Qed.
+
+Section wandM.
+Import proofmode.base.
+Lemma test_wandM mP Q R :
+  (mP -∗? Q) -∗ (Q -∗ R) -∗ (mP -∗? R).
+Proof.
+  iIntros "HPQ HQR HP". Show.
+  iApply "HQR". iApply "HPQ". Show.
+  done.
+Qed.
+
+End wandM.
+
 End tests.
 
 (** Test specifically if certain things print correctly. *)

theories/bi/derived_connectives.v

@@ -106,3 +106,15 @@ Arguments Timeless {_} _%I : simpl never.
 Arguments timeless {_} _%I {_}.
 Hint Mode Timeless + ! : typeclass_instances.
 Instance: Params (@Timeless) 1.
+
+(** An optional precondition [mP] to [Q].
+    TODO: We may actually consider generalizing this to a list of preconditions,
+    and e.g. also using it for texan triples. *)
+Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
+  match mP with
+  | None => Q
+  | Some P => (P -∗ Q)%I
+  end.
+Arguments bi_wandM {_} !_%I _%I /.
+Notation "mP -∗? Q" := (bi_wandM mP Q)
+  (at level 99, Q at level 200, right associativity) : bi_scope.

theories/bi/derived_laws_bi.v

@@ -460,6 +460,10 @@ Proof.
   - rewrite !and_elim_r wand_elim_r. done.
 Qed.
 
+Lemma wandM_sound (mP : option PROP) Q :
+  (mP -∗? Q) ⊣⊢ (default emp mP -∗ Q).
+Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
+
 (* Pure stuff *)
 Lemma pure_elim φ Q R : (Q ⊢ ⌜φ⌝) → (φ → Q ⊢ R) → Q ⊢ R.
 Proof.

theories/bi/lib/atomic.v

@@ -160,8 +160,8 @@ Section lemmas.
   Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X → PROP) γ' α β Pas Φ :
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
             (atomic_acc E1 Ei α Pas β Φ)
-            (λ x', atomic_acc E2 Ei α (β' x' ∗ pm_maybe_wand (γ' x') Pas)%I β
-                (λ x y, β' x' ∗ pm_maybe_wand (γ' x') (Φ x y)))%I.
+            (λ x', atomic_acc E2 Ei α (β' x' ∗ (γ' x' -∗? Pas))%I β
+                (λ x y, β' x' ∗ (γ' x' -∗? Φ x y)))%I.
   Proof.
     rewrite /ElimAcc.
     (* FIXME: Is there any way to prevent maybe_wand from unfolding?

theories/program_logic/weakestpre.v

 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
 From iris.bi Require Export weakestpre.
-From iris.proofmode Require Import tactics classes.
+From iris.proofmode Require Import base tactics classes.
 Set Default Proof Using "Type".
 Import uPred.
 
@@ -270,9 +270,9 @@ Section proofmode_classes.
     Atomic (stuckness_to_atomicity s) e →
     ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
             α β γ (WP e @ s; E1 {{ Φ }})
-            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E2 {{ v, |={E2}=> β x ∗ (γ x -∗? Φ v) }})%I.
   Proof.
-    intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
+    intros ?. rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
     iIntros (v) ">[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
@@ -281,9 +281,9 @@ Section proofmode_classes.
   Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
     ElimAcc (X:=X) (fupd E E) (fupd E E)
             α β γ (WP e @ s; E {{ Φ }})
-            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
+            (λ x, WP e @ s; E {{ v, |={E}=> β x ∗ (γ x -∗? Φ v) }})%I.
   Proof.
-    rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
+    rewrite /ElimAcc.
     iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
     iApply wp_fupd.
     iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".

theories/proofmode/class_instances_bi.v

@@ -340,6 +340,16 @@ Global Instance from_modal_bupd `{BiBUpd PROP} P :
 Proof. by rewrite /FromModal /= -bupd_intro. Qed.
 
 (** IntoWand *)
+Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
+  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
+Proof. done. Qed.
+Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
+  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
+Proof. done. Qed.
+Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
+  IntoWand' p q (mP -∗? Q) P' Q' → IntoWand p q (mP -∗? Q) P' Q' | 100.
+Proof. done. Qed.
+
 Global Instance into_wand_wand p q P Q P' :
   FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.
 Proof.
@@ -374,6 +384,10 @@ Proof.
   rewrite sep_and [(□ (_ → _))%I]intuitionistically_elim impl_elim_r //.
 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.
+Proof. rewrite /IntoWand wandM_sound. exact: into_wand_wand. Qed.
+
 Global Instance into_wand_and_l p q R1 R2 P' Q' :
   IntoWand p q R1 P' Q' → IntoWand p q (R1 ∧ R2) P' Q'.
 Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_l. Qed.
@@ -491,6 +505,9 @@ Qed.
 (** FromWand *)
 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.
+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⎤.
 Proof. by rewrite /FromWand -embed_wand => <-. Qed.
@@ -974,6 +991,10 @@ Proof.
   rewrite /ElimModal=> H Hφ. apply wand_intro_r.
   rewrite wand_curry -assoc (comm _ (□?p' _)%I) -wand_curry wand_elim_l; auto.
 Qed.
+Global Instance elim_modal_wandM φ p p' P P' Q Q' mR :
+  ElimModal φ p p' P P' Q Q' →
+  ElimModal φ p p' P P' (mR -∗? Q) (mR -∗? Q').
+Proof. rewrite /ElimModal !wandM_sound. exact: elim_modal_wand. Qed.
 Global Instance elim_modal_forall {A} φ p p' P P' (Φ Ψ : A → PROP) :
   (∀ x, ElimModal φ p p' P P' (Φ x) (Ψ x)) → ElimModal φ p p' P P' (∀ x, Φ x) (∀ x, Ψ x).
 Proof.
@@ -1011,6 +1032,9 @@ Proof.
   rewrite /AddModal=> H. apply wand_intro_r.
   by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
 Qed.
+Global Instance add_modal_wandM P P' Q mR :
+  AddModal P P' Q → AddModal P P' (mR -∗? Q).
+Proof. rewrite /AddModal wandM_sound. exact: add_modal_wand. Qed.
 Global Instance add_modal_forall {A} P P' (Φ : A → PROP) :
   (∀ x, AddModal P P' (Φ x)) → AddModal P P' (∀ x, Φ x).
 Proof.

theories/proofmode/class_instances_sbi.v

 From stdpp Require Import nat_cancel.
 From iris.bi Require Import bi tactics.
-From iris.proofmode Require Import modality_instances classes class_instances_bi coq_tactics ltac_tactics.
+From iris.proofmode Require Import base modality_instances classes class_instances_bi ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
 
@@ -499,9 +499,9 @@ Global Instance elim_acc_fupd `{BiFUpd PROP} {X} E1 E2 E α β mγ Q :
   (* FIXME: Why %I? ElimAcc sets the right scopes! *)
   ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α β mγ
           (|={E1,E}=> Q)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q)))%I.
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q))%I.
 Proof.
-  rewrite /ElimAcc. setoid_rewrite pm_maybe_wand_sound.
+  rewrite /ElimAcc.
   iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
   iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
   iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".

theories/proofmode/classes.v

@@ -161,13 +161,6 @@ Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
 Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
 Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
 
-Instance into_wand_wand' {PROP : bi} p q (P Q P' Q' : PROP) :
-  IntoWand' p q (P -∗ Q) P' Q' → IntoWand p q (P -∗ Q) P' Q' | 100.
-Proof. done. Qed.
-Instance into_wand_impl' {PROP : bi} p q (P Q P' Q' : PROP) :
-  IntoWand' p q (P → Q) P' Q' → IntoWand p q (P → Q) P' Q' | 100.
-Proof. done. Qed.
-
 Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
 Arguments FromWand {_} _%I _%I _%I : simpl never.
 Arguments from_wand {_} _%I _%I _%I {_}.

theories/proofmode/coq_tactics.v

@@ -7,8 +7,6 @@ Import env_notations.
 
 Local Notation "b1 && b2" := (if b1 then b2 else false) : bool_scope.
 
-Notation pm_maybe_wand mP Q := (pm_from_option (λ P, P -∗ Q)%I Q%I mP).
-
 (* Coq versions of the tactics *)
 Section bi_tactics.
 Context {PROP : bi}.
@@ -336,10 +334,6 @@ Proof.
   - rewrite /= IH (comm _ Q _) assoc. done.
 Qed.
 
-Lemma pm_maybe_wand_sound mP Q :
-  pm_maybe_wand mP Q ⊣⊢ (default emp mP -∗ Q).
-Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
-
 Global Instance envs_Forall2_refl (R : relation PROP) :
   Reflexive R → Reflexive (envs_Forall2 R).
 Proof. by constructor. Qed.
@@ -996,7 +990,7 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
   (∀ R, ∃ Δ'',
     envs_app false (Esnoc Enil j
       (Pin -∗
-       (∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)) -∗
+       (∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x) -∗
        R
       )%I) Δ'
       = Some Δ'' ∧

theories/proofmode/ltac_tactics.v

@@ -2007,7 +2007,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
      iSpecializePat H pats; last (
        iApplyHyp H; clear R; pm_reduce;
        (* Now the goal is
-          [∀ x, Pout x -∗ pm_maybe_wand (pm_option_fun Pclose x) (Q' x)],
+          [∀ x, Pout x -∗ pm_option_fun Pclose x -∗? Q' x],
           reduced because we can rely on Pclose being a constructor. *)
        let x := fresh in
        iIntros (x);

theories/proofmode/monpred.v

 From iris.bi Require Export monpred.
 From iris.bi Require Import plainly.
-From iris.proofmode Require Import tactics modality_instances coq_tactics.
+From iris.proofmode Require Import tactics modality_instances.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
@@ -557,12 +557,11 @@ Proof. by rewrite /MakeMonPredAt /ElimModal monPred_at_fupd=><-. Qed.
 Global Instance elim_acc_at_fupd `{BiFUpd PROP} {X : Type} E1 E2 E
        M1 M2 α β (mγ : X → option PROP) Q (Q' : X → monPred) i :
   ElimAcc (X:=X) M1 M2 α β mγ (|={E1,E}=> Q i)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' x i)))%I →
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q' x i))%I →
   ElimAcc (X:=X) M1 M2 α β mγ ((|={E1,E}=> Q) i)
           (λ x, (|={E2}=> ⎡β x⎤ ∗
-                         (pm_maybe_wand
-                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
-                            (|={E1,E}=> Q' x))) i)%I
+                         (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end -∗?
+                            |={E1,E}=> Q' x)) i)%I
   | 1.
 Proof.
   rewrite /ElimAcc monPred_at_fupd=><-. apply bi.forall_mono=>x.
@@ -575,12 +574,11 @@ fails. *)
 Global Instance elim_acc_at_fupd_unit `{BiFUpd PROP} E1 E2 E
        M1 M2 α β mγ Q Q' i :
   ElimAcc (X:=unit) M1 M2 α β mγ (|={E1,E}=> Q i)
-          (λ x, |={E2}=> β x ∗ (pm_maybe_wand (mγ x) (|={E1,E}=> Q' i)))%I →
+          (λ x, |={E2}=> β x ∗ (mγ x -∗? |={E1,E}=> Q' i))%I →
   ElimAcc (X:=unit) M1 M2 α β mγ ((|={E1,E}=> Q) i)
           (λ x, (|={E2}=> ⎡β x⎤ ∗
-                         (pm_maybe_wand
-                            (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end)
-                            (|={E1,E}=> Q'))) i)%I
+                         (match mγ x with Some 𝓟 => Some ⎡𝓟⎤ | None => None end -∗?
+                            |={E1,E}=> Q')) i)%I
   | 0.
 Proof. exact: elim_acc_at_fupd. Qed.
 

theories/proofmode/reduction.v

@@ -3,7 +3,6 @@ From iris.proofmode Require Import base environments.
 
 Declare Reduction pm_cbv := cbv [
   (* base *)
-  pm_option_bind pm_from_option pm_option_fun
   base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
   (* environments *)
   env_lookup env_lookup_delete env_delete env_app env_replace
@@ -13,9 +12,20 @@ Declare Reduction pm_cbv := cbv [
   envs_clear_spatial envs_clear_persistent envs_incr_counter
   envs_split_go envs_split prop_of_env
 ].
+(* 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
+  (* BI connectives *)
+  bi_persistently_if bi_affinely_if bi_intuitionistically_if
+  bi_wandM
+].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in
-  u.
+  let v := eval pm_cbn in u in
+  v.
 Ltac pm_reduce :=
   match goal with |- ?u => let v := pm_eval u in change v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.