From 9df1dae0e59e27cee6fa754bda2ac360276813b8 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 4 Oct 2016 17:09:57 +0200 Subject: [PATCH] appendix: base logic is now up-to-date --- algebra/upred.v | 77 +++++++++++++++++++++---------------- docs/base-logic.tex | 92 ++++++++++++++++++++++++--------------------- 2 files changed, 93 insertions(+), 76 deletions(-) diff --git a/algebra/upred.v b/algebra/upred.v index 806520a0..5005e73c 100644 --- a/algebra/upred.v +++ b/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. diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 85a49e12..a63bb983 100644 --- a/docs/base-logic.tex +++ b/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: -- 2.24.1