Merge branch 'ralf/soundness' into 'master'

Nicer soundness for our update modalities

See merge request iris/iris!230

theories/base_logic/bi.v

@@ -206,13 +206,15 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
 Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness_pure φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
-Proof. apply soundness_pure. Qed.
+Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
+Proof. apply pure_soundness. Qed.
 
-Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
-Proof. apply soundness_later. Qed.
+Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
+Proof. apply later_soundness. Qed.
+(** See [derived.v] for a similar soundness result for basic updates. *)
 End restate.
 
+
 (** New unseal tactic that also unfolds the BI layer.
     This is used by [base_logic.double_negation].
     TODO: Can we get rid of this? *)

theories/base_logic/derived.v

@@ -92,11 +92,17 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
+Lemma bupd_plain_soundness P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P.
+Proof.
+  eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
+  apply: plain.
+Qed.
+
 Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
 Proof.
   induction n as [|n IH]=> /=.
-  - apply soundness_pure.
-  - intros H. by apply IH, soundness_later.
+  - apply pure_soundness.
+  - intros H. by apply IH, later_soundness.
 Qed.
 
 Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.

theories/base_logic/lib/fancy_updates.v

@@ -59,11 +59,12 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness `{!invPreG Σ} E (P: iProp Σ) `{!Plain P}:
-  (∀ `{Hinv: !invG Σ}, (|={⊤,E}=> P)%I) → (▷ P)%I.
+Lemma fupd_plain_soundness `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
+  (∀ `{Hinv: !invG Σ}, bi_emp_valid (|={E1,E2}=> P)) → bi_emp_valid P.
 Proof.
-  iIntros (Hfupd). iMod wsat_alloc as (Hinv) "[Hw HE]".
-  iPoseProof (Hfupd Hinv) as "H".
+  iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
+  iAssert (|={⊤,E2}=> P)%I as "H".
+  { iMod fupd_intro_mask'; last iApply Hfupd. done. }
   rewrite uPred_fupd_eq /uPred_fupd_def.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
@@ -73,8 +74,8 @@ Lemma step_fupdN_soundness `{!invPreG Σ} φ n :
   φ.
 Proof.
   intros Hiter.
-  apply (soundness (M:=iResUR Σ) _  (S (S n))); simpl.
-  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  apply (soundness (M:=iResUR Σ) _  (S n)); simpl.
+  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iPoseProof (Hiter Hinv) as "H". clear Hiter.
   destruct n as [|n].
   - iApply fupd_plainly_mask_empty. iMod "H" as %?; auto.

theories/base_logic/upred.v

@@ -801,10 +801,10 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness_pure φ : (True ⊢ ⌜ φ ⌝) → φ.
+Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
 Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
 
-Lemma soundness_later P : (True ⊢ ▷ P) → (True ⊢ P).
+Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
   unseal=> -[HP]; split=> n x Hx _.
   apply uPred_mono with n ε; eauto using ucmra_unit_leastN.

theories/program_logic/total_adequacy.v

@@ -123,8 +123,8 @@ Theorem twp_total Σ Λ `{!invPreG Σ} s e σ Φ :
        stateI σ [] 0 ∗ WP e @ s; ⊤ [{ Φ }])%I) →
   sn erased_step ([e], σ). (* i.e. ([e], σ) is strongly normalizing *)
 Proof.
-  intros Hwp. apply (soundness (M:=iResUR Σ) _  2); simpl.
-  apply (fupd_plain_soundness ⊤ _)=> Hinv.
+  intros Hwp. apply (soundness (M:=iResUR Σ) _  1); simpl.
+  apply (fupd_plain_soundness ⊤ ⊤ _)=> Hinv.
   iMod (Hwp) as (stateI fork_post) "[Hσ H]".
   iApply (@twptp_total _ _ (IrisG _ _ Hinv stateI fork_post) with "Hσ").
   by iApply (@twp_twptp _ _ (IrisG _ _ Hinv stateI fork_post)).