appendix: base logic is now up-to-date

algebra/upred.v

@@ -1002,9 +1002,6 @@ Proof.
   by rewrite cmra_core_l cmra_core_idemp.
 Qed.
 
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
-Proof. by unseal. Qed.
-
 (* Always derived *)
 Hint Resolve always_mono always_elim.
 Global Instance always_mono' : Proper ((⊢) ==> (⊢)) (@uPred_always M).
@@ -1069,32 +1066,6 @@ Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
 Lemma always_entails_r' P Q : (P ⊢ □ Q) → P ⊢ P ★ □ Q.
 Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
 
-(* Conditional always *)
-Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-
-Lemma always_if_elim p P : □?p P ⊢ P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-
-Lemma always_if_pure p φ : □?p ■ φ ⊣⊢ ■ φ.
-Proof. destruct p; simpl; auto using always_pure. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
-Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
-Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ □?p P ★ □?p Q.
-Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
-Proof. destruct p; simpl; auto using always_later. Qed.
-
 (* Later *)
 Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
 Proof.
@@ -1128,6 +1099,10 @@ Proof.
   eauto using uPred_closed, uPred_mono, cmra_included_includedN.
 Qed.
 
+Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
+Proof. by unseal. Qed.
+
+
 (* Later derived *)
 Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
 Proof. by intros ->. Qed.
@@ -1169,6 +1144,34 @@ Proof. apply wand_intro_r; rewrite -later_sep; eauto using wand_elim_l. Qed.
 Lemma later_iff P Q : ▷ (P ↔ Q) ⊢ ▷ P ↔ ▷ Q.
 Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
+
+(* Conditional always *)
+Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
+Proof. solve_proper. Qed.
+
+Lemma always_if_elim p P : □?p P ⊢ P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+Lemma always_elim_if p P : □ P ⊢ □?p P.
+Proof. destruct p; simpl; auto using always_elim. Qed.
+
+Lemma always_if_pure p φ : □?p ■ φ ⊣⊢ ■ φ.
+Proof. destruct p; simpl; auto using always_pure. Qed.
+Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
+Proof. destruct p; simpl; auto using always_and. Qed.
+Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
+Proof. destruct p; simpl; auto using always_or. Qed.
+Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
+Proof. destruct p; simpl; auto using always_exist. Qed.
+Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ □?p P ★ □?p Q.
+Proof. destruct p; simpl; auto using always_sep. Qed.
+Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
+Proof. destruct p; simpl; auto using always_later. Qed.
+
+
 (* True now *)
 Global Instance except_last_ne n : Proper (dist n ==> dist n) (@uPred_except_last M).
 Proof. solve_proper. Qed.
@@ -1226,10 +1229,9 @@ Proof.
     by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
       -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
 Qed.
-Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
 Proof.
-  split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
-  rewrite -(persistent_core a). by apply cmra_core_monoN.
+  split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
 Qed.
 Lemma ownM_empty : True ⊢ uPred_ownM ∅.
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
@@ -1250,18 +1252,27 @@ Lemma cmra_valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
 Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma always_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ □ ✓ a.
 Proof. by unseal. Qed.
 Lemma cmra_valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
 
 (* Own and valid derived *)
+Lemma always_ownM (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+Proof.
+  intros; apply (anti_symm _); first by apply:always_elim.
+  by rewrite {1}always_ownM_core persistent_core.
+Qed.
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
 Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
 Lemma ownM_empty' : uPred_ownM ∅ ⊣⊢ True.
 Proof. apply (anti_symm _); auto using ownM_empty. Qed.
+Lemma always_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+  intros; apply (anti_symm _); first by apply:always_elim.
+  apply:always_cmra_valid_1.
+Qed.
 
 (* Viewshifts *)
 Lemma rvs_intro P : P =r=> P.

docs/base-logic.tex

@@ -299,78 +299,80 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
   {\prop \proves \propB \wand \propC}
 \end{mathpar}
 
-\paragraph{Laws for ghosts and physical resources.}
+\paragraph{Laws for the always modality.}
 \begin{mathpar}
-\begin{array}{rMcMl}
-\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
-\ownGGhost{\melt} &\proves& \mval(\melt) \\
-\TRUE &\proves&  \ownGGhost{\munit}
-\end{array}
+\infer[$\always$-mono]
+  {\prop \proves \propB}
+  {\always{\prop} \proves \always{\propB}}
 \and
+\begin{array}[c]{rMcMl}
+  \always{\prop} &\proves& \prop \\
+  \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
+  \always{\prop} \land \propB &\proves& \always{\prop} * \propB
+\end{array}
 \and
-\begin{array}{c}
-\ownPhys{\state} * \ownPhys{\state'} \proves \FALSE
+\begin{array}[c]{rMcMl}
+  \always{\prop} &\proves& \always\always\prop \\
+  \All x. \always{\prop} &\proves& \always{\All x. \prop} \\
+  \always{\Exists x. \prop} &\proves& \Exists x. \always{\prop}
 \end{array}
 \end{mathpar}
 
+
 \paragraph{Laws for the later modality.}
 \begin{mathpar}
 \infer[$\later$-mono]
-  {\pfctx \proves \prop}
-  {\pfctx \proves \later{\prop}}
+  {\prop \proves \propB}
+  {\later\prop \proves \later{\propB}}
 \and
 \infer[L{\"o}b]
   {}
   {(\later\prop\Ra\prop) \proves \prop}
 \and
-\infer[$\later$-$\exists$]
-  {\text{$\type$ is inhabited}}
-  {\later{\Exists x:\type.\prop} \proves \Exists x:\type. \later\prop}
-\\\\
 \begin{array}[c]{rMcMl}
-  \later{(\prop \wedge \propB)} &\provesIff& \later{\prop} \wedge \later{\propB}  \\
-  \later{(\prop \vee \propB)} &\provesIff& \later{\prop} \vee \later{\propB} \\
+  \All x. \later\prop &\proves& \later{\All x.\prop} \\
+  \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop}  \\
+  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop) \\
 \end{array}
 \and
 \begin{array}[c]{rMcMl}
-  \later{\All x.\prop} &\provesIff& \All x. \later\prop \\
-  \Exists x. \later\prop &\proves& \later{\Exists x.\prop}  \\
-  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
+  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
+  \always{\later\prop} &\provesIff& \later\always{\prop} \\
 \end{array}
 \end{mathpar}
-A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
 
-\paragraph{Laws for the always modality.}
+
+\paragraph{Laws for ghosts and validity.}
 \begin{mathpar}
-\infer[$\always$I]
-  {\always{\pfctx} \proves \prop}
-  {\always{\pfctx} \proves \always{\prop}}
-\and
-\infer[$\always$E]{}
-  {\always{\prop} \proves \prop}
-\and
-\begin{array}[c]{rMcMl}
-  \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
-  \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
-  \always{\later\prop} &\provesIff& \later\always{\prop} \\
-\end{array}
-\and
-\begin{array}[c]{rMcMl}
-  \always{(\prop \land \propB)} &\provesIff& \always{\prop} \land \always{\propB} \\
-  \always{(\prop \lor \propB)} &\provesIff& \always{\prop} \lor \always{\propB} \\
-  \always{\All x. \prop} &\provesIff& \All x. \always{\prop} \\
-  \always{\Exists x. \prop} &\provesIff& \Exists x. \always{\prop} \\
+\begin{array}{rMcMl}
+\ownGGhost{\melt} * \ownGGhost{\meltB} &\provesIff&  \ownGGhost{\melt \mtimes \meltB} \\
+\ownGGhost\melt &\proves& \always{\ownGGhost{\mcore\melt}} \\
+\TRUE &\proves&  \ownGGhost{\munit} \\
+\later\ownGGhost\melt &\proves& \Exists\meltB. \ownGGhost\meltB \land \later(\melt = \meltB)
 \end{array}
 \and
-{ \term =_\type \term' \proves \always \term =_\type \term'}
+\infer[valid-intro]
+{\melt \in \mval}
+{\TRUE \vdash \mval(\melt)}
 \and
-{ \ownGGhost{\mcore\melt} \proves \always \ownGGhost{\mcore\melt}}
+\infer[valid-elim]
+{\melt \notin \mval_0}
+{\mval(\melt) \proves \FALSE}
 \and
-{ \mval(\melt) \proves \always \mval(\melt)}
+\begin{array}{rMcMl}
+\ownGGhost{\melt} &\proves& \mval(\melt) \\
+\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
+\mval(\melt) &\proves& \always\mval(\melt)
+\end{array}
 \end{mathpar}
 
+
 \paragraph{Laws for the update modality.}
 \begin{mathpar}
+\infer[upd-mono]
+{\prop \proves \propB}
+{\upd\prop \proves \upd\propB}
+
 \infer[upd-intro]
 {}{\prop \proves \upd \prop}
 
@@ -388,7 +390,11 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
 
 \subsection{Soundness}
 
-The soundness statement of the logic 
+The soundness statement of the logic reads as follows: For any $n$, we have
+\begin{align*}
+  \lnot(\TRUE \vdash (\upd\later)^n \FALSE)
+\end{align*}
+where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
 
 
 %%% Local Variables: