move re-wrapping of iris-specific lemmas to bi.v

_CoqProject

@@ -48,7 +48,6 @@ theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v
 theories/base_logic/base_logic.v
-theories/base_logic/soundness.v
 theories/base_logic/double_negation.v
 theories/base_logic/lib/iprop.v
 theories/base_logic/lib/own.v

theories/base_logic/base_logic.v

@@ -7,8 +7,9 @@ Set Default Proof Using "Type".
 another [uPred] module is by Jason Gross and described in:
 https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00069.html *)
 Module Import uPred.
+  Export base_logic.bi.uPred.
   Export derived.uPred.
-  Export bi.
+  Export bi.bi.
 End uPred.
 
 (* Setup of the proof mode *)

theories/base_logic/bi.v

@@ -2,7 +2,8 @@ From iris.bi Require Export derived_connectives updates plainly.
 From iris.base_logic Require Export upred.
 Import uPred_primitive.
 
-(** BI instances for uPred.  This file does *not* unseal. *)
+(** BI instances for uPred, and re-stating the remaining primitive laws in terms
+of the BI interface.  This file does *not* unseal. *)
 
 Definition uPred_emp {M} : uPred M := uPred_pure True.
 
@@ -151,3 +152,75 @@ Hint Immediate uPred_affine.
 
 Global Instance uPred_plainly_exist_1 : BiPlainlyExist (uPredSI M).
 Proof. exact: @plainly_exist_1. Qed.
+
+(** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
+
+Module uPred.
+
+Section restate.
+Context {M : ucmraT}.
+Implicit Types φ : Prop.
+Implicit Types P Q : uPred M.
+Implicit Types A : Type.
+
+(* Force implicit argument M *)
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+Global Existing Instance uPred_primitive.ownM_ne.
+Global Existing Instance uPred_primitive.cmra_valid_ne.
+
+(** Re-exporting primitive Own and valid lemmas *)
+Lemma ownM_op (a1 a2 : M) :
+  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+Proof. exact: uPred_primitive.ownM_op. Qed.
+Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
+Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+Proof. exact: uPred_primitive.ownM_unit. Qed.
+Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Proof. exact: uPred_primitive.later_ownM. Qed.
+Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+Proof. exact: uPred_primitive.ownM_valid. Qed.
+Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
+Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
+Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Proof. exact: uPred_primitive.prod_validI. Qed.
+Lemma option_validI {A : cmraT} (mx : option A) :
+  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
+Proof. exact: uPred_primitive.option_validI. Qed.
+Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Proof. exact: uPred_primitive.discrete_valid. Qed.
+Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
+Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
+
+(** Consistency/soundness statement *)
+Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
+Proof. exact: uPred_primitive.soundness. Qed.
+
+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? *)
+Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
+  unfold bi_emp; simpl; unfold sbi_emp; simpl;
+  unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
+  bi_and, bi_or, bi_impl, bi_forall, bi_exist,
+  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
+  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
+  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
+  unfold plainly, bi_plainly_plainly; simpl;
+  uPred_primitive.unseal.
+
+End uPred.

theories/base_logic/derived.v

 From iris.base_logic Require Export bi.
 From iris.bi Require Export bi.
 Set Default Proof Using "Type".
-Import bi.
+Import bi base_logic.bi.uPred.
 
-Module uPred.
-
-(* New unseal tactic that also unfolds the BI layer *)
-Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
-  unfold bi_emp; simpl; unfold sbi_emp; simpl;
-  unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
-  bi_and, bi_or, bi_impl, bi_forall, bi_exist,
-  bi_sep, bi_wand, bi_persistently, sbi_internal_eq, sbi_later; simpl;
-  unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
-  sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently; simpl;
-  unfold plainly, bi_plainly_plainly; simpl;
-  uPred_primitive.unseal.
+(** Derived laws for Iris-specific primitive connectives (own, valid).
+    This file does NOT unseal! *)
 
+Module uPred.
 Section derived.
 Context {M : ucmraT}.
 Implicit Types φ : Prop.
@@ -35,47 +26,10 @@ Global Instance uPred_valid_flip_mono :
   Proper (flip (⊢) ==> flip impl) (@uPred_valid M).
 Proof. solve_proper. Qed.
 
-Global Existing Instance uPred_primitive.ownM_ne.
 Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-
-Global Existing Instance uPred_primitive.cmra_valid_ne.
 Global Instance cmra_valid_proper {A : cmraT} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
-(** Re-exporting primitive Own and valid lemmas *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
-Proof. exact: uPred_primitive.ownM_op. Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
-Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
-Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
-Proof. exact: uPred_primitive.ownM_unit. Qed.
-Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
-Proof. exact: uPred_primitive.later_ownM. Qed.
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
-Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
-
-Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmraT} P (a : A) : ✓ a → P ⊢ (✓ a).
-Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
-Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ■ ✓ a.
-Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. exact: uPred_primitive.prod_validI. Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
-Proof. exact: uPred_primitive.option_validI. Qed.
-Lemma discrete_valid {A : cmraT} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-Proof. exact: uPred_primitive.discrete_valid. Qed.
-Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
-Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
-
 (** Own and valid derived *)
 Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
@@ -105,7 +59,7 @@ Proof.
   by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
 Qed.
 
-(* Timeless instances *)
+(** Timeless instances *)
 Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
   Timeless (✓ a : uPred M)%I.
 Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
@@ -118,12 +72,12 @@ Proof.
     auto using and_elim_l, and_elim_r.
 Qed.
 
-(* Plainness *)
+(** Plainness *)
 Global Instance cmra_valid_plain {A : cmraT} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
-(* Persistence *)
+(** Persistence *)
 Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
   Persistent (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
@@ -132,10 +86,19 @@ Proof.
   intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
 Qed.
 
-(* For big ops *)
+(** For big ops *)
 Global Instance uPred_ownM_sep_homomorphism :
   MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
 Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
+
+
+(** Consistency/soundness statement *)
+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.

theories/base_logic/soundness.v

-From iris.base_logic Require Export base_logic.
-Set Default Proof Using "Type".
-Import uPred.
-
-Section adequacy.
-Context {M : ucmraT}.
-
-(** Consistency and adequancy statements *)
-Lemma soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ.
-Proof.
-  cut ((▷^n ⌜ φ ⌝ : uPred M)%I n ε → φ).
-  { intros help H. eapply help, H; eauto using ucmra_unit_validN. by unseal. }
-  rewrite /sbi_laterN; unseal. induction n as [|n IH]=> H; auto.
-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 adequacy.

theories/base_logic/upred.v

 From iris.algebra Require Export cmra updates.
 From iris.bi Require Import notation.
 From stdpp Require Import finite.
+From Coq.Init Require Import Nat.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
@@ -799,5 +800,13 @@ Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. by unseal. Qed.
 
+(** Consistency/soundness statement *)
+Lemma soundness φ n : (True ⊢ iter n uPred_later (⌜ φ ⌝)%I) → φ.
+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.
+Qed.
+
 End primitive.
 End uPred_primitive.

theories/program_logic/adequacy.v

 From iris.program_logic Require Export weakestpre.
 From iris.algebra Require Import gmap auth agree gset coPset.
-From iris.base_logic Require Import soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".

theories/program_logic/total_adequacy.v

 From iris.program_logic Require Export total_weakestpre adequacy.
 From iris.algebra Require Import gmap auth agree gset coPset list.
 From iris.bi Require Import big_op fixpoint.
-From iris.base_logic Require Import soundness.
 From iris.base_logic.lib Require Import wsat.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".