diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1fa75c28797a6a1f7544030ae2f3c606c272fcea..8ab85ac5c05a8870df09ef77cb295a5aa31f21f3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -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:
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 9cfed25eaca982e31b347286ce1b1b4eabe61bd7..3ba0967042888774ba91ee1af53f50d672ba8acc 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -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*}
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index f0b97ad9c950ade18eae79cfd362e1052dca58d4..2a45cae7cbd88a1fc94619caf86a6a06aadb95df 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -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
diff --git a/docs/ghost-state.tex b/docs/ghost-state.tex
index d8cd9b8fa4d95d17197ec5a4dd8672854f2deede..bd10d54efa60000c9290d79789776440300a521a 100644
--- a/docs/ghost-state.tex
+++ b/docs/ghost-state.tex
@@ -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.
diff --git a/docs/model.tex b/docs/model.tex
index af3ed1e4fd53c6eb62d3d2e139e68589bc12669b..6100fb39be49d0689d410ad482466b1962b4a34e 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -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.
diff --git a/opam b/opam
index f15ec44511f6d54609188b7f973bb8133d67400f..5d2cef8c9c67aa0b71e0c65377d97c3ea58ee6bc 100644
--- a/opam
+++ b/opam
@@ -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") }
]
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 8c0aadf791ecb702288bf281048c42c97cccc463..0c1a040fe84a3579d0eb511bb74d34e1ac80caf9 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -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 Some_pair_includedN_total_2 `{CmraTotal B} n a1 a2 b1 b2 :
+ Some (a1,b1) ≼{n} Some (a2,b2) → Some a1 ≼{n} Some a2 ∧ b1 ≼{n} b2.
+ Proof. intros ?%Some_pair_includedN. by rewrite -(Some_includedN_total _ b1). Qed.
+
+ Lemma Some_pair_included a1 a2 b1 b2 :
+ Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ Some b1 ≼ Some b2.
Proof. rewrite !Some_included. intros [[??]|[??]%prod_included]; eauto. Qed.
- Lemma Some_pair_included_total_1 `{CmraTotal A} (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼ Some (x2,y2) → x1 ≼ x2 ∧ Some y1 ≼ Some y2.
- Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total x1). Qed.
- Lemma Some_pair_included_total_2 `{CmraTotal B} (x1 x2 : A) (y1 y2 : B) :
- Some (x1,y1) ≼ Some (x2,y2) → Some x1 ≼ Some x2 ∧ y1 ≼ y2.
- Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total y1). Qed.
+ Lemma Some_pair_included_total_1 `{CmraTotal A} a1 a2 b1 b2 :
+ Some (a1,b1) ≼ Some (a2,b2) → a1 ≼ a2 ∧ Some b1 ≼ Some b2.
+ Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total a1). Qed.
+ Lemma Some_pair_included_total_2 `{CmraTotal B} a1 a2 b1 b2 :
+ Some (a1,b1) ≼ Some (a2,b2) → Some a1 ≼ Some a2 ∧ b1 ≼ b2.
+ Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
End option_prod.
Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
CmraMorphism (fmap f : option A → option B).
Proof.
split; first apply _.
- - intros n [x|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
- - move=> [x|] //. by apply Some_proper, cmra_morphism_pcore.
- - move=> [x|] [y|] //=. by rewrite -(cmra_morphism_op f).
+ - intros n [a|] ?; rewrite /cmra_validN //=. by apply (cmra_morphism_validN f).
+ - move=> [a|] //. by apply Some_proper, cmra_morphism_pcore.
+ - move=> [a|] [b|] //=. by rewrite -(cmra_morphism_op f).
Qed.
Program Definition optionRF (F : rFunctor) : rFunctor := {|
@@ -1464,7 +1473,7 @@ Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
-(* Dependently-typed functions over a finite domain *)
+(* Dependently-typed functions over a finite discrete domain *)
Section ofe_fun_cmra.
Context `{Hfin : Finite A} {B : A → ucmraT}.
Implicit Types f g : ofe_fun B.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index a4c6a03a727cd2165fb553fb6b0e148c1ad8de33..a0fd519b00d28b13f1a2587cd4b7c4acd91a7cdd 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -25,7 +25,7 @@ Section ofe.
by destruct (decide _) as [[]|].
Qed.
Global Instance ofe_fun_insert_proper x :
- Proper ((≡) ==> (≡) ==> (≡)) (ofe_fun_insert x) := ne_proper_2 _.
+ 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.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a09b287e85b6afdfd71b15e2226985ae528e6e50..b9a995537ea553ed15d6c179b48769353d47beb4 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -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.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index ed4736a1875450294db3b1b7474a06c9357e0fe8..67f56c2f782c5a6844f9c9998799824eeb3821f3 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -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).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 54ca4c7d18a88f295d4e7e80c35522150d2f3166..12ceaeb1d384a9a99976a025713675d318827631 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -186,9 +186,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 *)
@@ -1176,7 +1174,7 @@ Qed.
Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
-Instance ofe_funCF_contractive `{Finite C} (F : C → cFunctor) :
+Instance ofe_funCF_contractive {C} (F : C → cFunctor) :
(∀ c, cFunctorContractive (F c)) → cFunctorContractive (ofe_funCF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index 169b78a66aea71c24160702ae82502477cf9fb16..3721303550b60a3033b1e82ca6cdbe7ef52b203b 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -77,6 +77,12 @@ Lemma cmra_update_op x1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1
Proof.
rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.
+
+Lemma cmra_update_op_l x y : x â‹… y ~~> x.
+Proof. intros n mz. rewrite comm cmra_opM_assoc. apply cmra_validN_op_r. Qed.
+Lemma cmra_update_op_r x y : x â‹… y ~~> y.
+Proof. rewrite comm. apply cmra_update_op_l. Qed.
+
Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
Proof.
intros H n mz Hmz. apply H, Hmz.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c80b066b045d4ae7bce928ff18f2ef98ed8f672a..c37e3b6780f7456a7a85c06c72957bb20c7c513f 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -72,6 +72,14 @@ Section to_gen_heap.
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
+Lemma gen_heap_init `{gen_heapPreG L V Σ} σ :
+ (|==> ∃ _ : gen_heapG L V Σ, gen_heap_ctx σ)%I.
+Proof.
+ iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
+ { apply: auth_auth_valid. exact: to_gen_heap_valid. }
+ iModIntro. by iExists (GenHeapG L V Σ _ _ _ γ).
+Qed.
+
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
diff --git a/theories/heap_lang/adequacy.v b/theories/heap_lang/adequacy.v
index 135811da52f0c29ecda9cc66eca7b71608fda841..a184a59657dfd639315dd8aa4416f314160e0bd5 100644
--- a/theories/heap_lang/adequacy.v
+++ b/theories/heap_lang/adequacy.v
@@ -18,10 +18,8 @@ Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
(∀ `{heapG Σ}, WP e {{ v, ⌜φ v⌠}}%I) →
adequate e σ φ.
Proof.
- intros Hwp; eapply (wp_adequacy _ _); iIntros (?).
- iMod (own_alloc (◠to_gen_heap σ)) as (γ) "Hh".
- { apply: auth_auth_valid. exact: to_gen_heap_valid. }
- iModIntro. iExists (λ σ, own γ (◠to_gen_heap σ)); iFrame.
- set (Hheap := GenHeapG loc val Σ _ _ _ γ).
- by iApply (Hwp (HeapG _ _ _)).
+ intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
+ iMod (gen_heap_init σ) as (?) "Hh".
+ iModIntro. iExists gen_heap_ctx. iFrame "Hh".
+ iApply (Hwp (HeapG _ _ _)).
Qed.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 2c218e4b7c970b872d70c41920552007f38d1e9a..bc0f293de76332435089b43d57022a2425eb5ee7 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,6 +5,18 @@ From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
+Lemma tac_wp_expr_eval `{heapG Σ} Δ E Φ e e' :
+ e = e' →
+ envs_entails Δ (WP e' @ E {{ Φ }}) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. by intros ->. Qed.
+
+Ltac wp_expr_eval t :=
+ try iStartProof;
+ try (eapply tac_wp_expr_eval; [t; reflexivity|]).
+
+Ltac wp_expr_simpl := wp_expr_eval simpl.
+Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
+
Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
PureExec φ e1 e2 →
φ →
@@ -34,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
[apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
- |simpl_subst; try wp_value_head (* new goal *)
+ |wp_expr_simpl_subst; try wp_value_head (* new goal *)
])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
@@ -54,15 +66,16 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
Tactic Notation "wp_case" := wp_pure (Case _ _ _).
Tactic Notation "wp_match" := wp_case; wp_let.
-Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
- envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e f :
+ f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
+ envs_entails Δ (WP e @ E {{ v, WP f (of_val v) @ E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ E {{ Φ }}).
-Proof. rewrite /envs_entails=> ->. by apply: wp_bind. Qed.
+Proof. rewrite /envs_entails=> -> ->. by apply: wp_bind. Qed.
Ltac wp_bind_core K :=
lazymatch eval hnf in K with
| [] => idtac
- | _ => apply (tac_wp_bind K); simpl
+ | _ => eapply (tac_wp_bind K); [simpl; reflexivity|lazy beta]
end.
Tactic Notation "wp_bind" open_constr(efoc) :=
@@ -155,7 +168,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) =>
reshape_expr e ltac:(fun K e' =>
- wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
+ wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
lazymatch iTypeOf H with
| Some (_,?P) => fail "wp_apply: cannot apply" P
end
@@ -174,7 +187,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
|first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split;
[env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
- |simpl; try wp_value_head]]
+ |wp_expr_simpl; try wp_value_head]]
| _ => fail "wp_alloc: not a 'wp'"
end.
@@ -191,7 +204,7 @@ Tactic Notation "wp_load" :=
[apply _
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_load: not a 'wp'"
end.
@@ -207,7 +220,7 @@ Tactic Notation "wp_store" :=
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
|env_cbv; reflexivity
- |simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
+ |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
| _ => fail "wp_store: not a 'wp'"
end.
@@ -223,7 +236,7 @@ Tactic Notation "wp_cas_fail" :=
|let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
|try congruence
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_fail: not a 'wp'"
end.
@@ -240,6 +253,6 @@ Tactic Notation "wp_cas_suc" :=
iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
|try congruence
|env_cbv; reflexivity
- |simpl; try wp_value_head]
+ |wp_expr_simpl; try wp_value_head]
| _ => fail "wp_cas_suc: not a 'wp'"
end.
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 51681a36571459c2906a42b24794d8fbce80cfbf..6c6cb5072e6c79f64f29d69146ded474c0e2c76f 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -10,6 +10,16 @@ Section LiftingTests.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val → iProp Σ.
+ Definition simpl_test :
+ ⌜(10 = 4 + 6)%nat⌠-∗
+ WP let: "x" := ref #1 in "x" <- !"x";; !"x" {{ v, ⌜v = #1⌠}}.
+ Proof.
+ iIntros "?". wp_alloc l. repeat (wp_pure _) || wp_load || wp_store.
+ match goal with
+ | |- context [ (10 = 4 + 6)%nat ] => done
+ end.
+ Qed.
+
Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index 28f75f6c8a26e77a3c6ceea613114910dac6c48e..01441c800708b8ba694685b2b7bfc5ddf8646215 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,7 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
{{{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }}}.
Proof.
iIntros (Φ) "[Hl Ht] HΦ".
- iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
+ iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]").