Commit c5e25a27 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' into swasey/progress2

parents c056a95c adc0a095
......@@ -3,6 +3,7 @@ image: ralfjung/opam-ci:latest
stages:
- build
- deploy
- build_more
variables:
CPU_CORES: "9"
......@@ -19,7 +20,6 @@ variables:
- 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
- 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
- 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
- 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
cache:
key: "$CI_JOB_NAME"
paths:
......@@ -52,6 +52,7 @@ reverse-deps:
build-coq.8.7.dev:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev coq-mathcomp-ssreflect version dev"
except:
......@@ -68,7 +69,6 @@ build-coq.8.6.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.6.1 coq-mathcomp-ssreflect version 1.6.4"
VALIDATE: "1"
artifacts:
paths:
- build-time.txt
......
......@@ -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
......
......@@ -14,7 +14,7 @@ theories/algebra/dra.v
theories/algebra/cofe_solver.v
theories/algebra/agree.v
theories/algebra/excl.v
theories/algebra/iprod.v
theories/algebra/functions.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
......
......@@ -37,7 +37,8 @@ Elements that cannot be distinguished by programs within $n$ steps remain indist
The category $\OFEs$ consists of OFEs as objects, and non-expansive functions as arrows.
\end{defn}
Note that $\OFEs$ is cartesian closed. In particular:
Note that $\OFEs$ is bicartesian closed, \ie it has all sums, products and exponentials as well as an initial and a terminal object.
In particular:
\begin{defn}
Given two OFEs $\ofe$ and $\ofeB$, the set of non-expansive functions $\set{f : \ofe \nfn \ofeB}$ is itself an OFE with
\begin{align*}
......
......@@ -32,18 +32,25 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
\begin{align*}
\type \bnfdef{}&
\sigtype \mid
0 \mid
1 \mid
\type + \type \mid
\type \times \type \mid
\type \to \type
\\[0.4em]
\term, \prop, \pred \bnfdef{}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
\textlog{abort}\; \term \mid
() \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam \var:\type.\term \mid
\term(\term) \mid
\\&
\textlog{inj}_i\; \term \mid
\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term \mid \Ret\textlog{inj}_2\; \var. \term \;\textlog{end} \mid
%
\melt \mid
\mcore\term \mid
\term \mtimes \term \mid
......@@ -63,12 +70,16 @@ 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.
Well-typedness forces recursive definitions to be \emph{guarded}:
In $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
Furthermore, the type of the definition must be \emph{complete}.
The type $\Prop$ is complete, and if $\type$ is complete, then so is $\type' \to \type$.
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.}
......@@ -105,7 +116,10 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
}{
\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
}
%%% products
%%% empty, unit, products, sums
\and
\infer{\vctx \proves \wtt\term{0}}
{\vctx \proves \wtt{\textlog{abort}\; \term}\type}
\and
\axiom{\vctx \proves \wtt{()}{1}}
\and
......@@ -114,6 +128,14 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
\and
\infer{\vctx \proves \wtt\term{\type_i} \and i \in \{1, 2\}}
{\vctx \proves \wtt{\textlog{inj}_i\;\term}{\type_1 + \type_2}}
\and
\infer{\vctx \proves \wtt\term{\type_1 + \type_2} \and
\vctx, \var:\type_1 \proves \wtt{\term_1}\type \and
\vctx, \varB:\type_2 \proves \wtt{\term_2}\type}
{\vctx \proves \wtt{\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term_1 \mid \Ret\textlog{inj}_2\; \varB. \term_2 \;\textlog{end}}{\type}}
%%% functions
\and
\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
......@@ -124,7 +146,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
{\vctx \proves \wtt{\term(\termB)}{\type'}}
%%% monoids
\and
\infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
\infer{}{\vctx \proves \wtt\melt{\textlog{M}}}
\and
\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
\and
......@@ -156,7 +178,8 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
\and
\infer{
\vctx, \var:\type \proves \wtt{\term}{\type} \and
\text{$\var$ is guarded in $\term$}
\text{$\var$ is guarded in $\term$} \and
\text{$\type$ is complete}
}{
\vctx \proves \wtt{\MU \var:\type. \term}{\type}
}
......@@ -175,6 +198,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}}
......@@ -282,7 +308,7 @@ This is entirely standard.
% {}
% {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
\end{mathparpagebreakable}
Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.
\paragraph{Laws of (affine) bunched implications.}
......@@ -303,7 +329,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}
(\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q) \\
\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) &\proves& P =_{\Prop} 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,8 +362,7 @@ 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)} \\
(\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
\and
......@@ -332,7 +380,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\prop \proves \propB}
{\later\prop \proves \later{\propB}}
\and
\infer[L{\"o}b]
\inferhref{L{\"o}b}{Loeb}
{}
{(\later\prop\Ra\prop) \proves \prop}
\and
......@@ -344,7 +392,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 +442,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 +454,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:
......
......@@ -35,8 +35,13 @@ We collect here some important and frequently used derived proof rules.
\infer{}
{\prop \proves \later\prop}
\infer{}
{\TRUE \proves \plainly\TRUE}
\end{mathparpagebreakable}
Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.
\subsection{Persistent assertions}
We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.
......
......@@ -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/}}
......
......@@ -9,11 +9,13 @@ The semantic domains are interpreted as follows:
\[
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{\Prop} &\eqdef& \UPred(\monoid) \\
\Sem{\textlog{M}} &\eqdef& \monoid
\Sem{\textlog{M}} &\eqdef& \monoid \\
\Sem{0} &\eqdef& \Delta \emptyset \\
\Sem{1} &\eqdef& \Delta \{ () \}
\end{array}
\qquad\qquad
\begin{array}[t]{@{}l@{\ }c@{\ }l@{}}
\Sem{1} &\eqdef& \Delta \{ () \} \\
\Sem{\type + \type'} &\eqdef& \Sem{\type} + \Sem{\type} \\
\Sem{\type \times \type'} &\eqdef& \Sem{\type} \times \Sem{\type} \\
\Sem{\type \to \type'} &\eqdef& \Sem{\type} \nfn \Sem{\type} \\
\end{array}
......@@ -54,10 +56,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}
......@@ -79,9 +82,15 @@ For every definition, we have to show all the side-conditions: The maps have to
\Sem{\vctx \proves \MU \var:\type. \term : \type}_\gamma &\eqdef
\mathit{fix}(\Lam \termB : \Sem{\type}. \Sem{\vctx, x : \type \proves \term : \type}_{\mapinsert \var \termB \gamma}) \\
~\\
\Sem{\vctx \proves \textlog{abort}\;\term : \type}_\gamma &\eqdef \mathit{abort}_{\Sem\type}(\Sem{\vctx \proves \term:0}_\gamma) \\
\Sem{\vctx \proves () : 1}_\gamma &\eqdef () \\
\Sem{\vctx \proves (\term_1, \term_2) : \type_1 \times \type_2}_\gamma &\eqdef (\Sem{\vctx \proves \term_1 : \type_1}_\gamma, \Sem{\vctx \proves \term_2 : \type_2}_\gamma) \\
\Sem{\vctx \proves \pi_i(\term) : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
\Sem{\vctx \proves \pi_i\; \term : \type_i}_\gamma &\eqdef \pi_i(\Sem{\vctx \proves \term : \type_1 \times \type_2}_\gamma) \\
\Sem{\vctx \proves \textlog{inj}_i\;\term : \type_1 + \type_2}_\gamma &\eqdef \mathit{inj}_i(\Sem{\vctx \proves \term : \type_i}_\gamma) \\
\Sem{\vctx \proves \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var_1. \term_1 \mid \Ret\textlog{inj}_2\; \var_2. \term_2 \;\textlog{end} : \type }_\gamma &\eqdef
\Sem{\vctx, \var_i:\type_i \proves \term_i : \type}_{\mapinsert{\var_i}\termB \gamma} \\
&\qquad \text{where $\Sem{\vctx \proves \term : \type_1 + \type_2}_\gamma = \mathit{inj}_i(\termB)$}
\\
~\\
\Sem{ \melt : \textlog{M} }_\gamma &\eqdef \melt \\
\Sem{\vctx \proves \mcore\term : \textlog{M}}_\gamma &\eqdef \mcore{\Sem{\vctx \proves \term : \textlog{M}}_\gamma} \\
......@@ -93,6 +102,7 @@ For every definition, we have to show all the side-conditions: The maps have to
An environment $\vctx$ is interpreted as the set of
finite partial functions $\rho$, with $\dom(\rho) = \dom(\vctx)$ and
$\rho(x)\in\Sem{\vctx(x)}$.
Above, $\mathit{fix}$ is the fixed-point on COFEs, and $\mathit{abort}_T$ is the unique function $\emptyset \to T$.
\paragraph{Logical entailment.}
We can now define \emph{semantic} logical entailment.
......
......@@ -10,7 +10,7 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq" { (>= "8.6.1" & < "8.8~") | (= "dev") }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
]
......@@ -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.
......
......@@ -208,7 +208,7 @@ Lemma auth_frag_mono a b : a ≼ b → ◯ a ≼ ◯ b.
Proof. intros [c ->]. rewrite auth_frag_op. apply cmra_included_l. Qed.
Global Instance auth_frag_sep_homomorphism :
MonoidHomomorphism op op () (Auth None).
MonoidHomomorphism op op () (@Auth A None).
Proof. by split; [split; try apply _|]. Qed.
Lemma auth_both_op a b : Auth (Excl' a) b a b.
......
This diff is collapsed.
......@@ -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 ->.
......
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Definition ofe_fun_insert `{EqDecision A} {B : A ofeT}
(x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Instance: Params (@ofe_fun_insert) 5.
Definition ofe_fun_singleton `{Finite A} {B : A ucmraT}
(x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
Instance: Params (@ofe_fun_singleton) 5.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A ofeT}.
Implicit Types x : A.
Implicit Types f g : ofe_fun B.
(** Properties of ofe_fun_insert. *)
Global Instance ofe_fun_insert_ne x :
NonExpansive2 (ofe_fun_insert (B:=B) x).
Proof.
intros n y1 y2 ? f1 f2 ? x'; rewrite /ofe_fun_insert.
by destruct (decide _) as [[]|].
Qed.
Global Instance ofe_fun_insert_proper x :
Proper (() ==> () ==> ()) (ofe_fun_insert (B:=B) x) := ne_proper_2 _.
Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
Proof.
rewrite /ofe_fun_insert; destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).
Qed.
Lemma ofe_fun_lookup_insert_ne f x x' y :
x x' (ofe_fun_insert x y f) x' = f x'.
Proof. by rewrite /ofe_fun_insert; destruct (decide _). Qed.
Global Instance ofe_fun_insert_discrete f x y :
Discrete f Discrete y Discrete (ofe_fun_insert x y f).
Proof.
intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- rewrite ofe_fun_lookup_insert.
apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert.
- rewrite ofe_fun_lookup_insert_ne //.
apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert_ne.
Qed.
End ofe.
Section cmra.
Context `{Finite A} {B : A ucmraT}.
Implicit Types x : A.
Implicit Types f g : ofe_fun B.
Global Instance ofe_fun_singleton_ne x :
NonExpansive (ofe_fun_singleton x : B x _).
Proof. intros n y1 y2 ?; apply ofe_fun_insert_ne. done. by apply equiv_dist. Qed.
Global Instance ofe_fun_singleton_proper x :
Proper (() ==> ()) (ofe_fun_singleton x) := ne_proper _.
Lemma ofe_fun_lookup_singleton x (y : B x) : (ofe_fun_singleton x y) x = y.
Proof. by rewrite /ofe_fun_singleton ofe_fun_lookup_insert. Qed.
Lemma ofe_fun_lookup_singleton_ne x x' (y : B x) :
x x' (ofe_fun_singleton x y) x' = ε.
Proof. intros; by rewrite /ofe_fun_singleton ofe_fun_lookup_insert_ne. Qed.
Global Instance ofe_fun_singleton_discrete x (y : B x) :
( i, Discrete (ε : B i)) Discrete y Discrete (ofe_fun_singleton x y).
Proof. apply _. Qed.
Lemma ofe_fun_singleton_validN n x (y : B x) : {n} ofe_fun_singleton x y {n} y.
Proof.
split; [by move=>/(_ x); rewrite ofe_fun_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
rewrite ?ofe_fun_lookup_singleton ?ofe_fun_lookup_singleton_ne //.
by apply ucmra_unit_validN.
Qed.
Lemma ofe_fun_core_singleton x (y : B x) :
core (ofe_fun_singleton x y) ofe_fun_singleton x (core y).
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
?ofe_fun_lookup_singleton_ne // (core_id_core ).
Qed.
Global Instance ofe_fun_singleton_core_id x (y : B x) :
CoreId y CoreId (ofe_fun_singleton x y).
Proof. by rewrite !core_id_total ofe_fun_core_singleton=> ->. Qed.
Lemma ofe_fun_op_singleton (x : A) (y1 y2 : B x) :
ofe_fun_singleton x y1 ofe_fun_singleton x y2 ofe_fun_singleton x (y1 y2).
Proof.
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton.
- by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton_ne // left_id.
Qed.
Lemma ofe_fun_insert_updateP x (P : B x Prop) (Q : ofe_fun B Prop) g y1 :
y1 ~~>: P ( y2, P y2 Q (ofe_fun_insert x y2 g))
ofe_fun_insert x y1 g ~~>: Q.
Proof.
intros Hy1 HP; apply cmra_total_updateP.
intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
{ move: (Hg x). by rewrite ofe_fun_lookup_op ofe_fun_lookup_insert. }
exists (ofe_fun_insert x y2 g); split; [auto|].
intros x'; destruct (decide (x' = x)) as [->|];
rewrite ofe_fun_lookup_op ?ofe_fun_lookup_insert //; [].
move: (Hg x'). by rewrite ofe_fun_lookup_op !ofe_fun_lookup_insert_ne.
Qed.
Lemma ofe_fun_insert_updateP' x (P : B x Prop) g y1 :
y1 ~~>: P
ofe_fun_insert x y1 g ~~>: λ g', y2, g' = ofe_fun_insert x y2 g P y2.
Proof. eauto using ofe_fun_insert_updateP. Qed.
Lemma ofe_fun_insert_update g x y1 y2 :
y1 ~~> y2 ofe_fun_insert x y1 g ~~> ofe_fun_insert x y2 g.
Proof.
rewrite !cmra_update_updateP; eauto using ofe_fun_insert_updateP with subst.
Qed.
Lemma ofe_fun_singleton_updateP x (P : B x Prop) (Q : ofe_fun B Prop) y1 :
y1 ~~>: P ( y2, P y2 Q (ofe_fun_singleton x y2))
ofe_fun_singleton x y1 ~~>: Q.
Proof. rewrite /ofe_fun_singleton; eauto using ofe_fun_insert_updateP. Qed.
Lemma ofe_fun_singleton_updateP' x (P : B x Prop) y1 :
y1 ~~>: P
ofe_fun_singleton x y1 ~~>: λ g, y2, g = ofe_fun_singleton x y2 P y2.
Proof. eauto using ofe_fun_singleton_updateP. Qed.
Lemma ofe_fun_singleton_update x (y1 y2 : B x) :
y1 ~~> y2 ofe_fun_singleton x y1 ~~> ofe_fun_singleton x y2.
Proof. eauto using ofe_fun_insert_update. Qed.
Lemma ofe_fun_singleton_updateP_empty x (P : B x Prop) (Q : ofe_fun B Prop) :
ε ~~>: P ( y2, P y2 Q (ofe_fun_singleton x y2)) ε ~~>: Q.
Proof.
intros Hx HQ; apply cmra_total_updateP.
intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
exists (ofe_fun_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton.
- rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton_ne //. apply Hg.
Qed.
Lemma ofe_fun_singleton_updateP_empty' x (P : B x Prop) :
ε ~~>: P ε ~~>: λ g, y2, g = ofe_fun_singleton x y2 P y2.
Proof. eauto using ofe_fun_singleton_updateP_empty. Qed.
Lemma ofe_fun_singleton_update_empty x (y : B x) :
ε ~~> y ε ~~> ofe_fun_singleton x y.
Proof.
rewrite !cmra_update_updateP;
eauto using ofe_fun_singleton_updateP_empty with subst.
Qed.
End cmra.
......@@ -7,6 +7,7 @@ Set Default Proof Using "Type".
Section cofe.
Context `{Countable K} {A : ofeT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
i, m1 !! i {n} m2 !! i.
......
This diff is collapsed.
......@@ -6,6 +6,7 @@ Set Default Proof Using "Type".
Section cofe.
Context {A : ofeT}.
Implicit Types l : list A.
Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
......
......@@ -190,9 +190,7 @@ Section ofe.
split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
Qed.
Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x {0} y x {n} y.
Proof.
split=> ?. by apply equiv_dist, (discrete _). eauto using dist_le with lia.
Qed.
Proof. by rewrite -!discrete_iff. Qed.
End ofe.
(** Contractive functions *)
......@@ -511,42 +509,6 @@ Section fixpointAB_ne.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
End fixpointAB_ne.
(** Function space *)
(* We make [ofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition ofe_fun (A : Type) (B : ofeT) := A B.
Section ofe_fun.
Context {A : Type} {B : ofeT}.
Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, x, f x g x.
Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, x, f x {n} g x.
Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
intros Hfg k; apply equiv_dist=> n; apply Hfg.
- intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
Program Definition ofe_fun_chain `(c : chain ofe_funC)
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
{ compl c x := compl (ofe_fun_chain c x) }.
Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
End ofe_fun.
Arguments ofe_funC : clear implicits.
Notation "A -c> B" :=
(ofe_funC A B) (at level 99, B at level 200, right associativity).
Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
Inhabited (A -c> B) := populate (λ _, inhabitant).
(** Non-expansive function space *)
Record ofe_mor (A B : ofeT) : Type := CofeMor {
ofe_mor_car :> A B;
......@@ -762,37 +724,6 @@ Proof.
by apply prodC_map_ne; apply cFunctor_contractive.
Qed.
Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') :
NonExpansive (compose f : (A -c> B) A -c> B'