Commit a1398f31 authored by Ralf Jung's avatar Ralf Jung

soundness -> consistency

parent 86b184af
Pipeline #2788 passed with stage
in 9 minutes and 20 seconds
......@@ -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 *)
......
......@@ -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
......
......@@ -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
......
......@@ -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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment