From aab090749513e923fd08030c0196b525c79f725a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sun, 6 Mar 2016 23:21:26 +0100 Subject: [PATCH] docs: check \later and \always rules; sync with Coq --- algebra/upred.v | 13 ++++++------ docs/logic.tex | 53 ++++++++++++++++++++++++------------------------- 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/algebra/upred.v b/algebra/upred.v index 55bb3023..1e8ee934 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -917,8 +917,6 @@ Proof. unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|]. apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S. Qed. -Lemma later_True' : True ⊑ (▷ True : uPred M). -Proof. unseal; by split=> -[|n] x. Qed. Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I. Proof. unseal; split=> -[|n] x; by split. Qed. Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I. @@ -927,9 +925,9 @@ Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, Proof. unseal; by split=> -[|n] x. Qed. Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a). Proof. unseal; by split=> -[|[|n]] x. Qed. -Lemma later_exist {Inhabited A} (Φ : A → uPred M) : - (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I. -Proof. unseal; split=> -[|[|n]] x; split; done || by exists inhabitant. Qed. +Lemma later_exist' {Inhabited A} (Φ : A → uPred M) : + (▷ ∃ a, Φ a)%I ⊑ (∃ a, ▷ Φ a)%I. +Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed. Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I. Proof. unseal; split=> n x ?; split. @@ -949,12 +947,15 @@ Global Instance later_flip_mono' : Proper (flip (⊑) ==> flip (⊑)) (@uPred_later M). Proof. intros P Q; apply later_mono. Qed. Lemma later_True : (▷ True : uPred M)%I ≡ True%I. -Proof. apply (anti_symm (⊑)); auto using later_True'. Qed. +Proof. apply (anti_symm (⊑)); auto using later_intro. Qed. Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q). Proof. apply impl_intro_l; rewrite -later_and. apply later_mono, impl_elim with P; auto. Qed. +Lemma later_exist `{Inhabited A} (Φ : A → uPred M) : + (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I. +Proof. apply: anti_symm; eauto using later_exist', later_exist_1. Qed. Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q). Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed. Lemma later_iff P Q : (▷ (P ↔ Q)) ⊑ (▷ P ↔ ▷ Q). diff --git a/docs/logic.tex b/docs/logic.tex index bad60509..6e1ead9f 100644 --- a/docs/logic.tex +++ b/docs/logic.tex @@ -120,6 +120,8 @@ Iris syntax is built up from a signature $\Sig$ and a countably infinite set \t \end{align*} Recursive predicates must be \emph{guarded}: in\MU \var. \pred$, the variable$\var$can only appear under the later$\later$modality. +Note that$\always$and$\later$bind more tightly than$*$,$\wand$,$\land$,$\lor$, and$\Ra$. + \paragraph{Metavariable conventions.} We introduce additional metavariables ranging over terms and generally let the choice of metavariable indicate the term's type: \[ @@ -292,7 +294,6 @@ Axioms$\prop \Ra \propB$stand for judgments$\vctx \mid \cdot \proves \prop \R \judgment{}{\vctx \mid \pfctx \proves \prop} \paragraph{Laws of intuitionistic higher-order logic.} This is entirely standard. - \begin{mathparpagebreakable} \infer[Asm] {\prop \in \pfctx} @@ -384,18 +385,17 @@ This is entirely standard. (\prop * \propB) * \propC &\Lra& \prop * (\propB * \propC) \end{array} \and -\infer +\infer[$*$-mono] {\prop_1 \proves \propB_1 \and \prop_2 \proves \propB_2} {\prop_1 * \prop_2 \proves \propB_1 * \propB_2} \and -\inferB +\inferB[$\wand$I-E] {\prop * \propB \proves \propC} {\prop \proves \propB \wand \propC} \end{mathpar} \paragraph{Laws for ghosts and physical resources.} - \begin{mathpar} \begin{array}{rMcMl} \ownGGhost{\melt} * \ownGGhost{\meltB} &\Lra& \ownGGhost{\melt \mtimes \meltB} \\ @@ -409,60 +409,59 @@ This is entirely standard. \end{mathpar} \paragraph{Laws for the later modality.} -~\\\ralf{Go on checking below.} - - \begin{mathpar} -\inferH{Mono} +\infer[$\later$-mono] {\pfctx \proves \prop} {\pfctx \proves \later{\prop}} \and -\inferhref{L{\"o}b}{Loeb} - {\pfctx, \later{\prop} \proves \prop} - {\pfctx \proves \prop} +\infer[L{\"o}b] + {} + {(\later\prop\Ra\prop) \proves \prop} \and -\begin{array}[b]{rMcMl} - \later{\always{\prop}} &\Lra& \always{\later{\prop}} \\ +\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)} &\Lra& \later{\prop} \wedge \later{\propB} \\ \later{(\prop \vee \propB)} &\Lra& \later{\prop} \vee \later{\propB} \\ \end{array} \and -\begin{array}[b]{rMcMl} +\begin{array}[c]{rMcMl} \later{\All x.\prop} &\Lra& \All x. \later\prop \\ - \later{\Exists x.\prop} &\Lra& \Exists x. \later\prop \\ + \Exists x. \later\prop &\Ra& \later{\Exists x.\prop} \\ \later{(\prop * \propB)} &\Lra& \later\prop * \later\propB \end{array} \end{mathpar} \paragraph{Laws for the always modality.} - \begin{mathpar} -\axiomH{Necessity} - {\always{\prop} \Ra \prop} -\and -\inferhref{$\always$I}{AlwaysIntro} +\infer[$\always$I] {\always{\pfctx} \proves \prop} {\always{\pfctx} \proves \always{\prop}} \and -\begin{array}[b]{rMcMl} - \always(\term =_\type \termB) &\Lra& \term=_\type \termB \\ - \always{\prop} * \propB &\Lra& \always{\prop} \land \propB \\ - \always{(\prop \Ra \propB)} &\Ra& \always{\prop} \Ra \always{\propB} \\ +\infer[$\always$E]{} + {\always{\prop} \Ra \prop} +\and +\begin{array}[c]{rMcMl} + \always{(\prop * \propB)} &\Ra& \always{(\prop \land \propB)} \\ + \always{\prop} * \propB &\Ra& \always{\prop} \land \propB \\ + \always{\later\prop} &\Lra& \later\always{\prop} \\ \end{array} \and -\begin{array}[b]{rMcMl} +\begin{array}[c]{rMcMl} \always{(\prop \land \propB)} &\Lra& \always{\prop} \land \always{\propB} \\ \always{(\prop \lor \propB)} &\Lra& \always{\prop} \lor \always{\propB} \\ \always{\All x. \prop} &\Lra& \All x. \always{\prop} \\ \always{\Exists x. \prop} &\Lra& \Exists x. \always{\prop} \\ \end{array} \end{mathpar} -Note that $\always$ binds more tightly than $*$, $\land$, $\lor$, and $\Ra$. \paragraph{Laws of primitive view shifts.} +~\\\ralf{Add these.} \paragraph{Laws of weakest preconditions.} - +~\\\ralf{Add these.} %%% Local Variables: %%% mode: latex -- GitLab