Commit 3e1e5e0f authored by Aleš Bizjak's avatar Aleš Bizjak

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

parents 418eeacc 06aedc30
Pipeline #2413 passed with stage
In this changelog, we document "large-ish" changes to Iris that affect even the
way the logic is used on paper. We also mention some significant changes in the
Coq development, but not every API-breaking change is listed. Changes marked
[#] still need to be ported to the Iris Documentation LaTeX file.
## Iris 2.0
This version accompanies the final ICFP paper.
* [# algebra] Make the core of an RA or CMRA a partial function.
* [heap_lang] No longer use dependent types for expressions. Instead, values
carry a proof of closedness. Substitution, closedness and value-ness proofs
are performed by computation after reflecting into a term langauge that knows
about values and closed expressions.
* [program_logic/language] The language does not define its own "atomic"
predicate. Instead, atomicity is defined as reducing in one step to a value.
## Iris 2.0-rc1
This is the Coq development and Iris Documentation as submitted to ICFP.
......@@ -127,7 +127,7 @@ Proof.
- by split; simpl; rewrite ?cmra_core_l.
- by split; simpl; rewrite ?cmra_core_idemp.
- intros ??; rewrite! auth_included; intros [??].
by split; simpl; apply cmra_core_preserving.
by split; simpl; apply cmra_core_mono.
- assert ( n (a b1 b2 : A), b1 b2 {n} a b1 {n} a).
{ intros n a b1 b2 <-; apply cmra_includedN_l. }
intros n [[[a1|]|] b1] [[[a2|]|] b2];
......@@ -222,9 +222,9 @@ Instance auth_map_cmra_monotone {A B : ucmraT} (f : A → B) :
Proof.
split; try apply _.
- intros n [[[a|]|] b]; rewrite /= /cmra_validN /=; try
naive_solver eauto using includedN_preserving, validN_preserving.
naive_solver eauto using cmra_monotoneN, validN_preserving.
- by intros [x a] [y b]; rewrite !auth_included /=;
intros [??]; split; simpl; apply: included_preserving.
intros [??]; split; simpl; apply: cmra_monotone.
Qed.
Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
CofeMor (auth_map f).
......
This diff is collapsed.
......@@ -202,10 +202,10 @@ Proof.
- intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
+ exists CsumBot. rewrite csum_included; eauto.
+ destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving a a' ca) as (ca'&->&?); auto.
destruct (cmra_pcore_mono a a' ca) as (ca'&->&?); auto.
exists (Cinl ca'). rewrite csum_included; eauto 10.
+ destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
destruct (cmra_pcore_preserving b b' cb) as (cb'&->&?); auto.
destruct (cmra_pcore_mono b b' cb) as (cb'&->&?); auto.
exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
......@@ -330,7 +330,7 @@ Proof.
- intros n [a|b|]; simpl; auto using validN_preserving.
- intros x y; rewrite !csum_included.
intros [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]; simpl;
eauto 10 using included_preserving.
eauto 10 using cmra_monotone.
Qed.
Program Definition csumRF (Fa Fb : rFunctor) : rFunctor := {|
......
......@@ -20,7 +20,7 @@ Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
mixin_dra_core_disjoint_l x : x core x x;
mixin_dra_core_l x : x core x x x;
mixin_dra_core_idemp x : x core (core x) core x;
mixin_dra_core_preserving x y :
mixin_dra_core_mono x y :
z, x y x y core (x y) core x z z core x z
}.
Structure draT := DRAT {
......@@ -78,9 +78,9 @@ Section dra_mixin.
Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
Lemma dra_core_idemp x : x core (core x) core x.
Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
Lemma dra_core_preserving x y :
Lemma dra_core_mono x y :
z, x y x y core (x y) core x z z core x z.
Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed.
End dra_mixin.
Record validity (A : draT) := Validity {
......@@ -166,7 +166,7 @@ Proof.
naive_solver eauto using dra_core_l, dra_core_disjoint_l.
- intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
- intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
destruct (dra_core_preserving x z) as (z'&Hz').
destruct (dra_core_mono x z) as (z'&Hz').
unshelve eexists (Validity z' (px py pz) _); [|split; simpl].
{ intros (?&?&?); apply Hz'; tauto. }
+ tauto.
......
......@@ -134,7 +134,7 @@ Proof.
- intros m i. by rewrite lookup_op lookup_core cmra_core_l.
- intros m i. by rewrite !lookup_core cmra_core_idemp.
- intros m1 m2; rewrite !lookup_included=> Hm i.
rewrite !lookup_core. by apply cmra_core_preserving.
rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m m1 m2 Hm Hm12.
......@@ -399,7 +399,7 @@ Proof.
split; try apply _.
- by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
- intros m1 m2; rewrite !lookup_included=> Hm i.
by rewrite !lookup_fmap; apply: included_preserving.
by rewrite !lookup_fmap; apply: cmra_monotone.
Qed.
Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A gmapC K B).
......
......@@ -84,3 +84,6 @@ Section gset.
rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
Qed.
End gset.
Arguments gset_disjR _ {_ _}.
Arguments gset_disjUR _ {_ _}.
......@@ -114,7 +114,7 @@ Section iprod_cmra.
- by intros f x; rewrite iprod_lookup_op iprod_lookup_core cmra_core_l.
- by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
- intros f1 f2; rewrite !iprod_included_spec=> Hf x.
by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
......@@ -282,7 +282,7 @@ Proof.
split; first apply _.
- intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
- intros g1 g2; rewrite !iprod_included_spec=> Hf x.
rewrite /iprod_map; apply (included_preserving _), Hf.
rewrite /iprod_map; apply (cmra_monotone _), Hf.
Qed.
Definition iprodC_map `{Finite A} {B1 B2 : A cofeT}
......
......@@ -187,7 +187,7 @@ Section cmra.
- intros l; rewrite list_equiv_lookup=> i.
by rewrite !list_lookup_core cmra_core_idemp.
- intros l1 l2; rewrite !list_lookup_included=> Hl i.
rewrite !list_lookup_core. by apply cmra_core_preserving.
rewrite !list_lookup_core. by apply cmra_core_mono.
- intros n l1 l2. rewrite !list_lookup_validN.
setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
- intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
......@@ -374,7 +374,7 @@ Proof.
- intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
by apply (validN_preserving (fmap f : option A option B)).
- intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
by apply (included_preserving (fmap f : option A option B)).
by apply (cmra_monotone (fmap f : option A option B)).
Qed.
Program Definition listURF (F : urFunctor) : urFunctor := {|
......
......@@ -68,7 +68,7 @@ Qed.
Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
`{!CMRAMonotone f} (P : uPred M1) :
uPred M2 := {| uPred_holds n x := P n (f x) |}.
Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed.
Next Obligation. naive_solver eauto using uPred_mono, cmra_monotoneN. Qed.
Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
......@@ -212,7 +212,7 @@ Program Definition uPred_wand_def {M} (P Q : uPred M) : uPred M :=
Next Obligation.
intros M P Q n x1 x1' HPQ ? n3 x3 ???; simpl in *.
apply uPred_mono with (x1 x3);
eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le.
eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
Qed.
Next Obligation. naive_solver. Qed.
Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
......@@ -223,7 +223,7 @@ Definition uPred_wand_eq :
Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n (core x) |}.
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
......@@ -1038,7 +1038,7 @@ Qed.
Lemma always_ownM (a : M) : Persistent a uPred_ownM a ⊣⊢ uPred_ownM a.
Proof.
split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
rewrite -(persistent_core a). by apply cmra_core_preservingN.
rewrite -(persistent_core a). by apply cmra_core_monoN.
Qed.
Lemma ownM_something : True a, uPred_ownM a.
Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
......
This diff is collapsed.
......@@ -59,6 +59,35 @@ Frame-preserving updates on the $M_i$ lift to the product:
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
\subsection{Sum}
\label{sec:summ}
The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as:
\begin{align*}
\monoid_1 \csumm \monoid_2 \eqdef{}& \cinl(\melt_1:\monoid_1) \mid \cinr(\melt_2:\monoid_2) \mid \bot \\
\mval_n \eqdef{}& \setComp{\cinl(\melt_1)\!}{\!\melt_1 \in \mval'_n}
\cup \setComp{\cinr(\melt_2)\!}{\!\melt_2 \in \mval''_n} \\
\cinl(\melt_1) \mtimes \cinl(\meltB_1) \eqdef{}& \cinl(\melt_1 \mtimes \meltB_1) \\
% \munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
% \munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt) \\
\mcore{\cinl(\melt_1)} \eqdef{}& \begin{cases}\mnocore & \text{if $\mcore{\melt_1} = \mnocore$} \\ \cinl({\mcore{\melt_1}}) & \text{otherwise} \end{cases}
\end{align*}
The composition and core for $\cinr$ are defined symmetrically.
The remaining cases of the composition and core are all $\bot$.
Above, $\mval'$ refers to the validity of $\monoid_1$, and $\mval''$ to the validity of $\monoid_2$.
We obtain the following frame-preserving updates, as well as their symmetric counterparts:
\begin{mathpar}
\inferH{sum-update}
{\melt \mupd_{M_1} \meltsB}
{\cinl(\melt) \mupd \setComp{ \cinl(\meltB)}{\meltB \in \meltsB}}
\inferH{sum-swap}
{\All \melt_\f, n. \melt \mtimes \melt_\f \notin \mval'_n \and \meltB \in \mval''}
{\cinl(\melt) \mupd \cinr(\meltB)}
\end{mathpar}
Crucially, the second rule allows us to \emph{swap} the ``side'' of the sum that the CMRA is on if $\mval$ has \emph{no possible frame}.
\subsection{Finite partial function}
\label{sec:fpfnm}
......@@ -118,59 +147,17 @@ There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can
\axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
\end{mathpar}
\subsection{One-shot}
The purpose of the one-shot CMRA is to lazily initialize the state of a ghost location.
Given some CMRA $\monoid$, we define $\oneshotm(\monoid)$ as follows:
\begin{align*}
\oneshotm(\monoid) \eqdef{}& \ospending + \osshot(\monoid) + \munit + \bot \\
\mval_n \eqdef{}& \set{\ospending, \munit} \cup \setComp{\osshot(\melt)}{\melt \in \mval_n}
\\%\end{align*}
%\begin{align*}
\osshot(\melt) \mtimes \osshot(\meltB) \eqdef{}& \osshot(\melt \mtimes \meltB) \\
\munit \mtimes \ospending \eqdef{}& \ospending \mtimes \munit \eqdef \ospending \\
\munit \mtimes \osshot(\melt) \eqdef{}& \osshot(\melt) \mtimes \munit \eqdef \osshot(\melt)
\end{align*}%
Notice that $\oneshotm(\monoid)$ is a disjoint sum with the four constructors (injections) $\ospending$, $\osshot$, $\munit$ and $\bot$.
The remaining cases of composition go to $\bot$.
\begin{align*}
\mcore{\ospending} \eqdef{}& \munit & \mcore{\osshot(\melt)} \eqdef{}& \mcore\melt \\
\mcore{\munit} \eqdef{}& \munit & \mcore{\bot} \eqdef{}& \bot
\end{align*}
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\axiom{\ospending \nequiv{n} \ospending}
\infer{\melt \nequiv{n} \meltB}{\osshot(\melt) \nequiv{n} \osshot(\meltB)}
\axiom{\munit \nequiv{n} \munit}
\axiom{\bot \nequiv{n} \bot}
\end{mathpar}
$\oneshotm(-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
We obtain the following frame-preserving updates:
\begin{mathpar}
\inferH{oneshot-shoot}
{\melt \in \mval}
{\ospending \mupd \osshot(\melt)}
\inferH{oneshot-update}
{\melt \mupd \meltsB}
{\osshot(\melt) \mupd \setComp{\osshot(\meltB)}{\meltB \in \meltsB}}
\end{mathpar}
\subsection{Exclusive CMRA}
Given a cofe $\cofe$, we define a CMRA $\exm(\cofe)$ such that at most one $x \in \cofe$ can be owned:
\begin{align*}
\exm(\cofe) \eqdef{}& \exinj(\cofe) + \munit + \bot \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot} \\
\munit \mtimes \exinj(x) \eqdef{}& \exinj(x) \mtimes \munit \eqdef \exinj(x)
\exm(\cofe) \eqdef{}& \exinj(\cofe) + \bot \\
\mval_n \eqdef{}& \setComp{\melt\in\exm(\cofe)}{\melt \neq \bot}
\end{align*}
The remaining cases of composition go to $\bot$.
All cases of composition go to $\bot$.
\begin{align*}
\mcore{\exinj(x)} \eqdef{}& \munit & \mcore{\munit} \eqdef{}& \munit &
\mcore{\exinj(x)} \eqdef{}& \mnocore &
\mcore{\bot} \eqdef{}& \bot
\end{align*}
The step-indexed equivalence is inductively defined as follows:
......
......@@ -35,7 +35,7 @@
\newcommand{\upclose}{\mathord{\uparrow}}
\newcommand{\ALT}{\ |\ }
\newcommand{\spac}{\,} % a space
\newcommand{\spac}{\:} % a space
\def\All #1.{\forall #1.\spac}%
\def\Exists #1.{\exists #1.\spac}%
......@@ -56,6 +56,8 @@
\newcommand{\eqdef}{\triangleq}
\newcommand{\bnfdef}{\vcentcolon\vcentcolon=}
\newcommand{\maybe}[1]{#1^?}
\newcommand*\setComp[2]{\left\{#1\spac\middle|\spac#2\right\}}
\newcommand*\set[1]{\left\{#1\right\}}
\newcommand*\record[1]{\left\{\spac#1\spac\right\}}
......@@ -67,6 +69,7 @@
\end{array}
}
\newcommand{\op}{\textrm{op}}
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\cod}{\mathrm{cod}}
\newcommand{\chain}{\mathrm{chain}}
......@@ -112,8 +115,6 @@
%% Some commonly used identifiers
\newcommand{\op}{\textrm{op}}
\newcommand{\SProp}{\textdom{SProp}}
\newcommand{\UPred}{\textdom{UPred}}
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
......@@ -144,10 +145,9 @@
\newcommand{\f}{\mathrm{f}} % for "frame"
\newcommand{\mcar}[1]{|#1|}
\newcommand{\mcarp}[1]{\mcar{#1}^{+}}
\newcommand{\munit}{\varepsilon}
\newcommand{\mcore}[1]{\llparenthesis#1\rrparenthesis}
\newcommand{\mcore}[1]{{\mid}#1{\mid}} % using "|" here makes LaTeX diverge. WTF.
\newcommand{\mnocore}\top
\newcommand{\mtimes}{\mathbin{\cdot}}
\newcommand{\mupd}{\rightsquigarrow}
......@@ -328,6 +328,9 @@
% STANDARD DERIVED CONSTRUCTIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\unittt}{()}
\newcommand{\unit}{1}
% Agreement
\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
\newcommand{\aginj}{\textlog{ag}}
......@@ -347,6 +350,11 @@
\newcommand{\AuthInv}{\textsf{AuthInv}}
\newcommand{\Auth}{\textsf{Auth}}
% Sum
\newcommand{\csumm}{\mathrel{+_{\!\bot}}}
\newcommand{\cinl}{\textsf{inl}}
\newcommand{\cinr}{\textsf{inr}}
% One-Shot
\newcommand{\oneshotm}{\ensuremath{\textmon{OneShot}}}
\newcommand{\ospending}{\textlog{pending}}
......
......@@ -10,18 +10,6 @@ A \emph{language} $\Lang$ consists of a set \textdom{Expr} of \emph{expressions}
A reduction $\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f$ indicates that, when $\expr_1$ reduces to $\expr$, a \emph{new thread} $\expr_\f$ is forked off.
\item All values are stuck:
\[ \expr, \_ \step \_, \_, \_ \Ra \toval(\expr) = \bot \]
\item There is a predicate defining \emph{atomic} expressions satisfying
\let\oldcr\cr
\begin{mathpar}
{\All\expr. \atomic(\expr) \Ra \toval(\expr) = \bot} \and
{{
\begin{inbox}
\All\expr_1, \state_1, \expr_2, \state_2, \expr_\f. \atomic(\expr_1) \land \expr_1, \state_1 \step \expr_2, \state_2, \expr_\f \Ra {}\\\qquad\qquad\qquad\quad~~ \Exists \val_2. \toval(\expr_2) = \val_2
\end{inbox}
}}
\end{mathpar}
In other words, atomic expression \emph{reduce in one step to a value}.
It does not matter whether they fork off an arbitrary expression.
\end{itemize}
\begin{defn}
......@@ -29,6 +17,11 @@ It does not matter whether they fork off an arbitrary expression.
\[ \Exists \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \]
\end{defn}
\begin{defn}
An expression $\expr$ is said to be \emph{atomic} if it reduces in one step to a value:
\[ \All\state_1, \expr_2, \state_2, \expr_\f. \expr, \state_1 \step \expr_2, \state_2, \expr_\f \Ra \Exists \val_2. \toval(\expr_2) = \val_2 \]
\end{defn}
\begin{defn}[Context]
A function $\lctx : \textdom{Expr} \to \textdom{Expr}$ is a \emph{context} if the following conditions are satisfied:
\begin{enumerate}[itemsep=0pt]
......@@ -68,8 +61,8 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
\item A language $\Lang$
\item A locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit
\item A language $\Lang$, and
\item a locally contractive bifunctor $\iFunc : \COFEs \to \CMRAs$ defining the ghost state, such that for all COFEs $A$, the CMRA $\iFunc(A)$ has a unit. (By \lemref{lem:cmra-unit-total-core}, this means that the core of $\iFunc(A)$ is a total function.)
\end{itemize}
\noindent
......@@ -141,7 +134,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion about propositions, defined as follows:
......
......@@ -109,7 +109,7 @@ Proof.
- by intros ?; constructor; rewrite /= cmra_core_l.
- by intros ?; constructor; rewrite /= cmra_core_idemp.
- intros r1 r2; rewrite !res_included.
by intros (?&?&?); split_and!; apply cmra_core_preserving.
by intros (?&?&?); split_and!; apply cmra_core_mono.
- intros n r1 r2 (?&?&?);
split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
- intros n r r1 r2 (?&?&?) [???]; simpl in *.
......@@ -212,7 +212,7 @@ Proof.
split; first apply _.
- intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: included_preserving.
intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
Qed.
Definition resC_map {Λ} {A A' : cofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
......
......@@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}.
Global Instance from_exist_exist {A} (Φ: A uPred M): FromExist ( a, Φ a) Φ.
Proof. done. Qed.
Lemma tac_exist {A} Δ P (Φ : A uPred M) :
FromExist P Φ ( a, Δ Φ a) Δ P.
Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
Class IntoExist {A} (P : uPred M) (Φ : A uPred M) :=
into_exist : P x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
......@@ -316,4 +312,7 @@ Proof. rewrite /IntoExist=> HP ?. by rewrite HP later_exist. Qed.
Global Instance into_exist_always {A} P (Φ : A uPred M) :
IntoExist P Φ IntoExist ( P) (λ a, (Φ a))%I.
Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
Class TimelessElim (Q : uPred M) :=
timeless_elim `{!TimelessP P} : P (P - Q) Q.
End classes.
......@@ -375,6 +375,16 @@ Proof.
by rewrite right_id always_and_sep_l' wand_elim_r HQ.
Qed.
Lemma tac_timeless Δ Δ' i p P Q :
TimelessElim Q
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
by rewrite always_if_later right_id HQ timeless_elim.
Qed.
(** * Always *)
Lemma tac_always_intro Δ Q : envs_persistent Δ = true (Δ Q) Δ Q.
Proof. intros. by apply: always_intro. Qed.
......@@ -719,6 +729,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
(** * Existential *)
Lemma tac_exist {A} Δ P (Φ : A uPred M) :
FromExist P Φ ( a, Δ Φ a) Δ P.
Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
Lemma tac_exist_destruct {A} Δ i p j P (Φ : A uPred M) Q :
envs_lookup i Δ = Some (p, P) IntoExist P Φ
( a, Δ',
......
......@@ -30,6 +30,12 @@ Global Instance into_wand_pvs E1 E2 R P Q :
IntoWand R P Q IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite pvs_wand_r. Qed.
Global Instance timeless_elim_pvs E1 E2 Q : TimelessElim (|={E1,E2}=> Q).
Proof.
intros P ?. rewrite (pvs_timeless E1 P) pvs_frame_r.
by rewrite wand_elim_r pvs_trans; last set_solver.
Qed.
Class IsFSA {A} (P : iProp Λ Σ) (E : coPset)
(fsa : FSA Λ Σ A) (fsaV : Prop) (Φ : A iProp Λ Σ) := {
is_fsa : P ⊣⊢ fsa E Φ;
......@@ -48,6 +54,12 @@ Global Instance to_assert_pvs {A} P Q E (fsa : FSA Λ Σ A) fsaV Φ :
Proof.
intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r (is_fsa Q) fsa_pvs_fsa.
Qed.
Global Instance timeless_elim_fsa {A} Q E (fsa : FSA Λ Σ A) fsaV Φ :
IsFSA Q E fsa fsaV Φ TimelessElim Q.
Proof.
intros ? P ?. rewrite (is_fsa Q) -{2}fsa_pvs_fsa.
by rewrite (pvs_timeless _ P) pvs_frame_r wand_elim_r.
Qed.
Lemma tac_pvs_intro Δ E1 E2 Q : E1 = E2 (Δ Q) Δ |={E1,E2}=> Q.
Proof. intros -> ->. apply pvs_intro. Qed.
......@@ -74,26 +86,6 @@ Proof.
intros ? -> ??. rewrite (is_fsa Q) -fsa_pvs_fsa.
eapply tac_pvs_elim; set_solver.
Qed.
Lemma tac_pvs_timeless Δ Δ' E1 E2 i p P Q :
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' ={E1,E2}=> Q) Δ ={E1,E2}=> Q.
Proof.
intros ??? HQ. rewrite envs_simple_replace_sound //; simpl.
rewrite always_if_later (pvs_timeless E1 (?_ P)%I) pvs_frame_r.
by rewrite right_id wand_elim_r HQ pvs_trans; last set_solver.
Qed.
Lemma tac_pvs_timeless_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E i p P Q Φ :
IsFSA Q E fsa fsaV Φ
envs_lookup i Δ = Some (p, P)%I TimelessP P
envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ'
(Δ' fsa E Φ) Δ Q.
Proof.
intros ????. rewrite (is_fsa Q) -fsa_pvs_fsa.
eauto using tac_pvs_timeless.
Qed.
End pvs.
Tactic Notation "iPvsIntro" := apply tac_pvs_intro; first try fast_done.
......@@ -161,26 +153,5 @@ Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
iDestructHelp H as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Tactic Notation "iTimeless" constr(H) :=
match goal with
| |- _ |={_,_}=> _ =>
eapply tac_pvs_timeless with _ H _ _;
[env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|simpl]
| |- _ =>
eapply tac_pvs_timeless_fsa with _ _ _ _ H _ _ _;
[let P := match goal with |- IsFSA ?P _ _ _ _ => P end in
apply _ || fail "iTimeless: " P "not a pvs"
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|simpl]
end.
Tactic Notation "iTimeless" constr(H) "as" constr(Hs) :=
iTimeless H; iDestruct H as Hs.
Hint Extern 2 (of_envs _ _) =>
match goal with |- _ (|={_}=> _)%I => iPvsIntro end.
......@@ -501,6 +501,15 @@ Tactic Notation "iNext":=
|let P := match goal with |- FromLater ?P _ => P end in
apply _ || fail "iNext:" P "does not contain laters"|].
Tactic Notation "iTimeless" constr(H) :=
eapply tac_timeless with _ H _ _;
[let Q := match goal with |- TimelessElim ?Q => Q end in
apply _ || fail "iTimeless: cannot eliminate later in goal" Q
|env_cbv; reflexivity || fail "iTimeless:" H "not found"
|let P := match goal with |- TimelessP ?P => P end in
apply _ || fail "iTimeless: " P "not timeless"
|env_cbv; reflexivity|].
(** * Introduction tactic *)
Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" := first
[ (* (∀ _, _) *) apply tac_forall_intro; intros x
......
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