diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3853fde1690ea8e268ab7956ecda3c129f0d6197..cfd5f40d65b455f251f9fc76133d5e60b5c2dce3 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,13 +7,19 @@ Coq development, but not every API-breaking change is listed. Changes marked
This version accompanies the final ICFP paper.
-* [# algebra] Make the core of an RA or CMRA a partial function.
+* [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.
+* [program_logic/lifting] Lifting lemmas no longer round-trip through a
+ user-chosen predicate to define the configurations we can reduce to; they
+ directly relate to the operational semantics. This is equivalent and
+ much simpler to read.
+ Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
+ are removed.
## Iris 2.0-rc1
diff --git a/ProofMode.md b/ProofMode.md
index 5a086022abc189210c9db55f233ac297e6876661..ed7f788813bfa06bec042d9bace9c9b1b2bc26cd 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -1,13 +1,20 @@
Tactic overview
===============
+Many of the tactics below apply to more goals than described in this document
+since the behavior of these tactics can be tuned via instances of the type
+classes in the file `proofmode/classes`. Most notable, many of the tactics can
+be applied when the to be introduced or to be eliminated connective appears
+under a later, a primitive view shift, or in the conclusion of a weakest
+precondition connective.
+
Applying hypotheses and lemmas
------------------------------
- `iExact "H"` : finish the goal if the conclusion matches the hypothesis `H`
- `iAssumption` : finish the goal if the conclusion matches any hypothesis
-- `iApply trm` : match the conclusion of the current goal against the
- conclusion of `tetrmrm` and generates goals for the premises of `trm`. See
+- `iApply pm_trm` : match the conclusion of the current goal against the
+ conclusion of `pm_trm` and generates goals for the premises of `pm_trm`. See
proof mode terms below.
Context management
@@ -23,9 +30,10 @@ Context management
`x1 ... xn` into universal quantifiers. The symbol `★` can be used to revert
the entire spatial context.
- `iRename "H1" into "H2"` : rename the hypothesis `H1` into `H2`.
-- `iSpecialize trm` : instantiate universal quantifiers and eliminate
- implications/wands of a hypothesis `trm`. See proof mode terms below.
-- `iPoseProof trm as "H"` : put `trm` into the context as a new hypothesis `H`.
+- `iSpecialize pm_trm` : instantiate universal quantifiers and eliminate
+ implications/wands of a hypothesis `pm_trm`. See proof mode terms below.
+- `iPoseProof pm_trm as "H"` : put `pm_trm` into the context as a new hypothesis
+ `H`.
- `iAssert P with "spat" as "ipat"` : create a new goal with conclusion `P` and
put `P` in the context of the original goal. The specialization pattern
`spat` specifies which hypotheses will be consumed by proving `P` and the
@@ -52,11 +60,11 @@ Elimination of logical connectives
----------------------------------
- `iExFalso` : Ex falso sequitur quod libet.
-- `iDestruct trm as (x1 ... xn) "spat1 ... spatn"` : elimination of existential
- quantifiers using Coq introduction patterns `x1 ... xn` and elimination of
- object level connectives using the proof mode introduction patterns
- `ipat1 ... ipatn`.
-- `iDestruct trm as %cpat` : elimination of a pure hypothesis using the Coq
+- `iDestruct pm_trm as (x1 ... xn) "spat1 ... spatn"` : elimination of
+ existential quantifiers using Coq introduction patterns `x1 ... xn` and
+ elimination of object level connectives using the proof mode introduction
+ patterns `ipat1 ... ipatn`.
+- `iDestruct pm_trm as %cpat` : elimination of a pure hypothesis using the Coq
introduction pattern `cpat`.
Separating logic specific tactics
@@ -75,15 +83,15 @@ The later modality
Rewriting
---------
-- `iRewrite trm` : rewrite an equality in the conclusion.
-- `iRewrite trm in "H"` : rewrite an equality in the hypothesis `H`.
+- `iRewrite pm_trm` : rewrite an equality in the conclusion.
+- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
Iris
----
- `iPvsIntro` : introduction of a primitive view shift. Generates a goal if
the masks are not syntactically equal.
-- `iPvs trm as (x1 ... xn) "ipat"` : runs a primitive view shift `trm`.
+- `iPvs pm_trm as (x1 ... xn) "ipat"` : runs a primitive view shift `pm_trm`.
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iInv> N as (x1 ... xn) "ipat"` : open the invariant `N` and establish that
it is timeless so no laters have to be added.
@@ -186,7 +194,7 @@ Many of the proof mode tactics (such as `iDestruct`, `iApply`, `iRewrite`) can
take both hypotheses and lemmas, and allow one to instantiate universal
quantifiers and implications/wands of these hypotheses/lemmas on the fly.
-The syntax for the arguments, called _proof mode terms_, of these tactics is:
+The syntax for the arguments of these tactics, called _proof mode terms_, is:
(H $! t1 ... tn with "spat1 .. spatn")
diff --git a/_CoqProject b/_CoqProject
index 473926602eadb226fce69a2b79883589ea58f292..c2e66758e9d4ff54a1fddf3d1c4b7307d1e86254 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -122,3 +122,4 @@ proofmode/weakestpre.v
proofmode/ghost_ownership.v
proofmode/sts.v
proofmode/classes.v
+proofmode/class_instances.v
diff --git a/algebra/auth.v b/algebra/auth.v
index d9fa09e152742fe889072b811e75fc6ffa7f44da..301268fbddbbc9dc9c2ee456528ddd87598f0d5b 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -191,11 +191,17 @@ Proof.
exists bf2. rewrite -assoc.
apply (Hab' _ (Some _)); auto. by rewrite /= assoc.
Qed.
+
Lemma auth_update_no_frame a b : a ~l~> b @ Some ∅ → ◠a ⋅ ◯ a ~~> ◠b ⋅ ◯ b.
Proof.
intros. rewrite -{1}(right_id _ _ a) -{1}(right_id _ _ b).
by apply auth_update.
Qed.
+Lemma auth_update_no_frag af b : ∅ ~l~> b @ Some af → ◠af ~~> ◠(b ⋅ af) ⋅ ◯ b.
+Proof.
+ intros. rewrite -{1}(left_id _ _ af) -{1}(right_id _ _ (â— _)).
+ by apply auth_update.
+Qed.
End cmra.
Arguments authR : clear implicits.
diff --git a/algebra/gset.v b/algebra/gset.v
index c60bd02cd2eb8cd673f0a4ef89341ecfc098ddd9..3ae61b0fd28e13e7f9400e3c1ae7443445112a99 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -57,24 +57,47 @@ Section gset.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Arguments op _ _ _ _ : simpl never.
- Lemma gset_alloc_updateP_strong (Q : gset_disj K → Prop) (I : gset K) X :
- (∀ i, i ∉ X → i ∉ I → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+ Lemma gset_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
+ (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
+ (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
Proof.
- intros HQ; apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
- destruct (exist_fresh (X ∪ Y ∪ I)) as [i ?].
+ intros Hfresh HQ.
+ apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
+ destruct (Hfresh (X ∪ Y)) as (i&?&?); first set_solver.
exists (GSet ({[ i ]} ∪ X)); split.
- apply HQ; set_solver by eauto.
- apply gset_disj_valid_op. set_solver by eauto.
Qed.
Lemma gset_alloc_updateP (Q : gset_disj K → Prop) X :
(∀ i, i ∉ X → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
- Proof. move=>??. eapply gset_alloc_updateP_strong with (I:=∅); by eauto. Qed.
- Lemma gset_alloc_updateP_strong' (I : gset K) X :
- GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
+ Proof.
+ intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
+ intros Y ?; exists (fresh Y); eauto using is_fresh.
+ Qed.
+ Lemma gset_alloc_updateP_strong' P X :
+ (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
+ GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X ∧ P i.
Proof. eauto using gset_alloc_updateP_strong. Qed.
Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, ∃ i, Y = GSet ({[ i ]} ∪ X) ∧ i ∉ X.
Proof. eauto using gset_alloc_updateP. Qed.
+ Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K → Prop) :
+ (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
+ (∀ i, P i → Q (GSet {[i]})) → GSet ∅ ~~>: Q.
+ Proof.
+ intros. apply (gset_alloc_updateP_strong P); eauto.
+ intros i; rewrite right_id_L; auto.
+ Qed.
+ Lemma gset_alloc_empty_updateP (Q : gset_disj K → Prop) :
+ (∀ i, Q (GSet {[i]})) → GSet ∅ ~~>: Q.
+ Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
+ Lemma gset_alloc_empty_updateP_strong' P :
+ (∀ Y : gset K, ∃ j, j ∉ Y ∧ P j) →
+ GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]} ∧ P i.
+ Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
+ Lemma gset_alloc_empty_updateP' : GSet ∅ ~~>: λ Y, ∃ i, Y = GSet {[ i ]}.
+ Proof. eauto using gset_alloc_empty_updateP. Qed.
+
Lemma gset_alloc_local_update X i Xf :
i ∉ X → i ∉ Xf → GSet X ~l~> GSet ({[i]} ∪ X) @ Some (GSet Xf).
Proof.
@@ -83,6 +106,12 @@ Section gset.
- intros mZ ?%gset_disj_valid_op HXf.
rewrite -gset_disj_union -?assoc ?HXf ?cmra_opM_assoc; set_solver.
Qed.
+ Lemma gset_alloc_empty_local_update i Xf :
+ i ∉ Xf → GSet ∅ ~l~> GSet {[i]} @ Some (GSet Xf).
+ Proof.
+ intros. rewrite -(right_id_L _ _ {[i]}).
+ apply gset_alloc_local_update; set_solver.
+ Qed.
End gset.
Arguments gset_disjR _ {_ _}.
diff --git a/docs/algebra.tex b/docs/algebra.tex
index c22f0baa7a314ce5dd47baf87a313cb3484f29a8..a970524c14c9d56940cf3b69c2550386d0851549 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -211,7 +211,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\end{defn}
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
-
+\ralf{Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.}
%%% Local Variables:
%%% mode: latex
diff --git a/docs/constructions.tex b/docs/constructions.tex
index cf4114d7b525dea873d4bb0b180db09f46df1f42..40571188f68a0ca7b4ec90de8acce72c8bd96b63 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -3,7 +3,7 @@
\subsection{Next (type-level later)}
-Given a COFE $\cofe$, we define $\latert\cofe$ as follows:
+Given a COFE $\cofe$, we define $\latert\cofe$ as follows (using a datatype-like notation to define the type):
\begin{align*}
\latert\cofe \eqdef{}& \latertinj(x:\cofe) \\
\latertinj(x) \nequiv{n} \latertinj(y) \eqdef{}& n = 0 \lor x \nequiv{n-1} y
@@ -62,7 +62,7 @@ Frame-preserving updates on the $M_i$ lift to the product:
\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:
+The \emph{sum CMRA} $\monoid_1 \csumm \monoid_2$ for any CMRAs $\monoid_1$ and $\monoid_2$ is defined as (again, we use a datatype-like notation):
\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}
@@ -104,36 +104,35 @@ We obtain the following frame-preserving updates:
{\emptyset \mupd \setComp{[\gname \mapsto \melt]}{\gname \in K}}
\inferH{fpfn-update}
- {\melt \mupd \meltsB}
+ {\melt \mupd_\monoid \meltsB}
{f[i \mapsto \melt] \mupd \setComp{ f[i \mapsto \meltB]}{\meltB \in \meltsB}}
\end{mathpar}
-Remember that $\mval$ is the set of elements of a CMRA that are valid at \emph{all} step-indices.
+Above, $\mval$ refers to the validity of $\monoid$.
$K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
\subsection{Agreement}
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
-\newcommand{\aginjc}{\mathrm{c}} % the "c" field of an agreement element
-\newcommand{\aginjV}{\mathrm{V}} % the "V" field of an agreement element
\begin{align*}
- \agm(\cofe) \eqdef{}& \record{\aginjc : \mathbb{N} \to \cofe , \aginjV : \SProp} \\
- & \text{quotiented by} \\
- \melt \equiv \meltB \eqdef{}& \melt.\aginjV = \meltB.\aginjV \land \All n. n \in \melt.\aginjV \Ra \melt.\aginjc(n) \nequiv{n} \meltB.\aginjc(n) \\
- \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.\aginjV \Lra m \in \meltB.\aginjV) \land (\All m \leq n. m \in \melt.\aginjV \Ra \melt.\aginjc(m) \nequiv{m} \meltB.\aginjc(m)) \\
- \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.\aginjV \land \All m \leq n. \melt.\aginjc(n) \nequiv{m} \melt.\aginjc(m) } \\
+ \agm(\cofe) \eqdef{}& \set{(c, V) \in (\mathbb{N} \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
+ \textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land
+ \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n) \\
+% \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
+ \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
+ \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
\mcore\melt \eqdef{}& \melt \\
- \melt \mtimes \meltB \eqdef{}& (\melt.\aginjc, \setComp{n}{n \in \melt.\aginjV \land n \in \meltB.\aginjV \land \melt \nequiv{n} \meltB })
+ \melt \mtimes \meltB \eqdef{}& \left(\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V \land \melt \nequiv{n} \meltB }\right)
\end{align*}
-Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $\aginjc$ and $\aginjV$.
+%Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
$\agm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
-You can think of the $\aginjc$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in \aginjV$ steps.
+You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
-However, given such a chain, we cannot constructively define its limit: Clearly, the $\aginjV$ of the limit is the limit of the $\aginjV$ of the chain.
+However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
But what to pick for the actual data, for the element of $\cofe$?
-Only if $\aginjV = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $\aginjV$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin \aginjV$.
+Only if $V = \mathbb{N}$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
@@ -160,12 +159,12 @@ All cases of composition go to $\bot$.
\mcore{\exinj(x)} \eqdef{}& \mnocore &
\mcore{\bot} \eqdef{}& \bot
\end{align*}
+Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
+
The step-indexed equivalence is inductively defined as follows:
\begin{mathpar}
\infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
- \axiom{\munit \nequiv{n} \munit}
-
\axiom{\bot \nequiv{n} \bot}
\end{mathpar}
$\exm(-)$ is a locally non-expansive functor from $\COFEs$ to $\CMRAs$.
diff --git a/docs/derived.tex b/docs/derived.tex
index 8fa3c08cdc3127bcf5ba551db4bcdd4e762f1d4f..34471d0804706e0c67c8d15e08368f9c957567a5 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -221,9 +221,9 @@ We can derive some specialized forms of the lifting axioms for the operational s
\begin{mathparpagebreakable}
\infer[wp-lift-atomic-step]
{\atomic(\expr_1) \and
- \red(\expr_1, \state_1) \and
- \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)}
- {\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. \pred(\ofval(\val), \state_2, \expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+ \red(\expr_1, \state_1)}
+ { {\begin{inbox}~~\later\ownPhys{\state_1} * \later\All \val_2, \state_2, \expr_\f. (\expr_1,\state_1 \step \ofval(\val),\state_2,\expr_\f) \land \ownPhys{\state_2} \wand \prop[\val_2/\var] * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\ \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
+ \end{inbox}} }
\infer[wp-lift-atomic-det-step]
{\atomic(\expr_1) \and
@@ -238,50 +238,12 @@ We can derive some specialized forms of the lifting axioms for the operational s
{\later ( \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE}) \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\end{mathparpagebreakable}
-Furthermore, we derive some forms that directly involve view shifts and Hoare triples.
-\begin{mathparpagebreakable}
- \infer[ht-lift-step]
- {\mask_2 \subseteq \mask_1 \and
- \toval(\expr_1) = \bot \and
- \red(\expr_1, \state_1) \and
- \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\
- \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
- \All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) * \ownPhys{\state_2} * \prop' \vs[\mask_2][\mask_1] \propB_1 * \propB_2 \\\\
- \All \expr_2, \state_2, \expr_\f. \hoare{\propB_1}{\expr_2}{\Ret\val.\propC}[\mask_1] \and
- \All \expr_2, \state_2, \expr_\f. \hoare{\propB_2}{\expr_\f}{\Ret\any. \TRUE}[\top]}
- { \hoare\prop{\expr_1}{\Ret\val.\propC}[\mask_1] }
-
- \infer[ht-lift-atomic-step]
- {\atomic(\expr_1) \and
- \red(\expr_1, \state_1) \and
- \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f) \\\\
- \prop \vs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\prop' \and
- \All \expr_2, \state_2, \expr_\f. \hoare{\pred(\expr_2,\state_2,\expr_\f) * \prop}{\expr_\f}{\Ret\any. \TRUE}[\top]}
- { \hoare{\later\ownPhys{\state_1} * \later\prop}{\expr_1}{\Ret\val.\Exists \state_2, \expr_\f. \ownPhys{\state_2} * \pred(\ofval(\expr_2),\state_2,\expr_\f)}[\mask_1] }
-
- \infer[ht-lift-pure-step]
- {\toval(\expr_1) = \bot \and
- \All\state_1. \red(\expr_1, \state_1) \and
- \All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_\f) \\\\
- \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
- \All \expr_2, \expr_\f. \hoare{\pred(\expr_2,\expr_\f) * \prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
- { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
-
- \infer[ht-lift-pure-det-step]
- {\toval(\expr_1) = \bot \and
- \All\state_1. \red(\expr_1, \state_1) \and
- \All \state_1, \expr_2', \state_2, \expr_\f'. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \expr_2 = \expr_2' \land \expr_\f = \expr_\f' \\\\
- \hoare{\prop}{\expr_2}{\Ret\val.\propB}[\mask_1] \and
- \hoare{\prop'}{\expr_\f}{\Ret\any. \TRUE}[\top]}
- { \hoare{\later(\prop*\prop')}{\expr_1}{\Ret\val.\propB}[\mask_1] }
-\end{mathparpagebreakable}
-
\subsection{Global functor and ghost ownership}
-Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(F_i)_{i \in I}$ for some finite $I$ by picking
-\[ F(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn F_i(\cofe) \]
+Hereinafter we assume the global CMRA functor (served up as a parameter to Iris) is obtained from a family of functors $(\iFunc_i)_{i \in I}$ for some finite $I$ by picking
+\[ \iFunc(\cofe) \eqdef \prod_{i \in I} \textlog{GhName} \fpfn \iFunc_i(\cofe) \]
We don't care so much about what concretely $\textlog{GhName}$ is, as long as it is countable and infinite.
-With $M_i \eqdef F_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$.
+With $M_i \eqdef \iFunc_i(\iProp)$, we write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$.
In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the ``ghost location'' $\gname$ is allocated and we own piece $\melt$.
From~\ruleref{pvs-update}, \ruleref{vs-update} and the frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfnm}, we have the following derived rules.
diff --git a/docs/logic.tex b/docs/logic.tex
index 94b627f16a121040314d985cb3ea23dab7e99a6e..95b5adf17c7876cb32563c729388549e6666e147 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -58,6 +58,7 @@ For any language $\Lang$, we define the corresponding thread-pool semantics.
\clearpage
\section{Logic}
+\label{sec:logic}
To instantiate Iris, you need to define the following parameters:
\begin{itemize}
@@ -134,7 +135,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$.
-%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.
+\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.}
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:
@@ -382,15 +383,17 @@ This is entirely standard.
{\vctx\mid\pfctx \proves \exists \var: \type.\; \prop \\
\vctx,\var : \type\mid\pfctx , \prop \proves \propB}
{\vctx\mid\pfctx \proves \propB}
-\and
-\infer[$\lambda$]
- {}
- {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
-\and
-\infer[$\mu$]
- {}
- {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
+% \and
+% \infer[$\lambda$]
+% {}
+% {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]}
+% \and
+% \infer[$\mu$]
+% {}
+% {\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$.
+
\paragraph{Laws of (affine) bunched implications.}
\begin{mathpar}
@@ -449,6 +452,7 @@ This is entirely standard.
\later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB
\end{array}
\end{mathpar}
+A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ is derivable for some $\term$.
\begin{mathpar}
\infer
@@ -589,18 +593,16 @@ This is entirely standard.
\begin{mathpar}
\infer[wp-lift-step]
{\mask_2 \subseteq \mask_1 \and
- \toval(\expr_1) = \bot \and
- \red(\expr_1, \state_1) \and
- \All \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \pred(\expr_2,\state_2,\expr_\f)}
+ \toval(\expr_1) = \bot}
{ {\begin{inbox} % for some crazy reason, LaTeX is actually sensitive to the space between the "{ {" here and the "} }" below...
- ~~\pvs[\mask_1][\mask_2] \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. \pred(\expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
+ ~~\pvs[\mask_1][\mask_2] \Exists \state_1. \red(\expr_1,\state_1) \land \later\ownPhys{\state_1} * \later\All \expr_2, \state_2, \expr_\f. (\expr_1, \state_1 \step \expr_2, \state_2, \expr_\f) \land {}\\\qquad\qquad\qquad\qquad\qquad \ownPhys{\state_2} \wand \pvs[\mask_2][\mask_1] \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} {}\\\proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}
\end{inbox}} }
\infer[wp-lift-pure-step]
{\toval(\expr_1) = \bot \and
\All \state_1. \red(\expr_1, \state_1) \and
- \All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 \land \pred(\expr_2,\expr_\f)}
- {\later\All \expr_2, \expr_\f. \pred(\expr_2, \expr_\f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
+ \All \state_1, \expr_2, \state_2, \expr_\f. \expr_1,\state_1 \step \expr_2,\state_2,\expr_\f \Ra \state_1 = \state_2 }
+ {\later\All \state, \expr_2, \expr_\f. (\expr_1,\state \step \expr_2, \state,\expr_\f) \Ra \wpre{\expr_2}[\mask_1]{\Ret\var.\prop} * \wpre{\expr_\f}[\top]{\Ret\any.\TRUE} \proves \wpre{\expr_1}[\mask_1]{\Ret\var.\prop}}
\end{mathpar}
Here we define $\wpre{\expr_\f}[\mask]{\Ret\var.\prop} \eqdef \TRUE$ if $\expr_\f = \bot$ (remember that our stepping relation can, but does not have to, define a forked-off expression).
diff --git a/docs/model.tex b/docs/model.tex
index f6ce778183b83d9714185250e1a298940cf0736e..6f5f765550487e683bfd39835b87019590399e08 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -52,9 +52,11 @@ For every definition, we have to show all the side-conditions: The maps have to
The first complicated task in building a model of full Iris is defining the semantic model of $\Prop$.
We start by defining the functor that assembles the CMRAs we need to the global resource CMRA:
\begin{align*}
- \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \exm(\textdom{State}), \ghostRes: \iFunc(\cofe^\op, \cofe)}
+ \textdom{ResF}(\cofe^\op, \cofe) \eqdef{}& \record{\wld: \mathbb{N} \fpfn \agm(\latert \cofe), \pres: \maybe{\exm(\textdom{State})}, \ghostRes: \iFunc(\cofe^\op, \cofe)}
\end{align*}
-Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$.
+Above, $\maybe\monoid$ is the monoid obtained by adding a unit to $\monoid$.
+(It's not a coincidence that we used the same notation for the range of the core; it's the same type either way: $\monoid + 1$.)
+Remember that $\iFunc$ is the user-chosen bifunctor from $\COFEs$ to $\CMRAs$ (see~\Sref{sec:logic}).
$\textdom{ResF}(\cofe^\op, \cofe)$ is a CMRA by lifting the individual CMRAs pointwise.
Furthermore, if $F$ is locally contractive, then so is $\textdom{ResF}$.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index da060db51554e3dd23928e7676e1ddd7cda84891..5d847b13308bb3e97edbe601ec5492411143640f 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -179,6 +179,7 @@ Definition atomic (e : expr) :=
| Store e1 e2 => bool_decide (is_Some (to_val e1) ∧ is_Some (to_val e2))
| CAS e0 e1 e2 =>
bool_decide (is_Some (to_val e0) ∧ is_Some (to_val e1) ∧ is_Some (to_val e2))
+ | Fork _ => true
(* Make "skip" atomic *)
| App (Rec _ _ (Lit _)) (Lit _) => true
| _ => false
diff --git a/prelude/coPset.v b/prelude/coPset.v
index 9e37b07d05b7479608af74e3588599e5d1ecc0b7..85aec1c9cb567e4cecc8ea2c2d95bc762e69fe3c 100644
--- a/prelude/coPset.v
+++ b/prelude/coPset.v
@@ -315,9 +315,22 @@ Proof.
apply coPset_finite_spec; destruct X as [[t ?]]; apply of_Pset_raw_finite.
Qed.
-(** * Conversion from gsets of positives *)
+(** * Conversion to and from gsets of positives *)
+Lemma to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
+Proof. done. Qed.
+Definition to_gset (X : coPset) : gset positive :=
+ let 'Mapset m := to_Pset X in
+ Mapset (GMap m (bool_decide_pack _ (to_gset_wf m))).
+
Definition of_gset (X : gset positive) : coPset :=
let 'Mapset (GMap (PMap t Ht) _) := X in of_Pset_raw t ↾ of_Pset_wf _ Ht.
+
+Lemma elem_of_to_gset X i : set_finite X → i ∈ to_gset X ↔ i ∈ X.
+Proof.
+ intros ?. rewrite <-elem_of_to_Pset by done.
+ unfold to_gset. by destruct (to_Pset X).
+Qed.
+
Lemma elem_of_of_gset X i : i ∈ of_gset X ↔ i ∈ X.
Proof. destruct X as [[[t ?]]]; apply elem_of_of_Pset_raw. Qed.
Lemma of_gset_finite X : set_finite (of_gset X).
diff --git a/prelude/hlist.v b/prelude/hlist.v
index 8c888c732290a9b90917fe6d68b26ffc56ded8c1..386cc42066800d3ca7986b4521f49102dc2db8a0 100644
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
@@ -1,4 +1,5 @@
From iris.prelude Require Import tactics.
+Local Set Universe Polymorphism.
(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 48403855e61fd192d625c7e54af8377c8c4c33c5..61b832c85008da818b3b3f5722f265cf2c261bc4 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -28,7 +28,6 @@ Class inG (Λ : language) (Σ : gFunctors) (A : cmraT) := InG {
inG_prf : A = projT2 Σ inG_id (iPreProp Λ (globalF Σ))
}.
Arguments inG_id {_ _ _} _.
-Hint Mode inG - - + : typeclass_instances.
Definition to_globalF `{i : inG Λ Σ A} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 4c91e6fa64851b29ef82f4375ece0cdc8747a50d..3c4808b2ffc73c4dba7ad98ad890b59be85e4720 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -43,7 +43,7 @@ Lemma inv_open E N P :
|={E,E'}=> ▷ P ★ (▷ P ={E',E}=★ True).
Proof.
rewrite inv_eq /inv. iDestruct 1 as (i) "[% #Hi]".
- iExists (E ∖ {[ i ]}). iSplit. { iPureIntro. set_solver. }
+ iExists (E ∖ {[ i ]}). iSplit; first (iPureIntro; set_solver).
iPvs (pvs_openI' with "Hi") as "HP"; [set_solver..|].
iPvsIntro. iSplitL "HP"; first done. iIntros "HP".
iPvs (pvs_closeI' _ _ P with "[HP]"); [set_solver|iSplit; done|set_solver|].
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
new file mode 100644
index 0000000000000000000000000000000000000000..08b7d7bab9c1d281d6880439dc22099ee6c5b4d9
--- /dev/null
+++ b/proofmode/class_instances.v
@@ -0,0 +1,314 @@
+From iris.proofmode Require Export classes.
+From iris.algebra Require Import upred_big_op gmap upred_tactics.
+Import uPred.
+
+Section classes.
+Context {M : ucmraT}.
+Implicit Types P Q R : uPred M.
+
+(* FromAssumption *)
+Global Instance from_assumption_exact p P : FromAssumption p P P.
+Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
+Global Instance from_assumption_always_l p P Q :
+ FromAssumption p P Q → FromAssumption p (□ P) Q.
+Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
+Global Instance from_assumption_always_r P Q :
+ FromAssumption true P Q → FromAssumption true P (□ Q).
+Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+Global Instance from_assumption_rvs p P Q :
+ FromAssumption p P Q → FromAssumption p P (|=r=> Q)%I.
+Proof. rewrite /FromAssumption=>->. apply rvs_intro. Qed.
+
+(* IntoPure *)
+Global Instance into_pure_pure φ : @IntoPure M (■φ) φ.
+Proof. done. Qed.
+Global Instance into_pure_eq {A : cofeT} (a b : A) :
+ Timeless a → @IntoPure M (a ≡ b) (a ≡ b).
+Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
+Global Instance into_pure_valid `{CMRADiscrete A} (a : A) : @IntoPure M (✓ a) (✓ a).
+Proof. by rewrite /IntoPure discrete_valid. Qed.
+
+(* FromPure *)
+Global Instance from_pure_pure φ : @FromPure M (■φ) φ.
+Proof. intros ?. by apply pure_intro. Qed.
+Global Instance from_pure_eq {A : cofeT} (a b : A) : @FromPure M (a ≡ b) (a ≡ b).
+Proof. intros ->. apply eq_refl. Qed.
+Global Instance from_pure_valid {A : cmraT} (a : A) : @FromPure M (✓ a) (✓ a).
+Proof. intros ?. by apply valid_intro. Qed.
+Global Instance from_pure_rvs P φ : FromPure P φ → FromPure (|=r=> P) φ.
+Proof. intros ??. by rewrite -rvs_intro (from_pure P). Qed.
+
+(* IntoPersistentP *)
+Global Instance into_persistentP_always_trans P Q :
+ IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
+Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
+Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
+Proof. done. Qed.
+Global Instance into_persistentP_persistent P :
+ PersistentP P → IntoPersistentP P P | 100.
+Proof. done. Qed.
+
+(* IntoLater *)
+Global Instance into_later_default P : IntoLater P P | 1000.
+Proof. apply later_intro. Qed.
+Global Instance into_later_later P : IntoLater (â–· P) P.
+Proof. done. Qed.
+Global Instance into_later_and P1 P2 Q1 Q2 :
+ IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
+Global Instance into_later_or P1 P2 Q1 Q2 :
+ IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
+Global Instance into_later_sep P1 P2 Q1 Q2 :
+ IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ★ P2) (Q1 ★ Q2).
+Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+
+Global Instance into_later_big_sepM `{Countable K} {A}
+ (Φ Ψ : K → A → uPred M) (m : gmap K A) :
+ (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
+ IntoLater ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x).
+Proof.
+ rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
+Qed.
+Global Instance into_later_big_sepS `{Countable A}
+ (Φ Ψ : A → uPred M) (X : gset A) :
+ (∀ x, IntoLater (Φ x) (Ψ x)) →
+ IntoLater ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x).
+Proof.
+ rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
+Qed.
+
+(* FromLater *)
+Global Instance from_later_later P : FromLater (â–· P) P.
+Proof. done. Qed.
+Global Instance from_later_and P1 P2 Q1 Q2 :
+ FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
+Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
+Global Instance from_later_or P1 P2 Q1 Q2 :
+ FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
+Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
+Global Instance from_later_sep P1 P2 Q1 Q2 :
+ FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ★ P2) (Q1 ★ Q2).
+Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
+
+(* IntoWand *)
+Global Instance into_wand_wand P Q : IntoWand (P -★ Q) P Q.
+Proof. done. Qed.
+Global Instance into_wand_impl P Q : IntoWand (P → Q) P Q.
+Proof. apply impl_wand. Qed.
+Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
+Proof. by apply and_elim_l', impl_wand. Qed.
+Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
+Proof. apply and_elim_r', impl_wand. Qed.
+Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
+Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
+Global Instance into_wand_rvs R P Q :
+ IntoWand R P Q → IntoWand R (|=r=> P) (|=r=> Q) | 100.
+Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite rvs_wand_r. Qed.
+
+(* FromAnd *)
+Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
+Proof. done. Qed.
+Global Instance from_and_sep_persistent_l P1 P2 :
+ PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
+Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
+Global Instance from_and_sep_persistent_r P1 P2 :
+ PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
+Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
+Global Instance from_and_always P Q1 Q2 :
+ FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
+Global Instance from_and_later P Q1 Q2 :
+ FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
+
+(* FromSep *)
+Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
+Proof. done. Qed.
+Global Instance from_sep_always P Q1 Q2 :
+ FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
+Global Instance from_sep_later P Q1 Q2 :
+ FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
+Global Instance from_sep_rvs P Q1 Q2 :
+ FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
+Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
+
+Global Instance from_sep_ownM (a b : M) :
+ FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
+Proof. by rewrite /FromSep ownM_op. Qed.
+Global Instance from_sep_big_sepM
+ `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
+ (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+ FromSep ([★ map] k ↦ x ∈ m, Φ k x)
+ ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+ rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
+Qed.
+Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
+ (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
+ FromSep ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+ rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
+Qed.
+
+(* IntoOp *)
+Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
+Proof. by rewrite /IntoOp. Qed.
+Global Instance into_op_persistent {A : cmraT} (a : A) :
+ Persistent a → IntoOp a a a.
+Proof. intros; apply (persistent_dup a). Qed.
+Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
+ IntoOp a b1 b2 → IntoOp a' b1' b2' →
+ IntoOp (a,a') (b1,b1') (b2,b2').
+Proof. by constructor. Qed.
+Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
+ IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
+Proof. by constructor. Qed.
+
+(* IntoSep *)
+Global Instance into_sep_sep p P Q : IntoSep p (P ★ Q) P Q.
+Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
+Global Instance into_sep_ownM p (a b1 b2 : M) :
+ IntoOp a b1 b2 →
+ IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+Proof.
+ rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
+Qed.
+
+Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
+Proof. by rewrite /IntoSep /= always_and_sep. Qed.
+Global Instance into_sep_and_persistent_l P Q :
+ PersistentP P → IntoSep false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
+Global Instance into_sep_and_persistent_r P Q :
+ PersistentP Q → IntoSep false (P ∧ Q) P Q.
+Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
+
+Global Instance into_sep_later p P Q1 Q2 :
+ IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
+Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
+
+Global Instance into_sep_big_sepM
+ `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
+ (∀ k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
+ IntoSep p ([★ map] k ↦ x ∈ m, Φ k x)
+ ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
+Proof.
+ rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
+ by apply big_sepM_mono.
+Qed.
+Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
+ (∀ x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) →
+ IntoSep p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
+Proof.
+ rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
+ by apply big_sepS_mono.
+Qed.
+
+(* Frame *)
+Global Instance frame_here R : Frame R R True.
+Proof. by rewrite /Frame right_id. Qed.
+
+Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ.
+Global Instance make_sep_true_l P : MakeSep True P P.
+Proof. by rewrite /MakeSep left_id. Qed.
+Global Instance make_sep_true_r P : MakeSep P True P.
+Proof. by rewrite /MakeSep right_id. Qed.
+Global Instance make_sep_default P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_sep_l R P1 P2 Q Q' :
+ Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
+Global Instance frame_sep_r R P1 P2 Q Q' :
+ Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
+Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
+
+Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
+Global Instance make_and_true_l P : MakeAnd True P P.
+Proof. by rewrite /MakeAnd left_id. Qed.
+Global Instance make_and_true_r P : MakeAnd P True P.
+Proof. by rewrite /MakeAnd right_id. Qed.
+Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_and_l R P1 P2 Q Q' :
+ Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+Global Instance frame_and_r R P1 P2 Q Q' :
+ Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
+Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
+
+Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
+Global Instance make_or_true_l P : MakeOr True P True.
+Proof. by rewrite /MakeOr left_absorb. Qed.
+Global Instance make_or_true_r P : MakeOr P True True.
+Proof. by rewrite /MakeOr right_absorb. Qed.
+Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
+Proof. done. Qed.
+Global Instance frame_or R P1 P2 Q1 Q2 Q :
+ Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
+Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
+
+Global Instance frame_wand R P1 P2 Q2 :
+ Frame R P2 Q2 → Frame R (P1 -★ P2) (P1 -★ Q2).
+Proof.
+ rewrite /Frame=> ?. apply wand_intro_l.
+ by rewrite assoc (comm _ P1) -assoc wand_elim_r.
+Qed.
+
+Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
+Global Instance make_later_true : MakeLater True True.
+Proof. by rewrite /MakeLater later_True. Qed.
+Global Instance make_later_default P : MakeLater P (â–· P) | 100.
+Proof. done. Qed.
+
+Global Instance frame_later R P Q Q' :
+ Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
+Proof.
+ rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
+Qed.
+
+Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
+ (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
+Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
+ (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
+Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
+
+Global Instance frame_rvs R P Q : Frame R P Q → Frame R (|=r=> P) (|=r=> Q).
+Proof. rewrite /Frame=><-. by rewrite rvs_frame_l. Qed.
+
+(* FromOr *)
+Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
+Proof. done. Qed.
+Global Instance from_or_rvs P Q1 Q2 :
+ FromOr P Q1 Q2 → FromOr (|=r=> P) (|=r=> Q1) (|=r=> Q2).
+Proof. rewrite /FromOr=><-. apply or_elim; apply rvs_mono; auto with I. Qed.
+
+(* IntoOr *)
+Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
+Proof. done. Qed.
+Global Instance into_or_later P Q1 Q2 :
+ IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
+Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
+
+(* FromExist *)
+Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
+Proof. done. Qed.
+Global Instance from_exist_rvs {A} P (Φ : A → uPred M) :
+ FromExist P Φ → FromExist (|=r=> P) (λ a, |=r=> Φ a)%I.
+Proof.
+ rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
+Qed.
+
+(* IntoExist *)
+Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.
+Proof. done. Qed.
+Global Instance into_exist_later {A} P (Φ : A → uPred M) :
+ IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
+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.
+End classes.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index e9fe31f4dda5caf8f4241cb5034feccbd831e657..0c0a1cc283ed7d546b38528f35bf2385fd53130e 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -1,5 +1,4 @@
From iris.algebra Require Export upred.
-From iris.algebra Require Import upred_big_op gmap upred_tactics.
Import uPred.
Section classes.
@@ -8,337 +7,55 @@ Implicit Types P Q : uPred M.
Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : □?p P ⊢ Q.
Global Arguments from_assumption _ _ _ {_}.
-Global Instance from_assumption_exact p P : FromAssumption p P P.
-Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
-Global Instance from_assumption_always_l p P Q :
- FromAssumption p P Q → FromAssumption p (□ P) Q.
-Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
-Global Instance from_assumption_always_r P Q :
- FromAssumption true P Q → FromAssumption true P (□ Q).
-Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
-Global Instance from_assumption_rvs p P Q :
- FromAssumption p P Q → FromAssumption p P (|=r=> Q)%I.
-Proof. rewrite /FromAssumption=>->. apply rvs_intro. Qed.
Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P ⊢ ■φ.
Global Arguments into_pure : clear implicits.
-Global Instance into_pure_pure φ : IntoPure (■φ) φ.
-Proof. done. Qed.
-Global Instance into_pure_eq {A : cofeT} (a b : A) :
- Timeless a → IntoPure (a ≡ b) (a ≡ b).
-Proof. intros. by rewrite /IntoPure timeless_eq. Qed.
-Global Instance into_pure_valid `{CMRADiscrete A} (a : A) : IntoPure (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
Class FromPure (P : uPred M) (φ : Prop) := from_pure : φ → True ⊢ P.
Global Arguments from_pure : clear implicits.
-Global Instance from_pure_pure φ : FromPure (■φ) φ.
-Proof. intros ?. by apply pure_intro. Qed.
-Global Instance from_pure_eq {A : cofeT} (a b : A) : FromPure (a ≡ b) (a ≡ b).
-Proof. intros ->. apply eq_refl. Qed.
-Global Instance from_pure_valid {A : cmraT} (a : A) : FromPure (✓ a) (✓ a).
-Proof. intros ?. by apply valid_intro. Qed.
-Global Instance from_pure_rvs P φ : FromPure P φ → FromPure (|=r=> P) φ.
-Proof. intros ??. by rewrite -rvs_intro (from_pure P). Qed.
Class IntoPersistentP (P Q : uPred M) := into_persistentP : P ⊢ □ Q.
Global Arguments into_persistentP : clear implicits.
-Global Instance into_persistentP_always_trans P Q :
- IntoPersistentP P Q → IntoPersistentP (□ P) Q | 0.
-Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
-Global Instance into_persistentP_always P : IntoPersistentP (â–¡ P) P | 1.
-Proof. done. Qed.
-Global Instance into_persistentP_persistent P :
- PersistentP P → IntoPersistentP P P | 100.
-Proof. done. Qed.
Class IntoLater (P Q : uPred M) := into_later : P ⊢ ▷ Q.
Global Arguments into_later _ _ {_}.
+
Class FromLater (P Q : uPred M) := from_later : ▷ Q ⊢ P.
Global Arguments from_later _ _ {_}.
-Global Instance into_later_default P : IntoLater P P | 1000.
-Proof. apply later_intro. Qed.
-Global Instance into_later_later P : IntoLater (â–· P) P.
-Proof. done. Qed.
-Global Instance into_later_and P1 P2 Q1 Q2 :
- IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance into_later_or P1 P2 Q1 Q2 :
- IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance into_later_sep P1 P2 Q1 Q2 :
- IntoLater P1 Q1 → IntoLater P2 Q2 → IntoLater (P1 ★ P2) (Q1 ★ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
-Global Instance into_later_big_sepM `{Countable K} {A}
- (Φ Ψ : K → A → uPred M) (m : gmap K A) :
- (∀ x k, IntoLater (Φ k x) (Ψ k x)) →
- IntoLater ([★ map] k ↦ x ∈ m, Φ k x) ([★ map] k ↦ x ∈ m, Ψ k x).
-Proof.
- rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
-Qed.
-Global Instance into_later_big_sepS `{Countable A}
- (Φ Ψ : A → uPred M) (X : gset A) :
- (∀ x, IntoLater (Φ x) (Ψ x)) →
- IntoLater ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ x).
-Proof.
- rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
-Qed.
-
-Global Instance from_later_later P : FromLater (â–· P) P.
-Proof. done. Qed.
-Global Instance from_later_and P1 P2 Q1 Q2 :
- FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∧ P2) (Q1 ∧ Q2).
-Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
-Global Instance from_later_or P1 P2 Q1 Q2 :
- FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ∨ P2) (Q1 ∨ Q2).
-Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
-Global Instance from_later_sep P1 P2 Q1 Q2 :
- FromLater P1 Q1 → FromLater P2 Q2 → FromLater (P1 ★ P2) (Q1 ★ Q2).
-Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
-
Class IntoWand (R P Q : uPred M) := into_wand : R ⊢ P -★ Q.
Global Arguments into_wand : clear implicits.
-Global Instance into_wand_wand P Q : IntoWand (P -★ Q) P Q.
-Proof. done. Qed.
-Global Instance into_wand_impl P Q : IntoWand (P → Q) P Q.
-Proof. apply impl_wand. Qed.
-Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
-Proof. by apply and_elim_l', impl_wand. Qed.
-Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
-Proof. apply and_elim_r', impl_wand. Qed.
-Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
-Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
-Global Instance into_wand_rvs R P Q :
- IntoWand R P Q → IntoWand R (|=r=> P) (|=r=> Q) | 100.
-Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite rvs_wand_r. Qed.
Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
Global Arguments from_and : clear implicits.
-Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
-Proof. done. Qed.
-Global Instance from_and_sep_persistent_l P1 P2 :
- PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
-Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
-Global Instance from_and_sep_persistent_r P1 P2 :
- PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
-Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
-Global Instance from_and_always P Q1 Q2 :
- FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
-Global Instance from_and_later P Q1 Q2 :
- FromAnd P Q1 Q2 → FromAnd (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
-
Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 ★ Q2 ⊢ P.
Global Arguments from_sep : clear implicits.
-Global Instance from_sep_sep P1 P2 : FromSep (P1 ★ P2) P1 P2 | 100.
-Proof. done. Qed.
-Global Instance from_sep_always P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (□ P) (□ Q1) (□ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
-Global Instance from_sep_later P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
-Global Instance from_sep_rvs P Q1 Q2 :
- FromSep P Q1 Q2 → FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
-Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
-
-Global Instance from_sep_ownM (a b : M) :
- FromSep (uPred_ownM (a â‹… b)) (uPred_ownM a) (uPred_ownM b) | 99.
-Proof. by rewrite /FromSep ownM_op. Qed.
-Global Instance from_sep_big_sepM
- `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) m :
- (∀ k x, FromSep (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
- FromSep ([★ map] k ↦ x ∈ m, Φ k x)
- ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
- rewrite /FromSep=> ?. rewrite -big_sepM_sepM. by apply big_sepM_mono.
-Qed.
-Global Instance from_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) X :
- (∀ x, FromSep (Φ x) (Ψ1 x) (Ψ2 x)) →
- FromSep ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
-Proof.
- rewrite /FromSep=> ?. rewrite -big_sepS_sepS. by apply big_sepS_mono.
-Qed.
-
Class IntoSep (p: bool) (P Q1 Q2 : uPred M) := into_sep : □?p P ⊢ □?p (Q1 ★ Q2).
Global Arguments into_sep : clear implicits.
+
Class IntoOp {A : cmraT} (a b1 b2 : A) := into_op : a ≡ b1 ⋅ b2.
Global Arguments into_op {_} _ _ _ {_}.
-Global Instance into_op_op {A : cmraT} (a b : A) : IntoOp (a â‹… b) a b.
-Proof. by rewrite /IntoOp. Qed.
-Global Instance into_op_persistent {A : cmraT} (a : A) :
- Persistent a → IntoOp a a a.
-Proof. intros; apply (persistent_dup a). Qed.
-Global Instance into_op_pair {A B : cmraT} (a b1 b2 : A) (a' b1' b2' : B) :
- IntoOp a b1 b2 → IntoOp a' b1' b2' →
- IntoOp (a,a') (b1,b1') (b2,b2').
-Proof. by constructor. Qed.
-Global Instance into_op_Some {A : cmraT} (a : A) b1 b2 :
- IntoOp a b1 b2 → IntoOp (Some a) (Some b1) (Some b2).
-Proof. by constructor. Qed.
-
-Global Instance into_sep_sep p P Q : IntoSep p (P ★ Q) P Q.
-Proof. rewrite /IntoSep. by rewrite always_if_sep. Qed.
-Global Instance into_sep_ownM p (a b1 b2 : M) :
- IntoOp a b1 b2 →
- IntoSep p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
- rewrite /IntoOp /IntoSep=> ->. by rewrite ownM_op always_if_sep.
-Qed.
-
-Global Instance into_sep_and P Q : IntoSep true (P ∧ Q) P Q.
-Proof. by rewrite /IntoSep /= always_and_sep. Qed.
-Global Instance into_sep_and_persistent_l P Q :
- PersistentP P → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_l. Qed.
-Global Instance into_sep_and_persistent_r P Q :
- PersistentP Q → IntoSep false (P ∧ Q) P Q.
-Proof. intros; by rewrite /IntoSep /= always_and_sep_r. Qed.
-
-Global Instance into_sep_later p P Q1 Q2 :
- IntoSep p P Q1 Q2 → IntoSep p (▷ P) (▷ Q1) (▷ Q2).
-Proof. by rewrite /IntoSep -later_sep !always_if_later=> ->. Qed.
-
-Global Instance into_sep_big_sepM
- `{Countable K} {A} (Φ Ψ1 Ψ2 : K → A → uPred M) p m :
- (∀ k x, IntoSep p (Φ k x) (Ψ1 k x) (Ψ2 k x)) →
- IntoSep p ([★ map] k ↦ x ∈ m, Φ k x)
- ([★ map] k ↦ x ∈ m, Ψ1 k x) ([★ map] k ↦ x ∈ m, Ψ2 k x).
-Proof.
- rewrite /IntoSep=> ?. rewrite -big_sepM_sepM !big_sepM_always_if.
- by apply big_sepM_mono.
-Qed.
-Global Instance into_sep_big_sepS `{Countable A} (Φ Ψ1 Ψ2 : A → uPred M) p X :
- (∀ x, IntoSep p (Φ x) (Ψ1 x) (Ψ2 x)) →
- IntoSep p ([★ set] x ∈ X, Φ x) ([★ set] x ∈ X, Ψ1 x) ([★ set] x ∈ X, Ψ2 x).
-Proof.
- rewrite /IntoSep=> ?. rewrite -big_sepS_sepS !big_sepS_always_if.
- by apply big_sepS_mono.
-Qed.
-
Class Frame (R P Q : uPred M) := frame : R ★ Q ⊢ P.
Global Arguments frame : clear implicits.
-Global Instance frame_here R : Frame R R True.
-Proof. by rewrite /Frame right_id. Qed.
-
-Class MakeSep (P Q PQ : uPred M) := make_sep : P ★ Q ⊣⊢ PQ.
-Global Instance make_sep_true_l P : MakeSep True P P.
-Proof. by rewrite /MakeSep left_id. Qed.
-Global Instance make_sep_true_r P : MakeSep P True P.
-Proof. by rewrite /MakeSep right_id. Qed.
-Global Instance make_sep_default P Q : MakeSep P Q (P ★ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_sep_l R P1 P2 Q Q' :
- Frame R P1 Q → MakeSep Q P2 Q' → Frame R (P1 ★ P2) Q' | 9.
-Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
-Global Instance frame_sep_r R P1 P2 Q Q' :
- Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
-Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
-
-Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
-Global Instance make_and_true_l P : MakeAnd True P P.
-Proof. by rewrite /MakeAnd left_id. Qed.
-Global Instance make_and_true_r P : MakeAnd P True P.
-Proof. by rewrite /MakeAnd right_id. Qed.
-Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_and_l R P1 P2 Q Q' :
- Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-Global Instance frame_and_r R P1 P2 Q Q' :
- Frame R P2 Q → MakeAnd P1 Q Q' → Frame R (P1 ∧ P2) Q' | 10.
-Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
-
-Class MakeOr (P Q PQ : uPred M) := make_or : P ∨ Q ⊣⊢ PQ.
-Global Instance make_or_true_l P : MakeOr True P True.
-Proof. by rewrite /MakeOr left_absorb. Qed.
-Global Instance make_or_true_r P : MakeOr P True True.
-Proof. by rewrite /MakeOr right_absorb. Qed.
-Global Instance make_or_default P Q : MakeOr P Q (P ∨ Q) | 100.
-Proof. done. Qed.
-Global Instance frame_or R P1 P2 Q1 Q2 Q :
- Frame R P1 Q1 → Frame R P2 Q2 → MakeOr Q1 Q2 Q → Frame R (P1 ∨ P2) Q.
-Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
-
-Global Instance frame_wand R P1 P2 Q2 :
- Frame R P2 Q2 → Frame R (P1 -★ P2) (P1 -★ Q2).
-Proof.
- rewrite /Frame=> ?. apply wand_intro_l.
- by rewrite assoc (comm _ P1) -assoc wand_elim_r.
-Qed.
-
-Class MakeLater (P lP : uPred M) := make_later : ▷ P ⊣⊢ lP.
-Global Instance make_later_true : MakeLater True True.
-Proof. by rewrite /MakeLater later_True. Qed.
-Global Instance make_later_default P : MakeLater P (â–· P) | 100.
-Proof. done. Qed.
-
-Global Instance frame_later R P Q Q' :
- Frame R P Q → MakeLater Q Q' → Frame R (▷ P) Q'.
-Proof.
- rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
-Qed.
-
-Global Instance frame_exist {A} R (Φ Ψ : A → uPred M) :
- (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∃ x, Φ x) (∃ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
- (∀ a, Frame R (Φ a) (Ψ a)) → Frame R (∀ x, Φ x) (∀ x, Ψ x).
-Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
-
-Global Instance frame_rvs R P Q : Frame R P Q → Frame R (|=r=> P) (|=r=> Q).
-Proof. rewrite /Frame=><-. by rewrite rvs_frame_l. Qed.
-
Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 ∨ Q2 ⊢ P.
Global Arguments from_or : clear implicits.
-Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
-Proof. done. Qed.
-Global Instance from_or_rvs P Q1 Q2 :
- FromOr P Q1 Q2 → FromOr (|=r=> P) (|=r=> Q1) (|=r=> Q2).
-Proof. rewrite /FromOr=><-. apply or_elim; apply rvs_mono; auto with I. Qed.
Class IntoOr P Q1 Q2 := into_or : P ⊢ Q1 ∨ Q2.
Global Arguments into_or : clear implicits.
-Global Instance into_or_or P Q : IntoOr (P ∨ Q) P Q.
-Proof. done. Qed.
-Global Instance into_or_later P Q1 Q2 :
- IntoOr P Q1 Q2 → IntoOr (▷ P) (▷ Q1) (▷ Q2).
-Proof. rewrite /IntoOr=>->. by rewrite later_or. Qed.
Class FromExist {A} (P : uPred M) (Φ : A → uPred M) :=
from_exist : (∃ x, Φ x) ⊢ P.
Global Arguments from_exist {_} _ _ {_}.
-Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
-Proof. done. Qed.
-Global Instance from_exist_rvs {A} P (Φ : A → uPred M) :
- FromExist P Φ → FromExist (|=r=> P) (λ a, |=r=> Φ a)%I.
-Proof.
- rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
-Qed.
Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
into_exist : P ⊢ ∃ x, Φ x.
Global Arguments into_exist {_} _ _ {_}.
-Global Instance into_exist_exist {A} (Φ : A → uPred M) : IntoExist (∃ a, Φ a) Φ.
-Proof. done. Qed.
-Global Instance into_exist_later {A} P (Φ : A → uPred M) :
- IntoExist P Φ → Inhabited A → IntoExist (▷ P) (λ a, ▷ (Φ a))%I.
-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.
-Global Instance timeless_elim_rvs Q : TimelessElim (|=r=> Q).
-Proof.
- intros P ?. by rewrite (rvs_timeless P) rvs_frame_r wand_elim_r rvs_trans.
-Qed.
+Global Arguments timeless_elim _ {_} _ {_}.
End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 7be01a1e5bb141fd604182b37d397d4d99f3323f..ebe55ff1941bce5d701972cd74eb1203ff7612c6 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -1,5 +1,5 @@
From iris.algebra Require Export upred.
-From iris.algebra Require Import upred_big_op upred_tactics gmap.
+From iris.algebra Require Import upred_big_op upred_tactics.
From iris.proofmode Require Export environments classes.
From iris.prelude Require Import stringmap hlist.
Import uPred.
@@ -551,25 +551,13 @@ Proof.
by rewrite right_id {1}(persistentP P) always_and_sep_l wand_elim_r.
Qed.
-(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
-not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
-[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
-make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
-Class IntoPosedProof (P1 P2 R : uPred M) :=
- into_pose_proof : (P1 ⊢ P2) → True ⊢ R.
-Arguments into_pose_proof : clear implicits.
-Instance to_posed_proof_True P : IntoPosedProof True P P.
-Proof. by rewrite /IntoPosedProof. Qed.
-Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P -★ Q).
-Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
-
-Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
- (P1 ⊢ P2) → IntoPosedProof P1 P2 R →
- envs_app true (Esnoc Enil j R) Δ = Some Δ' →
+Lemma tac_pose_proof Δ Δ' j P Q :
+ (True ⊢ P) →
+ envs_app true (Esnoc Enil j P) Δ = Some Δ' →
(Δ' ⊢ Q) → Δ ⊢ Q.
Proof.
- intros HP ?? <-. rewrite envs_app_sound //; simpl.
- by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
+ intros HP ? <-. rewrite envs_app_sound //; simpl.
+ by rewrite right_id -HP always_pure wand_True.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
@@ -747,6 +735,3 @@ Proof.
rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
Qed.
End tactics.
-
-Hint Extern 0 (IntoPosedProof True _ _) =>
- class_apply @to_posed_proof_True : typeclass_instances.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index df3203323e96350820f988dab219d639f553fec6..676710d71fdeaed2ca75e3fd6a3908ec13362a99 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -112,45 +112,45 @@ Tactic Notation "iPvsCore" constr(H) :=
|env_cbv; reflexivity|simpl]
end.
-Tactic Notation "iPvs" open_constr(H) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as "?").
-Tactic Notation "iPvs" open_constr(H) "as" constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1) ")"
+Tactic Notation "iPvs" open_constr(lem) :=
+ iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as "?").
+Tactic Notation "iPvs" open_constr(lem) "as" constr(pat) :=
+ iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- iDestructHelp H as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iPvsCore H; last iDestruct H as ( x1 x2 x3 ) pat).
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iDestructHelp H as (fun H =>
+ iDestructCore lem as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
- iDestructHelp H as (fun H =>
+ iDestructCore lem as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
- iDestructHelp H as (fun H =>
+ iDestructCore lem as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iDestructHelp H as (fun H =>
+ iDestructCore lem as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iPvs" open_constr(H) "as" "(" simple_intropattern(x1)
+Tactic Notation "iPvs" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
- iDestructHelp H as (fun H =>
+ iDestructCore lem as (fun H =>
iPvsCore H; last iDestruct H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
Hint Extern 2 (of_envs _ ⊢ _) =>
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 9e0ededc0ab3dd8805584be5d71867aca70108c6..89b691aa24367ca1803262e6a3dcff55de4f9dd6 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -1,6 +1,7 @@
From iris.proofmode Require Import coq_tactics intro_patterns spec_patterns.
From iris.algebra Require Export upred.
From iris.proofmode Require Export classes notation.
+From iris.proofmode Require Import class_instances.
From iris.prelude Require Import stringmap hlist.
Declare Reduction env_cbv := cbv [
@@ -208,31 +209,62 @@ Tactic Notation "iSpecialize" open_constr(t) :=
end.
(** * Pose proof *)
-Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
- lazymatch type of H1 with
- | string =>
- eapply tac_pose_proof_hyp with _ _ H1 _ H2 _;
- [env_cbv; reflexivity || fail "iPoseProof:" H1 "not found"
- |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
- | _ =>
- eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
- [first [eapply H1|apply uPred.equiv_iff; eapply H1]
- |apply _
- |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
+(* The tactic [iIntoEntails] tactic solves a goal [True ⊢ Q]. The arguments [t]
+is a Coq term whose type is of the following shape:
+
+- [∀ (x_1 : A_1) .. (x_n : A_n), True ⊢ Q]
+- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊢ P2], in which case [Q] becomes [P1 -★ P2]
+- [∀ (x_1 : A_1) .. (x_n : A_n), P1 ⊣⊢ P2], in which case [Q] becomes [P1 ↔ P2]
+
+The tactic instantiates each dependent argument [x_i] with an evar and generates
+a goal [P] for non-dependent arguments [x_i : P]. *)
+Tactic Notation "iIntoEntails" open_constr(t) :=
+ let rec go t :=
+ lazymatch type of t with
+ | True ⊢ _ => apply t
+ | _ ⊢ _ => apply (uPred.entails_wand _ _ t)
+ | _ ⊣⊢ _ => apply (uPred.equiv_iff _ _ t)
+ | ?P → ?Q => let H := fresh in assert P as H; [|go uconstr:(t H)]
+ | ∀ _ : ?T, _ =>
+ (* Put [T] inside an [id] to avoid TC inference from being invoked. *)
+ (* This is a workarround for Coq bug #4969. *)
+ let e := fresh in evar (e:id T);
+ let e' := eval unfold e in e in clear e; go (t e')
+ end
+ in go t.
+
+Tactic Notation "iPoseProofCore" open_constr(lem) "as" tactic(tac) :=
+ let pose_trm t tac :=
+ let Htmp := iFresh in
+ lazymatch type of t with
+ | string =>
+ eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
+ [env_cbv; reflexivity || fail "iPoseProof:" t "not found"
+ |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
+ |tac Htmp]
+ | _ =>
+ eapply tac_pose_proof with _ Htmp _; (* (j:=H) *)
+ [iIntoEntails t
+ |env_cbv; reflexivity || fail "iPoseProof:" Htmp "not fresh"
+ |tac Htmp]
+ end;
+ try (apply _) (* solve TC constraints. It is essential that this happens
+ after the continuation [tac] has been called. *)
+ in lazymatch lem with
+ | ITrm ?t ?xs ?pat =>
+ pose_trm t ltac:(fun Htmp =>
+ iSpecializeArgs Htmp xs; iSpecializePat Htmp pat; last (tac Htmp))
+ | _ => pose_trm lem tac
end.
-Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
- lazymatch t with
- | ITrm ?H1 ?xs ?pat =>
- iPoseProofCore H1 as H; last (iSpecializeArgs H xs; iSpecializePat H pat)
- | _ => iPoseProofCore t as H
- end.
+Tactic Notation "iPoseProof" open_constr(lem) "as" constr(H) :=
+ iPoseProofCore lem as (fun Htmp => iRename Htmp into H).
-Tactic Notation "iPoseProof" open_constr(t) :=
- let H := iFresh in iPoseProof t as H.
+Tactic Notation "iPoseProof" open_constr(lem) :=
+ iPoseProofCore lem as (fun _ => idtac).
(** * Apply *)
-Tactic Notation "iApply" open_constr(t) :=
+Tactic Notation "iApply" open_constr(lem) :=
let finish H := first
[iExact H
|eapply tac_apply with _ H _ _ _;
@@ -240,18 +272,17 @@ Tactic Notation "iApply" open_constr(t) :=
|let P := match goal with |- IntoWand ?P _ _ => P end in
apply _ || fail 1 "iApply: cannot apply" H ":" P
|lazy beta (* reduce betas created by instantiation *)]] in
- let Htmp := iFresh in
- lazymatch t with
- | ITrm ?H ?xs ?pat =>
- iPoseProofCore H as Htmp; last (
+ lazymatch lem with
+ | ITrm ?t ?xs ?pat =>
+ iPoseProofCore t as (fun Htmp =>
iSpecializeArgs Htmp xs;
try (iSpecializeArgs Htmp (hcons _ _));
iSpecializePat Htmp pat; last finish Htmp)
| _ =>
- iPoseProofCore t as Htmp; last (
+ iPoseProofCore lem as (fun Htmp =>
try (iSpecializeArgs Htmp (hcons _ _));
finish Htmp)
- end; try apply _.
+ end.
(** * Revert *)
Local Tactic Notation "iForallRevert" ident(x) :=
@@ -647,7 +678,7 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 ); iIntros p.
(** * Destruct tactic *)
-Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
+Tactic Notation "iDestructCore" open_constr(lem) "as" tactic(tac) :=
let intro_destruct n :=
let rec go n' :=
lazymatch n' with
@@ -663,49 +694,48 @@ Tactic Notation "iDestructHelp" open_constr(lem) "as" tactic(tac) :=
| string => tac lem
| iTrm =>
lazymatch lem with
- | @iTrm string ?H _ hnil ?pat =>
- iSpecializePat H pat; last tac H
- | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+ | @iTrm string ?H _ hnil ?pat => iSpecializePat H pat; last (tac H)
+ | _ => iPoseProofCore lem as tac
end
- | _ => let H := iFresh in iPoseProof lem as H; last tac H; try apply _
+ | _ => iPoseProofCore lem as tac
end.
-Tactic Notation "iDestruct" open_constr(H) "as" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1) ")"
+Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=
+ iDestructCore lem as (fun H => iDestructHyp H as pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) ")" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) ")" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) ")" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7) ")"
constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "(" simple_intropattern(x1)
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 ) pat).
+Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4)
simple_intropattern(x5) simple_intropattern(x6) simple_intropattern(x7)
simple_intropattern(x8) ")" constr(pat) :=
- iDestructHelp H as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
+ iDestructCore lem as (fun H => iDestructHyp H as ( x1 x2 x3 x4 x5 x6 x7 x8 ) pat).
-Tactic Notation "iDestruct" open_constr(H) "as" "%" simple_intropattern(pat) :=
- let Htmp := iFresh in iDestruct H as Htmp; last iPure Htmp as pat.
+Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
+ iDestructCore lem as (fun H => iPure H as pat).
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
@@ -781,33 +811,33 @@ Local Ltac iRewriteFindPred :=
match goal with |- (∀ y, @?Ψ y ⊣⊢ _) => unify Φ Ψ; reflexivity end
end.
-Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) :=
- let Heq := iFresh in iPoseProof t as Heq; last (
- eapply (tac_rewrite _ Heq _ _ lr);
- [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
- |let P := match goal with |- ?P ⊢ _ => P end in
- reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
- |iRewriteFindPred
- |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
-
-Tactic Notation "iRewrite" open_constr(t) := iRewriteCore false t.
-Tactic Notation "iRewrite" "-" open_constr(t) := iRewriteCore true t.
-
-Local Tactic Notation "iRewriteCore" constr(lr) open_constr(t) "in" constr(H) :=
- let Heq := iFresh in iPoseProof t as Heq; last (
- eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
- [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
- |env_cbv; reflexivity || fail "iRewrite:" H "not found"
- |let P := match goal with |- ?P ⊢ _ => P end in
- reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
- |iRewriteFindPred
- |intros ??? ->; reflexivity
- |env_cbv; reflexivity|lazy beta; iClear Heq]).
-
-Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
- iRewriteCore false t in H.
-Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
- iRewriteCore true t in H.
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
+ iPoseProofCore lem as (fun Heq =>
+ eapply (tac_rewrite _ Heq _ _ lr);
+ [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+ |let P := match goal with |- ?P ⊢ _ => P end in
+ reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+ |iRewriteFindPred
+ |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore false lem.
+Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore true lem.
+
+Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H) :=
+ iPoseProofCore lem as (fun Heq =>
+ eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
+ [env_cbv; reflexivity || fail "iRewrite:" Heq "not found"
+ |env_cbv; reflexivity || fail "iRewrite:" H "not found"
+ |let P := match goal with |- ?P ⊢ _ => P end in
+ reflexivity || fail "iRewrite:" Heq ":" P "not an equality"
+ |iRewriteFindPred
+ |intros ??? ->; reflexivity
+ |env_cbv; reflexivity|lazy beta; iClear Heq]).
+
+Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
+ iRewriteCore false lem in H.
+Tactic Notation "iRewrite" "-" open_constr(lem) "in" constr(H) :=
+ iRewriteCore true lem in H.
Ltac iSimplifyEq := repeat (
iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)