docs: check \later and \always rules; sync with Coq

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).

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