Commit 19989519 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 05845cc3 7de50f87
Pipeline #2793 passed with stage
in 9 minutes and 23 seconds
......@@ -1492,11 +1492,11 @@ Proof.
eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
Qed.
Corollary consistencyModal n : ¬ (True Nat.iter n (λ P, |=r=> P) False).
Corollary consistency_modal n : ¬ (True Nat.iter n (λ P, |=r=> P) False).
Proof. exact (adequacy False n). Qed.
Corollary consistency : ¬ (True False).
Proof. exact (consistencyModal 0). Qed.
Proof. exact (consistency_modal 0). Qed.
End uPred_logic.
(* Hint DB for the logic *)
......
......@@ -130,7 +130,7 @@ The fragment will then be available to the user of the logic, as their way of ta
It turns out that weakest precondition is actually quite convenient to work with, in particular when perfoming these proofs on paper.
Still, for a more traditional presentation, we can easily derive the notion of a Hoare triple:
\[
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\lambda\Ret\val.\propB})}
\hoare{\prop}{\expr}{\Ret\val.\propB}[\mask] \eqdef \always{(\prop \Ra \wpre{\expr}[\mask]{\Ret\val.\propB})}
\]
\subsection{Lost stuff}
......
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