Commit cbc5b184 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' into gen_proofmode

parents 6a0e1c76 7298dd39
Pipeline #5694 passed with stages
in 3 minutes and 28 seconds
......@@ -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:
......@@ -42,6 +42,7 @@ opam:
build-coq.8.7.dev:
<<: *template
stage: build_more
variables:
OPAM_PINS: "coq version 8.7.dev"
artifacts:
......
......@@ -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
......@@ -67,7 +74,10 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
{\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$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
......@@ -106,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
......@@ -115,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'}}
......@@ -125,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
......@@ -157,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}
}
......@@ -286,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.}
......@@ -317,8 +339,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\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)
(\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}
......@@ -326,8 +348,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\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}
%\and
%\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
\end{mathpar}
\paragraph{Laws for the persistence modality.}
......@@ -340,8 +362,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\always\prop \proves \prop}
\and
\begin{array}[c]{rMcMl}
\always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
(\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
(\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB
\end{array}
\and
\begin{array}[c]{rMcMl}
......@@ -358,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
......
......@@ -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.
......
......@@ -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}
......@@ -80,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} \\
......@@ -94,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,6 +10,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.7.dev" & < "8.8~" }
"coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
"coq" { >= "8.7.dev" & < "8.8~" | (= "dev") }
"coq-stdpp" { (= "dev.2017-11-29.1") | (= "dev") }
]
......@@ -555,11 +555,15 @@ Proof.
split; first by rewrite cmra_valid_validN.
eauto using cmra_discrete_valid, cmra_validN_le with lia.
Qed.
Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : {0} x {n} x.
Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x y x {n} y.
Proof.
split; first by apply cmra_included_includedN.
intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
Qed.
Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x {0} y x {n} y.
Proof. by rewrite -!cmra_discrete_included_iff. Qed.
(** Cancelable elements *)
Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
......@@ -1231,92 +1235,93 @@ Qed.
(** ** CMRA for the option type *)
Section option.
Context {A : cmraT}.
Implicit Types x y : A.
Implicit Types a b : A.
Implicit Types ma mb : option A.
Local Arguments core _ _ !_ /.
Local Arguments pcore _ _ !_ /.
Instance option_valid : Valid (option A) := λ mx,
match mx with Some x => x | None => True end.
Instance option_validN : ValidN (option A) := λ n mx,
match mx with Some x => {n} x | None => True end.
Instance option_pcore : PCore (option A) := λ mx, Some (mx = pcore).
Instance option_valid : Valid (option A) := λ ma,
match ma with Some a => a | None => True end.
Instance option_validN : ValidN (option A) := λ n ma,
match ma with Some a => {n} a | None => True end.
Instance option_pcore : PCore (option A) := λ ma, Some (ma = pcore).
Arguments option_pcore !_ /.
Instance option_op : Op (option A) := union_with (λ x y, Some (x y)).
Definition Some_valid x : Some x x := reflexivity _.
Definition Some_validN x n : {n} Some x {n} x := reflexivity _.
Definition Some_op x y : Some (x y) = Some x Some y := eq_refl.
Lemma Some_core `{CmraTotal A} x : Some (core x) = core (Some x).
Proof. rewrite /core /=. by destruct (cmra_total x) as [? ->]. Qed.
Lemma Some_op_opM x my : Some x my = Some (x ? my).
Proof. by destruct my. Qed.
Lemma option_included (mx my : option A) :
mx my mx = None x y, mx = Some x my = Some y (x y x y).
Instance option_op : Op (option A) := union_with (λ a b, Some (a b)).
Definition Some_valid a : Some a a := reflexivity _.
Definition Some_validN a n : {n} Some a {n} a := reflexivity _.
Definition Some_op a b : Some (a b) = Some a Some b := eq_refl.
Lemma Some_core `{CmraTotal A} a : Some (core a) = core (Some a).
Proof. rewrite /core /=. by destruct (cmra_total a) as [? ->]. Qed.
Lemma Some_op_opM a ma : Some a ma = Some (a ? ma).
Proof. by destruct ma. Qed.
Lemma option_included ma mb :
ma mb ma = None a b, ma = Some a mb = Some b (a b a b).
Proof.
split.
- intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
- intros [mc Hmc].
destruct ma as [a|]; [right|by left].
destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
setoid_subst; eauto using cmra_included_l.
- intros [->|(x&y&->&->&[Hz|[z Hz]])].
+ exists my. by destruct my.
- intros [->|(a&b&->&->&[Hc|[c Hc]])].
+ exists mb. by destruct mb.
+ exists None; by constructor.
+ exists (Some z); by constructor.
+ exists (Some c); by constructor.
Qed.
Lemma option_includedN n (mx my : option A) :
mx {n} my mx = None x y, mx = Some x my = Some y (x {n} y x {n} y).
Lemma option_includedN n ma mb :
ma {n} mb ma = None x y, ma = Some x mb = Some y (x {n} y x {n} y).
Proof.
split.
- intros [mz Hmz].
destruct mx as [x|]; [right|by left].
destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
- intros [mc Hmc].
destruct ma as [a|]; [right|by left].
destruct mb as [b|]; [exists a, b|destruct mc; inversion_clear Hmc].
destruct mc as [c|]; inversion_clear Hmc; split_and?; auto;
ofe_subst; eauto using cmra_includedN_l.
- intros [->|(x&y&->&->&[Hz|[z Hz]])].
+ exists my. by destruct my.
- intros [->|(a&y&->&->&[Hc|[c Hc]])].
+ exists mb. by destruct mb.
+ exists None; by constructor.
+ exists (Some z); by constructor.
+ exists (Some c); by constructor.
Qed.
Lemma option_cmra_mixin : CmraMixin (option A).
Proof.
apply cmra_total_mixin.
- eauto.
- by intros [x|] n; destruct 1; constructor; ofe_subst.
- by intros [a|] n; destruct 1; constructor; ofe_subst.
- destruct 1; by ofe_subst.
- by destruct 1; rewrite /validN /option_validN //=; ofe_subst.
- intros [x|]; [apply cmra_valid_validN|done].
- intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
- intros [x|] [y|]; constructor; rewrite 1?comm; auto.
- intros [x|]; simpl; auto.
destruct (pcore x) as [cx|] eqn:?; constructor; eauto using cmra_pcore_l.
- intros [x|]; simpl; auto.
destruct (pcore x) as [cx|] eqn:?; simpl; eauto using cmra_pcore_idemp.
- intros mx my; setoid_rewrite option_included.
intros [->|(x&y&->&->&[?|?])]; simpl; eauto.
+ destruct (pcore x) as [cx|] eqn:?; eauto.
destruct (cmra_pcore_proper x y cx) as (?&?&?); eauto 10.
+ destruct (pcore x) as [cx|] eqn:?; eauto.
destruct (cmra_pcore_mono x y cx) as (?&?&?); eauto 10.
- intros n [x|] [y|]; rewrite /validN /option_validN /=;
- intros [a|]; [apply cmra_valid_validN|done].
- intros n [a|]; unfold validN, option_validN; eauto using cmra_validN_S.
- intros [a|] [b|] [c|]; constructor; rewrite ?assoc; auto.
- intros [a|] [b|]; constructor; rewrite 1?comm; auto.
- intros [a|]; simpl; auto.
destruct (pcore a) as [ca|] eqn:?; constructor; eauto using cmra_pcore_l.
- intros [a|]; simpl; auto.
destruct (pcore a) as [ca|] eqn:?; simpl; eauto using cmra_pcore_idemp.
- intros ma mb; setoid_rewrite option_included.
intros [->|(a&b&->&->&[?|?])]; simpl; eauto.
+ destruct (pcore a) as [ca|] eqn:?; eauto.
destruct (cmra_pcore_proper a b ca) as (?&?&?); eauto 10.
+ destruct (pcore a) as [ca|] eqn:?; eauto.
destruct (cmra_pcore_mono a b ca) as (?&?&?); eauto 10.
- intros n [a|] [b|]; rewrite /validN /option_validN /=;
eauto using cmra_validN_op_l.
- intros n mx my1 my2.
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
- intros n ma mb1 mb2.
destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
inversion_clear Hx'; auto.
+ destruct (cmra_extend n x y1 y2) as (z1&z2&?&?&?); auto.
by exists (Some z1), (Some z2); repeat constructor.
+ by exists (Some x), None; repeat constructor.
+ by exists None, (Some x); repeat constructor.
+ destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto.
by exists (Some c1), (Some c2); repeat constructor.
+ by exists (Some a), None; repeat constructor.
+ by exists None, (Some a); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
Canonical Structure optionR := CmraT (option A) option_cmra_mixin.
Global Instance option_cmra_discrete : CmraDiscrete A CmraDiscrete optionR.
Proof. split; [apply _|]. by intros [x|]; [apply (cmra_discrete_valid x)|]. Qed.
Proof. split; [apply _|]. by intros [a|]; [apply (cmra_discrete_valid a)|]. Qed.
Instance option_unit : Unit (option A) := None.
Lemma option_ucmra_mixin : UcmraMixin optionR.
......@@ -1324,61 +1329,63 @@ Section option.
Canonical Structure optionUR := UcmraT (option A) option_ucmra_mixin.
(** Misc *)
Lemma op_None mx my : mx my = None mx = None my = None.
Proof. destruct mx, my; naive_solver. Qed.
Lemma op_is_Some mx my : is_Some (mx my) is_Some mx is_Some my.
Proof. rewrite -!not_eq_None_Some op_None. destruct mx, my; naive_solver. Qed.
Lemma op_None ma mb : ma mb = None ma = None mb = None.
Proof. destruct ma, mb; naive_solver. Qed.
Lemma op_is_Some ma mb : is_Some (ma mb) is_Some ma is_Some mb.
Proof. rewrite -!not_eq_None_Some op_None. destruct ma, mb; naive_solver. Qed.
Lemma cmra_opM_assoc' a mb mc : a ? mb ? mc a ? (mb mc).
Proof. destruct mb, mc; by rewrite /= -?assoc. Qed.
Global Instance Some_core_id (x : A) : CoreId x CoreId (Some x).
Global Instance Some_core_id a : CoreId a CoreId (Some a).
Proof. by constructor. Qed.
Global Instance option_core_id (mx : option A) :
( x : A, CoreId x) CoreId mx.
Proof. intros. destruct mx; apply _. Qed.
Lemma exclusiveN_Some_l n x `{!Exclusive x} my :
{n} (Some x my) my = None.
Proof. destruct my. move=> /(exclusiveN_l _ x) []. done. Qed.
Lemma exclusiveN_Some_r n x `{!Exclusive x} my :
{n} (my Some x) my = None.
Global Instance option_core_id ma : ( x : A, CoreId x) CoreId ma.
Proof. intros. destruct ma; apply _. Qed.
Lemma exclusiveN_Some_l n a `{!Exclusive a} mb :
{n} (Some a mb) mb = None.
Proof. destruct mb. move=> /(exclusiveN_l _ a) []. done. Qed.
Lemma exclusiveN_Some_r n a `{!Exclusive a} mb :
{n} (mb Some a) mb = None.
Proof. rewrite comm. by apply exclusiveN_Some_l. Qed.
Lemma exclusive_Some_l x `{!Exclusive x} my : (Some x my) my = None.
Proof. destruct my. move=> /(exclusive_l x) []. done. Qed.
Lemma exclusive_Some_r x `{!Exclusive x} my : (my Some x) my = None.
Lemma exclusive_Some_l a `{!Exclusive a} mb : (Some a mb) mb = None.
Proof. destruct mb. move=> /(exclusive_l a) []. done. Qed.
Lemma exclusive_Some_r a `{!Exclusive a} mb : (mb Some a) mb = None.
Proof. rewrite comm. by apply exclusive_Some_l. Qed.
Lemma Some_includedN n x y : Some x {n} Some y x {n} y x {n} y.
Lemma Some_includedN n a b : Some a {n} Some b a {n} b a {n} b.
Proof. rewrite option_includedN; naive_solver. Qed.
Lemma Some_included x y : Some x Some y x y x y.
Lemma Some_included a b : Some a Some b a b a b.
Proof. rewrite option_included; naive_solver. Qed.
Lemma Some_included_2 x y : x y Some x Some y.
Lemma Some_included_2 a b : a b Some a Some b.
Proof. rewrite Some_included; eauto. Qed.
Lemma Some_includedN_total `{CmraTotal A} n x y : Some x {n} Some y x {n} y.
Lemma Some_includedN_total `{CmraTotal A} n a b : Some a {n} Some b a {n} b.
Proof. rewrite Some_includedN. split. by intros [->|?]. eauto. Qed.
Lemma Some_included_total `{CmraTotal A} x y : Some x Some y x y.
Lemma Some_included_total `{CmraTotal A} a b : Some a Some b a b.
Proof. rewrite Some_included. split. by intros [->|?]. eauto. Qed.
Lemma Some_includedN_exclusive n x `{!Exclusive x} y :
Some x {n} Some y {n} y x {n} y.
Lemma Some_includedN_exclusive n a `{!Exclusive a} b :
Some a {n} Some b {n} b a {n} b.
Proof. move=> /Some_includedN [//|/exclusive_includedN]; tauto. Qed.
Lemma Some_included_exclusive x `{!Exclusive x} y :
Some x Some y y x y.
Lemma Some_included_exclusive a `{!Exclusive a} b :
Some a Some b b a b.
Proof. move=> /Some_included [//|/exclusive_included]; tauto. Qed.
Lemma is_Some_includedN n mx my : mx {n} my is_Some mx is_Some my.
Lemma is_Some_includedN n ma mb : ma {n} mb is_Some ma is_Some mb.
Proof. rewrite -!not_eq_None_Some option_includedN. naive_solver. Qed.
Lemma is_Some_included mx my : mx my is_Some mx is_Some my.
Lemma is_Some_included ma mb : ma mb is_Some ma is_Some mb.
Proof. rewrite -!not_eq_None_Some option_included. naive_solver. Qed.
Global Instance cancelable_Some x :
IdFree x Cancelable x Cancelable (Some x).
Global Instance cancelable_Some a :
IdFree a Cancelable a Cancelable (Some a).
Proof.
intros Hirr ?? [y|] [z|] ? EQ; inversion_clear EQ.
- constructor. by apply (cancelableN x).
- destruct (Hirr y); [|eauto using dist_le with lia].
by eapply (cmra_validN_op_l 0 x y), (cmra_validN_le n); last lia.
- destruct (Hirr z); [|symmetry; eauto using dist_le with lia].
intros Hirr ?? [b|] [c|] ? EQ; inversion_clear EQ.
- constructor. by apply (cancelableN a).
- destruct (Hirr b); [|eauto using dist_le with lia].
by eapply (cmra_validN_op_l 0 a b), (cmra_validN_le n); last lia.
- destruct (Hirr c); [|symmetry; eauto using dist_le with lia].
by eapply (cmra_validN_le n); last lia.
- done.
Qed.
......@@ -1389,35 +1396,37 @@ Arguments optionUR : clear implicits.
Section option_prod.
Context {A B : cmraT}.
Implicit Types a : A.
Implicit Types b : B.
Lemma Some_pair_includedN n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) {n} Some (x2,y2) Some x1 {n} Some x2 Some y1 {n} Some y2.
Lemma Some_pair_includedN n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) Some a1 {n} Some a2 Some b1 {n} Some b2.
Proof. rewrite !Some_includedN. intros [[??]|[??]%prod_includedN]; eauto. Qed.
Lemma Some_pair_includedN_total_1 `{CmraTotal A} n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) {n} Some (x2,y2) x1 {n} x2 Some y1 {n} Some y2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ x1). Qed.
Lemma Some_pair_includedN_total_2 `{CmraTotal B} n (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) {n} Some (x2,y2) Some x1 {n} Some x2 y1 {n} y2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ y1). Qed.
Lemma Some_pair_included (x1 x2 : A) (y1 y2 : B) :
Some (x1,y1) Some (x2,y2) Some x1 Some x2 Some y1 Some y2.
Lemma Some_pair_includedN_total_1 `{CmraTotal A} n a1 a2 b1 b2 :
Some (a1,b1) {n} Some (a2,b2) a1 {n} a2 Some b1 {n} Some b2.
Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ a1). Qed.
Lemma