From 473ad60bd03fc58d590ce1529502ee02cedf4f1e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Mar 2019 14:41:54 +0100
Subject: [PATCH] Nicer soundness statements for the base_logic.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This commit introduces the following soundness statements:

- Soundness of pure propositions `⌜ φ ⌝%I → φ`.
- Soundness of later `(▷ P)%I → P`.

The old soundness statement, `(▷^n ⌜ φ ⌝)%I → φ` is now a derived form.
---
 theories/base_logic/bi.v      |  6 ++++--
 theories/base_logic/derived.v |  9 ++++++---
 theories/base_logic/upred.v   | 12 +++++++-----
 3 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 9db6cf683..b6d065037 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -206,9 +206,11 @@ 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_iter φ n : Nat.iter n sbi_later (⌜ φ ⌝ : uPred M)%I → φ.
-Proof. exact: uPred_primitive.soundness. Qed.
+Lemma soundness_pure φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
+Proof. apply soundness_pure. Qed.
 
+Lemma soundness_later P : bi_emp_valid (▷ P) → bi_emp_valid P.
+Proof. apply soundness_later. Qed.
 End restate.
 
 (** New unseal tactic that also unfolds the BI layer.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index aa2e11301..e5b4462bd 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -92,15 +92,18 @@ Global Instance uPred_ownM_sep_homomorphism :
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
-Proof. rewrite laterN_iter. apply soundness_iter. Qed.
+Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof.
+  induction n as [|n IH]=> /=.
+  - apply soundness_pure.
+  - intros H. by apply IH, soundness_later.
+Qed.
 
 Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I.
 Proof. exact (soundness False n). Qed.
 
 Corollary consistency : ¬(False : uPred M)%I.
 Proof. exact (consistency_modal 0). Qed.
-
 End derived.
 
 End uPred.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index f6052c634..d9c180eb0 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -801,12 +801,14 @@ Lemma ofe_fun_validI {A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
-Lemma soundness φ n : (True ⊢ iter n uPred_later (⌜ φ ⌝)%I) → φ.
+Lemma soundness_pure φ : (True ⊢ ⌜ φ ⌝) → φ.
+Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
+
+Lemma soundness_later P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
-  cut (iter n (@uPred_later M) (⌜ φ ⌝)%I n ε → φ).
-  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
-  unseal. induction n as [|n IH]=> H; auto.
+  unseal=> -[HP]; split=> n x Hx _.
+  apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
+  by apply (HP (S n)); eauto using ucmra_unit_validN.
 Qed.
-
 End primitive.
 End uPred_primitive.
-- 
GitLab