From a1398f31a39e0c0a11c61cfefed3ae100e52604a Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 7 Oct 2016 11:15:14 +0200 Subject: [PATCH] soundness -> consistency --- algebra/upred.v | 8 ++++---- docs/base-logic.tex | 10 +++++++--- docs/model.tex | 5 +++-- program_logic/counter_examples.v | 4 ++-- 4 files changed, 16 insertions(+), 11 deletions(-) diff --git a/algebra/upred.v b/algebra/upred.v index 392e50779..096ca4dd2 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -1481,7 +1481,7 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed. Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q. Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed. -(* Soundness results *) +(** Consistency and adequancy statements *) Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) (■φ)) → φ. Proof. cut (∀ x, ✓{n} x → Nat.iter n (λ P, |=r=> ▷ P)%I (■φ)%I n x → φ). @@ -1492,11 +1492,11 @@ Proof. eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l. Qed. -Corollary soundnessN n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False). +Corollary consistencyModal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False). Proof. exact (adequacy False n). Qed. -Corollary soundness : ¬ (True ⊢ False). -Proof. exact (adequacy False 0). Qed. +Corollary consistency : ¬ (True ⊢ False). +Proof. exact (consistencyModal 0). Qed. End uPred_logic. (* Hint DB for the logic *) diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 9039a5af3..f6fbcc5bd 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -393,14 +393,18 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB} \end{mathpar} -\subsection{Soundness} +\subsection{Consistency} -The soundness statement of the logic reads as follows: For any $n$, we have +The consistency statement of the logic reads as follows: For any $n$, we have \begin{align*} - \lnot(\TRUE \vdash (\upd\later)^n \FALSE) + \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE) \end{align*} where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times. +The reason we want a stronger consistency than the usual $\lnot(\TRUE \proves \FALSE)$ is our modalities: it should be impossible to derive a contradiction below the modalities. +For $\always$, this follows from the elimination rule, but the other two modalities do not have an elimination rule. +Hence we declare that it is impossible to derive a contradiction below any combination of these two modalities. + %%% Local Variables: %%% mode: latex diff --git a/docs/model.tex b/docs/model.tex index 8767494c2..41b545ca2 100644 --- a/docs/model.tex +++ b/docs/model.tex @@ -110,10 +110,11 @@ n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs) \end{aligned} \] -The following theorem connects syntactic and semantic entailment: +The following soundness theorem connects syntactic and semantic entailment. +It is proven by showing that all the syntactic proof rules of \Sref{sec:base-logic} can be validated in the model. \[ \vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB} \] -It now becomes trivial to show soundness of the logic. +It now becomes straight-forward to show consistency of the logic. %%% Local Variables: %%% mode: latex diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v index aa3ceb25a..fe673a206 100644 --- a/program_logic/counter_examples.v +++ b/program_logic/counter_examples.v @@ -93,7 +93,7 @@ Module inv. Section inv. Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ. (* We assume that we cannot view shift to false. *) - Hypothesis soundness : ¬ (True ⊢ pvs M1 False). + Hypothesis consistency : ¬ (True ⊢ pvs M1 False). (** Some general lemmas and proof mode compatibility. *) Lemma inv_open' i P R : inv i P ★ (P -★ pvs M0 (P ★ pvs M1 R)) ⊢ pvs M1 R. @@ -186,7 +186,7 @@ Module inv. Section inv. Lemma contradiction : False. Proof. - apply soundness. iIntros "". + apply consistency. iIntros "". iVs A_alloc as (i) "#H". iPoseProof (saved_NA with "H") as "HN". iApply "HN". iApply saved_A. done. -- GitLab