Commit 702ad20d authored by Robbert Krebbers's avatar Robbert Krebbers

Merge commit '833f7c15' into gen_proofmode

parents bfc28202 833f7c15
......@@ -7,7 +7,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
* [#] Add new modality: ■ ("plainly").
* Add new modality: ■ ("plainly").
* Camera morphisms have to be homomorphisms, not just monotone functions.
* Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
......
......@@ -63,12 +63,13 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
%\\&
\ownM{\term} \mid \mval(\term) \mid
\always\prop \mid
\plainly\prop \mid
{\later\prop} \mid
\upd \prop
\end{align*}
Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
Note that the modalities $\upd$, $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
\paragraph{Variable conventions.}
......@@ -175,6 +176,9 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\always\prop}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\plainly\prop}{\Prop}}
\and
\infer{\vctx \proves \wtt{\prop}{\Prop}}
{\vctx \proves \wtt{\later\prop}{\Prop}}
......@@ -303,7 +307,30 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\prop \proves \propB \wand \propC}
\end{mathpar}
\paragraph{Laws for the always modality.}
\paragraph{Laws for the plainness modality.}
\begin{mathpar}
\infer[$\plainly$-mono]
{\prop \proves \propB}
{\plainly{\prop} \proves \plainly{\propB}}
\and
\infer[$\plainly$-E]{}
{\plainly\prop \proves \always\prop}
\and
\begin{array}[c]{rMcMl}
\TRUE &\proves& \plainly{\TRUE} \\
(\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q)
\end{array}
\and
\begin{array}[c]{rMcMl}
\plainly{\prop} &\proves& \plainly\plainly\prop \\
\All x. \plainly{\prop} &\proves& \plainly{\All x. \prop} \\
\plainly{\Exists x. \prop} &\proves& \Exists x. \plainly{\prop}
\end{array}
\and
\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
\end{mathpar}
\paragraph{Laws for the persistence modality.}
\begin{mathpar}
\infer[$\always$-mono]
{\prop \proves \propB}
......@@ -313,9 +340,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\always\prop \proves \prop}
\and
\begin{array}[c]{rMcMl}
\TRUE &\proves& \always{\TRUE} \\
\always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
(\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
\end{array}
\and
\begin{array}[c]{rMcMl}
......@@ -344,7 +370,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\and
\begin{array}[c]{rMcMl}
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
\always{\later\prop} &\provesIff& \later\always{\prop}
\always{\later\prop} &\provesIff& \later\always{\prop} \\
\plainly{\later\prop} &\provesIff& \later\plainly{\prop}
\end{array}
\end{mathpar}
......@@ -393,6 +420,10 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\inferH{upd-update}
{\melt \mupd \meltsB}
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
\inferH{upd-plainly}
{}
{\upd\plainly\prop \proves \prop}
\end{mathpar}
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
%\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
......@@ -401,13 +432,14 @@ The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that h
The consistency statement of the logic reads as follows: For any $n$, we have
\begin{align*}
\lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)
\lnot(\TRUE \proves (\later)^n\spac\FALSE)
\end{align*}
where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
where $(\later)^n$ is short for $\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.
For $\always$ and $\plainly$, this follows from the elimination rules.
For updates, we use the fact that $\upd\FALSE \proves \upd\plainly\FALSE \proves \FALSE$.
However, there is no elimination rule for $\later$, so we declare that it is impossible to derive a contradiction below any number of laters.
%%% Local Variables:
......
......@@ -260,6 +260,7 @@
\newcommand{\later}{\mathop{{\triangleright}}}
\newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
\newcommand{\always}{\mathop{\Box}}
\newcommand{\plainly}{\mathop{\blacksquare}}
%% Invariants and Ghost ownership
% PDS: Was 0pt inner, 2pt outer.
......
......@@ -16,7 +16,7 @@
\input{setup}
\title{\bfseries The Iris 3.0 Documentation}
\title{\bfseries The Iris 3.1 Documentation}
\author{\url{http://plv.mpi-sws.org/iris/}}
......
......@@ -54,10 +54,11 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Lam \melt. \setComp{n}{\begin{aligned}
\All m, \meltB.& m \leq n \land \melt\mtimes\meltB \in \mval_m \Ra {} \\
& m \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB) \Ra {}\\& m \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\melt\mtimes\meltB)\end{aligned}} \\
\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
\Sem{\vctx \proves \ownM{\term} : \Prop}_\gamma &\eqdef \Lam\meltB. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \mincl[n] \meltB} \\
\Sem{\vctx \proves \mval(\term) : \Prop}_\gamma &\eqdef \Lam\any. \setComp{n}{\Sem{\vctx \proves \term : \textlog{M}}_\gamma \in \mval_n} \\
\Sem{\vctx \proves \always{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\mcore\melt) \\
\Sem{\vctx \proves \plainly{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \Sem{\vctx \proves \prop : \Prop}_\gamma(\munit) \\
\Sem{\vctx \proves \later{\prop} : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{n = 0 \lor n-1 \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\melt)}\\
\Sem{\vctx \proves \upd\prop : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}
\All m, \melt'. & m \leq n \land (\melt \mtimes \melt') \in \mval_m \Ra {}\\& \Exists \meltB. (\meltB \mtimes \melt') \in \mval_m \land m \in \Sem{\vctx \proves \prop :\Prop}_\gamma(\meltB)
\end{aligned}
......
......@@ -26,15 +26,17 @@ Proof.
Thus Ag(T) is not necessarily complete.
*)
Record agree (A : Type) : Type := Agree {
Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Arguments Agree {_} _ _.
Arguments agree_car {_} _.
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Definition to_agree {A} (a : A) : agree A :=
{| agree_car := [a]; agree_not_nil := eq_refl |}.
Lemma elem_of_agree {A} (x : agree A) : a, a agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y x = y.
......@@ -82,7 +84,7 @@ Instance agree_validN : ValidN (agree A) := λ n x,
Instance agree_valid : Valid (agree A) := λ x, n, {n} x.
Program Instance agree_op : Op (agree A) := λ x y,
Agree (agree_car x ++ agree_car y) _.
{| agree_car := agree_car x ++ agree_car y |}.
Next Obligation. by intros [[|??]] y. Qed.
Instance agree_pcore : PCore (agree A) := Some.
......@@ -157,9 +159,6 @@ Proof.
apply discrete_iff_0; auto.
Qed.
Program Definition to_agree (a : A) : agree A :=
{| agree_car := [a]; agree_not_nil := eq_refl |}.
Global Instance to_agree_ne : NonExpansive to_agree.
Proof.
intros n a1 a2 Hx; split=> b /=;
......@@ -167,6 +166,15 @@ Proof.
Qed.
Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
Global Instance to_agree_discrete a : Discrete a Discrete (to_agree a).
Proof.
intros ? y [H H'] n; split.
- intros a' ->%elem_of_list_singleton. destruct (H a) as [b ?]; first by left.
exists b. by rewrite -discrete_iff_0.
- intros b Hb. destruct (H' b) as (b'&->%elem_of_list_singleton&?); auto.
exists a. by rewrite elem_of_list_singleton -discrete_iff_0.
Qed.
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
Proof.
move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
......
......@@ -93,7 +93,7 @@ Section frac_auth.
IsOp q q1 q2 IsOp a a1 a2 IsOp' (!{q} a) (!{q1} a1) (!{q2} a2).
Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
Global Instance is_op_frac_auth_persistent (q q1 q2 : frac) (a : A) :
Global Instance is_op_frac_auth_core_id (q q1 q2 : frac) (a : A) :
CoreId a IsOp q q1 q2 IsOp' (!{q} a) (!{q1} a) (!{q2} a).
Proof.
rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
......
......@@ -216,6 +216,13 @@ End ectx_language.
Arguments ectx_lang : clear implicits.
Coercion ectx_lang : ectxLanguage >-> language.
(* This definition makes sure that the fields of the [language] record do not
refer to the projections of the [ectxLanguage] record but to the actual fields
of the [ectxLanguage] record. This is crucial for canonical structure search to
work.
Note that this trick no longer works when we switch to canonical projections
because then the pattern match [let '...] will be desugared into projections. *)
Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
@Language E V St of_val to_val _
......
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