diff --git a/CHANGELOG.md b/CHANGELOG.md
index 71bcaac71237c996523b981de75bc7c7eccb7615..ad672458debb94858e2965932f657a47431009da 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -8,7 +8,7 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
* [#] Add new modality: â– ("plainly").
-* [#] Camera morphisms have to be homomorphisms, not just monotone functions.
+* Camera morphisms have to be homomorphisms, not just monotone functions.
* Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
(defined in the logic of Iris using impredicative quantification).
@@ -80,9 +80,18 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
tactics now no longer work when the universal quantifier or modality is
behind a type class opaque definition. Furthermore, this can change the
name of anonymous identifiers introduced with the "%" pattern.
+* Make `ofe_fun` dependently typed, subsuming `iprod`. The latter got removed.
+* Generalize `saved_prop` to let the user choose the location of the type-level
+ later. Rename the general form to `saved_anything`. Provide `saved_prop` and
+ `saved_pred` as special cases.
* Define the generic `fill` operation of the `ectxi_language` construct in terms
of a left fold instead of a right fold. This gives rise to more definitional
equalities.
+* The language hierarchy (`language`, `ectx_language`, `ectxi_language`) is now
+ fully formalized using canonical structures instead of using a mixture of
+ type classes and canonical structures. Also, it now uses explicit mixins. The
+ file `program_logic/ectxi_language` contains some documentation on how to
+ setup Iris for your language.
* Improved big operators:
+ They are no longer tied to cameras, but work on any monoid
+ The version of big operations over lists was redefined so that it enjoys
diff --git a/docs/algebra.tex b/docs/algebra.tex
index 972778a8217596cd47a8057cd0941ac803bf4fa9..9cfed25eaca982e31b347286ce1b1b4eabe61bd7 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -213,14 +213,16 @@ Note that for RAs, this and the RA-based definition of a frame-preserving update
Note that every RA is a discrete CMRA, by picking the discrete COFE for the equivalence relation.
Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE structure, as well as the step-index of $\mval$.
-\begin{defn}
- A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{monotone} (written $f : \monoid_1 \monra \monoid_2$) if it satisfies the following conditions:
+\begin{defn}[CMRA homomorphism]
+ A function $f : \monoid_1 \to \monoid_2$ between two CMRAs is \emph{a CMRA homomorphism} if it satisfies the following conditions:
\begin{enumerate}[itemsep=0pt]
\item $f$ is non-expansive
+ \item $f$ commutes with composition:\\
+ $\All \melt_1 \in \monoid_1, \melt_2 \in \monoid_1. f(\melt_1) \mtimes f(\melt_2) = f(\melt_1 \mtimes \melt_2)$
+ \item $f$ commutes with the core:\\
+ $\All \melt \in \monoid_1. \mcore{f(\melt)} = f(\mcore{\melt})$
\item $f$ preserves validity: \\
$\All n, \melt \in \monoid_1. \melt \in \mval_n \Ra f(\melt) \in \mval_n$
- \item $f$ preserves CMRA inclusion:\\
- $\All \melt \in \monoid_1, \meltB \in \monoid_1. \melt \mincl \meltB \Ra f(\melt) \mincl f(\meltB)$
\end{enumerate}
\end{defn}
diff --git a/docs/derived.tex b/docs/derived.tex
index 78cf6a6537cd19402a5b805168b3c26a1d59086b..13474276b789c17bccc6e7215c56fbd459908fb7 100644
--- a/docs/derived.tex
+++ b/docs/derived.tex
@@ -82,7 +82,7 @@ The two core assertions are: $\BoxSlice\namesp\prop\sname$, saying that there is
\inferH{Slice-delete-empty}
{f(\sname) = \BoxEmp}
- {\BoxSlice\namesp\propB\sname \proves \lateropt b\ABox\namesp\prop{f} \vs[\namesp] \Exists \prop'. \lateropt b(\later(\prop = \prop' * \propB) * \ABox\namesp{\prop'}{\mapinsert\gname\bot{f}})}
+ {\BoxSlice\namesp\propB\sname \proves \lateropt b\ABox\namesp\prop{f} \vs[\namesp] \Exists \prop'. \lateropt b(\later(\prop = \prop' * \propB) * \ABox\namesp{\prop'}{\mapinsert\sname\bot{f}})}
\inferH{Slice-fill}
{f(\sname) = \BoxEmp}
@@ -117,10 +117,10 @@ We need a CMRA as follows:
Now we can define the assertions:
\begin{align*}
- \SliceInv(\sname, \prop) \eqdef{}& \Exists b. \ownGhost\sname{(\authfull b, \munit)} * (b = 1 \Ra \prop) \\
+ \SliceInv(\sname, \prop) \eqdef{}& \Exists b. \ownGhost\sname{(\authfull b, \munit)} * ((b = \BoxFull) \Ra \prop) \\
\BoxSlice\namesp\prop\sname \eqdef{}& \ownGhost\sname{(\munit, \prop)} * \knowInv\namesp{\SliceInv(\sname,\prop)} \\
\ABox\namesp\prop{f} \eqdef{}& \Exists \propB : \nat \to \Prop. \later\left( \prop = \Sep_{\sname \in \dom(f)} \propB(\sname) \right ) * {}\\
- & \Sep_{\sname \in \dom(f)} \Exists \gname. \ownGhost\sname{(\authfrag f(\sname), \propB(\sname))} * \knowInv\namesp{\SliceInv(\sname,\propB(\sname))}
+ & \Sep_{\sname \in \dom(f)} \ownGhost\sname{(\authfrag f(\sname), \propB(\sname))} * \knowInv\namesp{\SliceInv(\sname,\propB(\sname))}
\end{align*}
\endgroup % Model paragraph
@@ -136,7 +136,7 @@ Here are some derived rules:
\inferH{Slice-split}
{f(\sname) = s}
- {\kern-4ex\BoxSlice\namesp{\propB_1 * \propB_2}\sname \proves \lateropt b \ABox\namesp\prop{f} \vs[\namesp] \Exists \sname_1 \notin \dom(f), \sname_2 \notin \dom(f). \sname_1 \neq \sname_1 \land {}\\\kern5ex \always\BoxSlice\namesp{\propB_1}{\sname_1} * \always\BoxSlice\namesp{\propB_2}{\sname_2} * \lateropt b \ABox\namesp\prop{\mapinsert{\sname_2}{s}{\mapinsert{\sname_1}{s}{\mapinsert\sname\bot{f}}}}}
+ {\kern-4ex\BoxSlice\namesp{\propB_1 * \propB_2}\sname \proves \lateropt b \ABox\namesp\prop{f} \vs[\namesp] \Exists \sname_1 \notin \dom(f), \sname_2 \notin \dom(f). \sname_1 \neq \sname_2 \land {}\\\kern5ex \always\BoxSlice\namesp{\propB_1}{\sname_1} * \always\BoxSlice\namesp{\propB_2}{\sname_2} * \lateropt b \ABox\namesp\prop{\mapinsert{\sname_2}{s}{\mapinsert{\sname_1}{s}{\mapinsert\sname\bot{f}}}}}
\inferH{Slice-merge}
{\sname_1 \neq \sname_2 \and f(\sname_1) = f(\sname_2) = s}
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 084200b03e8136b9d40510a34b2af53a0fbf01d6..3541c1070f23841302de950e763c2ea2c226c1eb 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -257,7 +257,7 @@ This can be instantiated, for example, with ownership of an authoritative RA to
\begin{align*}
\textdom{wp} \eqdef{}& \MU \textdom{wp}. \Lam \mask, \expr, \pred. \\
- & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \prop) \lor {}\\
+ & (\Exists\val. \toval(\expr) = \val \land \pvs[\mask] \pred(\val)) \lor {}\\
& \Bigl(\toval(\expr) = \bot \land \All \state. I(\state) \vsW[\mask][\emptyset] {}\\
&\qquad \red(\expr, \state) * \later\All \expr', \state', \vec\expr. (\expr, \state \step \expr', \state', \vec\expr) \vsW[\emptyset][\mask] {}\\
&\qquad\qquad I(\state') * \textdom{wp}(\mask, \expr', \pred) * \Sep_{\expr'' \in \vec\expr} \textdom{wp}(\top, \expr'', \Lam \any. \TRUE)\Bigr) \\
diff --git a/opam b/opam
index e3f1c66f6607ab205aecc834a2b2ecb3cbb350f8..6e0055ed38a08223a584482192853ae4172988c4 100644
--- a/opam
+++ b/opam
@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.6.1" & < "8.8~" }
"coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
- "coq-stdpp" { (= "dev.2017-10-28.7") | (= "dev") }
+ "coq-stdpp" { (= "dev.2017-11-22.1") | (= "dev") }
]
diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 06262f85016146a1e84bda7aabd214fa1a33f602..79f8e4978406798c1221ae3887e41e39da0d2565 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,8 @@
From mathcomp Require Export ssreflect.
From stdpp Require Export prelude.
Set Default Proof Using "Type".
+(* Reset options set by the ssreflect plugin to their defaults *)
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
+Global Unset Asymmetric Patterns.
Ltac done := stdpp.tactics.done.
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index a18c18aeb4804e8fe5f97cda6cf11fb05bf65c7b..3729d5f48233a6347e7cb53a50703fd11e647fcb 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -30,10 +30,10 @@ Arguments big_opL {M} o {_ A} _ !_ /.
Typeclasses Opaque big_opL.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
- format "[^ o list] k ↦ x ∈ l , P") : C_scope.
+ format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
(at level 200, o at level 1, l at level 10, x at level 1, right associativity,
- format "[^ o list] x ∈ l , P") : C_scope.
+ format "[^ o list] x ∈ l , P") : stdpp_scope.
Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K → A → M)
(m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
@@ -42,10 +42,10 @@ Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
Typeclasses Opaque big_opM.
Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
(at level 200, o at level 1, m at level 10, k, x at level 1, right associativity,
- format "[^ o map] k ↦ x ∈ m , P") : C_scope.
+ format "[^ o map] k ↦ x ∈ m , P") : stdpp_scope.
Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
(at level 200, o at level 1, m at level 10, x at level 1, right associativity,
- format "[^ o map] x ∈ m , P") : C_scope.
+ format "[^ o map] x ∈ m , P") : stdpp_scope.
Definition big_opS `{Monoid M o} `{Countable A} (f : A → M)
(X : gset A) : M := big_opL o (λ _, f) (elements X).
@@ -54,7 +54,7 @@ Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opS.
Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
- format "[^ o set] x ∈ X , P") : C_scope.
+ format "[^ o set] x ∈ X , P") : stdpp_scope.
Definition big_opMS `{Monoid M o} `{Countable A} (f : A → M)
(X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
@@ -63,7 +63,7 @@ Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
Typeclasses Opaque big_opMS.
Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
(at level 200, o at level 1, X at level 10, x at level 1, right associativity,
- format "[^ o mset] x ∈ X , P") : C_scope.
+ format "[^ o mset] x ∈ X , P") : stdpp_scope.
(** * Properties about big ops *)
Section big_op.
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index b6c22f5ba318be9dae79d2b19d144a26013b32f1..3c3b1171ca0a40c770e295e5aaff79a7dcecd443 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -8,8 +8,8 @@ Instance: Params (@pcore) 2.
Class Op (A : Type) := op : A → A → A.
Hint Mode Op ! : typeclass_instances.
Instance: Params (@op) 2.
-Infix "â‹…" := op (at level 50, left associativity) : C_scope.
-Notation "(â‹…)" := op (only parsing) : C_scope.
+Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
+Notation "(â‹…)" := op (only parsing) : stdpp_scope.
(* The inclusion quantifies over [A], not [option A]. This means we do not get
reflexivity. However, if we used [option A], the following would no longer
@@ -17,8 +17,8 @@ Notation "(â‹…)" := op (only parsing) : C_scope.
x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
*)
Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
-Infix "≼" := included (at level 70) : C_scope.
-Notation "(≼)" := included (only parsing) : C_scope.
+Infix "≼" := included (at level 70) : stdpp_scope.
+Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ ≼ _) => reflexivity.
Instance: Params (@included) 3.
@@ -31,11 +31,11 @@ Notation "✓{ n } x" := (validN n x)
Class Valid (A : Type) := valid : A → Prop.
Hint Mode Valid ! : typeclass_instances.
Instance: Params (@valid) 2.
-Notation "✓ x" := (valid x) (at level 20) : C_scope.
+Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
- (at level 70, n at next level, format "x ≼{ n } y") : C_scope.
+ (at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (_ ≼{_} _) => reflexivity.
@@ -140,7 +140,7 @@ End cmra_mixin.
Definition opM {A : cmraT} (x : A) (my : option A) :=
match my with Some y => x â‹… y | None => x end.
-Infix "â‹…?" := opM (at level 50, left associativity) : C_scope.
+Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
(** * CoreId elements *)
Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
diff --git a/theories/algebra/dra.v b/theories/algebra/dra.v
index fcbccb2a249c522e4b8cdef15746551219d8b09b..dc459baf45b763368a8be51d8773630aef0541e4 100644
--- a/theories/algebra/dra.v
+++ b/theories/algebra/dra.v
@@ -199,7 +199,7 @@ Proof. split; naive_solver eauto using dra_op_valid. Qed.
(* TODO: This has to be proven again. *)
(*
Lemma to_validity_included x y:
- (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
+ (✓ y ∧ to_validity x ≼ to_validity y)%stdpp ↔ (✓ x ∧ x ≼ y).
Proof.
split.
- move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 9997c5c4bae25b969a73c9ff488296b0ca942d1e..56d17e71096d71848325e74fce4f1ea7b0b9e2b3 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -620,9 +620,9 @@ Definition ccompose {A B C}
(f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
Instance: Params (@ccompose) 3.
Infix "â—Ž" := ccompose (at level 40, left associativity).
-Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
- f1 ≡{n}≡ f2 → g1 ≡{n}≡ g2 → f1 ◎ g1 ≡{n}≡ f2 ◎ g2.
-Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
+Global Instance ccompose_ne {A B C} :
+ NonExpansive2 (@ccompose A B C).
+Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
(* Function space maps *)
Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
@@ -1061,6 +1061,7 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
+Instance: Params (@Next) 1.
Section later.
Context {A : ofeT}.
@@ -1100,8 +1101,7 @@ Section later.
(* f is contractive iff it can factor into `Next` and a non-expansive function. *)
Lemma contractive_alt {B : ofeT} (f : A → B) :
- Contractive f ↔ ∃ g : later A → B,
- (NonExpansive g) ∧ (∀ x, f x ≡ g (Next x)).
+ Contractive f ↔ ∃ g : later A → B, NonExpansive g ∧ ∀ x, f x ≡ g (Next x).
Proof.
split.
- intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index c49f186fc0db0d634dc7058db8c0765f56587cfc..66e4726e9c67e57f4b690e5930614bac087009c9 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -79,7 +79,7 @@ Qed.
Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
Proof.
intros S1 S2 HS T1 T2 HT. rewrite /up_set.
- f_equiv=> // s1 s2 Hs. by apply up_preserving.
+ f_equiv=> // s1 s2. by apply up_preserving.
Qed.
Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
Proof.
diff --git a/theories/base_logic/deprecated.v b/theories/base_logic/deprecated.v
index 90180e673c4acdc4deec7b2d9fa7333bc45d1fd3..3a3b9c86208c569e9855f1bd64d0f11950bd9667 100644
--- a/theories/base_logic/deprecated.v
+++ b/theories/base_logic/deprecated.v
@@ -2,11 +2,11 @@ From iris.base_logic Require Import primitive.
Set Default Proof Using "Type".
(* Deprecated 2016-11-22. Use ⌜φ⌠instead. *)
-Notation "■φ" := (uPred_pure φ%C%type)
+Notation "■φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity, only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x = y⌠instead. *)
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) (only parsing) : uPred_scope.
+Notation "x = y" := (uPred_pure (x%stdpp%type = y%stdpp%type)) (only parsing) : uPred_scope.
(* Deprecated 2016-11-22. Use ⌜x ## y ⌠instead. *)
-Notation "x ## y" := (uPred_pure (x%C%type ## y%C%type)) (only parsing) : uPred_scope.
+Notation "x ## y" := (uPred_pure (x%stdpp%type ## y%stdpp%type)) (only parsing) : uPred_scope.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c6c897cbe4b616d6563585a1e3ea14a608812780..55f213448edb758142cd0a5ed2cd38267a548e6a 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -672,9 +672,7 @@ Proof.
Qed.
(* Later derived *)
-Lemma later_proper P Q : (P ⊣⊢ Q) → ▷ P ⊣⊢ ▷ Q.
-Proof. by intros ->. Qed.
-Hint Resolve later_mono later_proper.
+Hint Resolve later_mono.
Global Instance later_mono' : Proper ((⊢) ==> (⊢)) (@uPred_later M).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
@@ -725,9 +723,9 @@ Proof. done. Qed.
Lemma later_laterN n P : ▷^(S n) P ⊣⊢ ▷ ▷^n P.
Proof. done. Qed.
Lemma laterN_later n P : ▷^(S n) P ⊣⊢ ▷^n ▷ P.
-Proof. induction n; simpl; auto. Qed.
+Proof. induction n; f_equiv/=; auto. Qed.
Lemma laterN_plus n1 n2 P : ▷^(n1 + n2) P ⊣⊢ ▷^n1 ▷^n2 P.
-Proof. induction n1; simpl; auto. Qed.
+Proof. induction n1; f_equiv/=; auto. Qed.
Lemma laterN_le n1 n2 P : n1 ≤ n2 → ▷^n1 P ⊢ ▷^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
@@ -745,22 +743,22 @@ Proof. induction n as [|n IH]; simpl; by rewrite -?later_intro. Qed.
Lemma laterN_True n : ▷^n True ⊣⊢ True.
Proof. apply (anti_symm (⊢)); auto using laterN_intro. Qed.
Lemma laterN_forall {A} n (Φ : A → uPred M) : (▷^n ∀ a, Φ a) ⊣⊢ (∀ a, ▷^n Φ a).
-Proof. induction n as [|n IH]; simpl; rewrite -?later_forall; auto. Qed.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_forall ?IH; auto. Qed.
Lemma laterN_exist_2 {A} n (Φ : A → uPred M) : (∃ a, ▷^n Φ a) ⊢ ▷^n (∃ a, Φ a).
Proof. apply exist_elim; eauto using exist_intro, laterN_mono. Qed.
Lemma laterN_exist `{Inhabited A} n (Φ : A → uPred M) :
(▷^n ∃ a, Φ a) ⊣⊢ ∃ a, ▷^n Φ a.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_exist; auto. Qed.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_exist ?IH; auto. Qed.
Lemma laterN_and n P Q : ▷^n (P ∧ Q) ⊣⊢ ▷^n P ∧ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_and; auto. Qed.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_and ?IH; auto. Qed.
Lemma laterN_or n P Q : ▷^n (P ∨ Q) ⊣⊢ ▷^n P ∨ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_or; auto. Qed.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_or ?IH; auto. Qed.
Lemma laterN_impl n P Q : ▷^n (P → Q) ⊢ ▷^n P → ▷^n Q.
Proof.
apply impl_intro_l; rewrite -laterN_and; eauto using impl_elim, laterN_mono.
Qed.
Lemma laterN_sep n P Q : ▷^n (P ∗ Q) ⊣⊢ ▷^n P ∗ ▷^n Q.
-Proof. induction n as [|n IH]; simpl; rewrite -?later_sep; auto. Qed.
+Proof. induction n as [|n IH]; simpl; rewrite -?later_sep ?IH; auto. Qed.
Lemma laterN_wand n P Q : ▷^n (P -∗ Q) ⊢ ▷^n P -∗ ▷^n Q.
Proof.
apply wand_intro_r; rewrite -laterN_sep; eauto using wand_elim_l,laterN_mono.
@@ -980,6 +978,13 @@ Lemma plainly_plainly P `{!Plain P} : ■P ⊣⊢ P.
Proof. apply (anti_symm (⊢)); eauto. Qed.
Lemma plainly_intro P Q `{!Plain P} : (P ⊢ Q) → P ⊢ ■Q.
Proof. rewrite -(plainly_plainly P); apply plainly_intro'. Qed.
+Lemma plainly_alt P : ■P ⊣⊢ P ≡ True.
+Proof.
+ apply (anti_symm (⊢)).
+ - rewrite -prop_ext. apply plainly_mono, and_intro; apply impl_intro_r; auto.
+ - rewrite internal_eq_sym (internal_eq_rewrite _ _ (λ P, ■P)%I).
+ by rewrite plainly_pure True_impl.
+Qed.
Lemma bupd_plain P `{!Plain P} : (|==> P) ⊢ P.
Proof. by rewrite -{1}(plainly_plainly P) bupd_plainly. Qed.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index 38754d6147edf9846ec42c203c5aef33a835ddd2..a27253cd1667f3dcd789eb57fe9e6ec25c65a5ba 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -9,7 +9,7 @@ Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
Notation "|=n=> Q" := (uPred_nnupd Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P ⊢ |=n=> Q)
- (at level 99, Q at level 200, only parsing) : C_scope.
+ (at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P =n=∗ Q" := (P -∗ |=n=> Q)%I
(at level 99, Q at level 200, format "P =n=∗ Q") : uPred_scope.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 5b5cd98d8b840049f92beb4e6d07b62f691a1bb4..cdc57057a08a659e3e8ae04da26d55f82565955e 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -24,7 +24,7 @@ Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
format "P ={ E1 , E2 }=∗ Q") : uPred_scope.
Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
- (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.
+ (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "|={ E }=> Q" := (fupd E E Q)
(at level 99, E at level 50, Q at level 200,
@@ -33,7 +33,7 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=∗ Q") : uPred_scope.
Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
- (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
+ (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
Section fupd.
Context `{invG Σ}.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 1608c9a29e941181ae9db80c95ecf686113466dd..8b140f72453a3e8003307a1b281ee04435552bd8 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -92,7 +92,7 @@ End inv.
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
- let pat := constr:(IList [[IName Htmp; patback]]) in
+ let pat := constr:(IList [[IIdent Htmp; patback]]) in
iMod (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v
index 76857b335d1feb7ecf538fcb3e5e3976c475ddb7..dc226f276d5a29ec5eaf26085ca33c4bda87d040 100644
--- a/theories/base_logic/lib/namespaces.v
+++ b/theories/base_logic/lib/namespaces.v
@@ -21,8 +21,8 @@ Instance nclose : UpClose namespace coPset := unseal nclose_aux.
Definition nclose_eq : @nclose = @nclose_def := seal_eq nclose_aux.
Notation "N .@ x" := (ndot N x)
- (at level 19, left associativity, format "N .@ x") : C_scope.
-Notation "(.@)" := ndot (only parsing) : C_scope.
+ (at level 19, left associativity, format "N .@ x") : stdpp_scope.
+Notation "(.@)" := ndot (only parsing) : stdpp_scope.
Instance ndisjoint : Disjoint namespace := λ N1 N2, nclose N1 ## nclose N2.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 2ff8cc19d2601f5d6ac72a4c08069d520a1bfba9..9b5f721e7e6577d6f646ac315cbeaa85a5e47e48 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -1,48 +1,118 @@
From iris.base_logic Require Export own.
From iris.algebra Require Import agree.
From stdpp Require Import gmap.
+From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
-Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
- saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
-Definition savedPropΣ (F : cFunctor) : gFunctors :=
- #[ GFunctor (agreeRF (â–¶ F)) ].
+(* "Saved anything" -- this can give you saved propositions, saved predicates,
+ saved whatever-you-like. *)
-Instance subG_savedPropΣ {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
+Class savedAnythingG (Σ : gFunctors) (F : cFunctor) :=
+ saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ))).
+Definition savedAnythingΣ (F : cFunctor) `{!cFunctorContractive F} : gFunctors :=
+ #[ GFunctor (agreeRF F) ].
+
+Instance subG_savedAnythingΣ {Σ F} `{!cFunctorContractive F} :
+ subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
Proof. solve_inG. Qed.
-Definition saved_prop_own `{savedPropG Σ F}
+Definition saved_anything_own `{savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
- own γ (to_agree $ Next (cFunctor_map F (iProp_fold, iProp_unfold) x)).
-Typeclasses Opaque saved_prop_own.
-Instance: Params (@saved_prop_own) 3.
+ own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
+Typeclasses Opaque saved_anything_own.
+Instance: Params (@saved_anything_own) 4.
-Section saved_prop.
- Context `{savedPropG Σ F}.
+Section saved_anything.
+ Context `{savedAnythingG Σ F}.
Implicit Types x y : F (iProp Σ).
Implicit Types γ : gname.
- Global Instance saved_prop_persistent γ x : Persistent (saved_prop_own γ x).
- Proof. rewrite /saved_prop_own; apply _. Qed.
+ Global Instance saved_anything_persistent γ x :
+ Persistent (saved_anything_own γ x).
+ Proof. rewrite /saved_anything_own; apply _. Qed.
+
+ Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
+ Proof. solve_proper. Qed.
+ Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
+ Proof. solve_proper. Qed.
- Lemma saved_prop_alloc_strong x (G : gset gname) :
- (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_prop_own γ x)%I.
+ Lemma saved_anything_alloc_strong x (G : gset gname) :
+ (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_anything_own γ x)%I.
Proof. by apply own_alloc_strong. Qed.
- Lemma saved_prop_alloc x : (|==> ∃ γ, saved_prop_own γ x)%I.
+ Lemma saved_anything_alloc x : (|==> ∃ γ, saved_anything_own γ x)%I.
Proof. by apply own_alloc. Qed.
- Lemma saved_prop_agree γ x y :
- saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
+ Lemma saved_anything_agree γ x y :
+ saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y.
Proof.
- apply wand_intro_r.
- rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+ iIntros "Hx Hy". rewrite /saved_anything_own.
+ iDestruct (own_valid_2 with "Hx Hy") as "Hv".
+ rewrite agree_validI agree_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert (∀ z, G2 (G1 z) ≡ z) as help.
{ intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
- rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
+ rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv.
Qed.
-End saved_prop.
+End saved_anything.
+
+(** Provide specialized versions of this for convenience. **)
+
+(* Saved propositions. *)
+Notation savedPropG Σ := (savedAnythingG Σ (▶ ∙)).
+Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
+
+Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+ saved_anything_own (F := ▶ ∙) γ (Next P).
+
+Instance saved_prop_own_contractive `{savedPropG Σ} γ :
+ Contractive (saved_prop_own γ).
+Proof. solve_contractive. Qed.
+
+Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+ (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
+ (|==> ∃ γ, saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+Lemma saved_prop_agree `{savedPropG Σ} γ P Q :
+ saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
+Proof.
+ iIntros "HP HQ". iApply later_equivI. iApply (saved_anything_agree with "HP HQ").
+Qed.
+
+(* Saved predicates. *)
+Notation savedPredG Σ A := (savedAnythingG Σ (A -c> ▶ ∙)).
+Notation savedPredΣ A := (savedAnythingΣ (A -c> ▶ ∙)).
+
+Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+ saved_anything_own (F := A -c> ▶ ∙) γ (CofeMor Next ∘ Φ).
+
+Instance saved_pred_own_contractive `{savedPredG Σ A} γ :
+ Contractive (saved_pred_own γ : (A -c> iProp Σ) → iProp Σ).
+Proof.
+ solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
+Qed.
+
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+ (|==> ∃ γ, ⌜γ ∉ G⌠∧ saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
+Lemma saved_pred_alloc `{savedPredG Σ A} (Φ : A → iProp Σ) :
+ (|==> ∃ γ, saved_pred_own γ Φ)%I.
+Proof. iApply saved_anything_alloc. Qed.
+
+(* We put the `x` on the outside to make this lemma easier to apply. *)
+Lemma saved_pred_agree `{savedPredG Σ A} γ Φ Ψ x :
+ saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
+Proof.
+ iIntros "HΦ HΨ". unfold saved_pred_own. iApply later_equivI.
+ iDestruct (ofe_funC_equivI (CofeMor Next ∘ Φ) (CofeMor Next ∘ Ψ)) as "[FE _]".
+ simpl. iApply ("FE" with "[-]").
+ iApply (saved_anything_agree with "HΦ HΨ").
+Qed.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index a77383a4524e7a06a80674953b99b5efe5143b3e..c8ab4eb42184ab7bd29885a29e9712d2a57af845 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -16,10 +16,10 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I
Notation "P ={ E1 , E2 }=> Q" := (P ={E1,E2}=> Q)%I
(at level 99, E1,E2 at level 50, Q at level 200,
- format "P ={ E1 , E2 }=> Q") : C_scope.
+ format "P ={ E1 , E2 }=> Q") : stdpp_scope.
Notation "P ={ E }=> Q" := (P ={E}=> Q)%I
(at level 99, E at level 50, Q at level 200,
- format "P ={ E }=> Q") : C_scope.
+ format "P ={ E }=> Q") : stdpp_scope.
Section vs.
Context `{invG Σ}.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 1bc3e3d16a06e09d99ada1a723a4f582744a323f..a26f4f6ae6395fd36dfc415e01f14410ffd7d46c 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -23,6 +23,7 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
Arguments ownI {_ _} _ _%I.
Typeclasses Opaque ownI.
+Instance: Params (@invariant_unfold) 1.
Instance: Params (@ownI) 3.
Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
@@ -104,7 +105,7 @@ Qed.
Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
Proof.
rewrite /ownI /wsat -!lock.
- iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
+ iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
@@ -115,7 +116,7 @@ Qed.
Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
Proof.
rewrite /ownI /wsat -!lock.
- iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
+ iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[].
@@ -128,7 +129,7 @@ Lemma ownI_alloc φ P :
wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌠∗ wsat ∗ ownI i P.
Proof.
iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
- iDestruct "Hw" as (I) "[? HI]".
+ iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "[$]") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
@@ -150,7 +151,7 @@ Lemma ownI_alloc_open φ P :
(∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
wsat ==∗ ∃ i, ⌜φ i⌠∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
Proof.
- iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]".
+ iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "[$]") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index 3aab1eeb26c85419f51946db655848aa2e04a47a..1e123fa4bb0058bce0980ab3320647fea1a7f2aa 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -168,7 +168,7 @@ Definition uPred_bupd {M} := unseal uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := seal_eq uPred_bupd_aux.
(* Latest notation *)
-Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%C%type)
+Notation "'⌜' φ 'âŒ'" := (uPred_pure φ%stdpp%type)
(at level 1, φ at level 200, format "⌜ φ âŒ") : uPred_scope.
Notation "'False'" := (uPred_pure False) : uPred_scope.
Notation "'True'" := (uPred_pure True) : uPred_scope.
@@ -198,7 +198,7 @@ Notation "✓ x" := (uPred_cmra_valid x) (at level 20) : uPred_scope.
Notation "|==> Q" := (uPred_bupd Q)
(at level 99, Q at level 200, format "|==> Q") : uPred_scope.
Notation "P ==∗ Q" := (P ⊢ |==> Q)
- (at level 99, Q at level 200, only parsing) : C_scope.
+ (at level 99, Q at level 200, only parsing) : stdpp_scope.
Notation "P ==∗ Q" := (P -∗ |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope.
@@ -206,7 +206,7 @@ Coercion uPred_valid {M} (P : uPred M) : Prop := True%I ⊢ P.
Typeclasses Opaque uPred_valid.
Notation "P -∗ Q" := (P ⊢ Q)
- (at level 99, Q at level 200, right associativity) : C_scope.
+ (at level 99, Q at level 200, right associativity) : stdpp_scope.
Module uPred.
Definition unseal_eqs :=
@@ -307,7 +307,8 @@ Proof.
unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
apply HPQ; eauto using cmra_validN_S.
Qed.
-Global Instance later_proper' :
+Definition later_ne : NonExpansive (@uPred_later M) := _.
+Global Instance later_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
Global Instance plainly_ne : NonExpansive (@uPred_plainly M).
Proof.
@@ -649,7 +650,7 @@ Proof.
- intros i a b; eapply Hf, ucmra_unit_validN.
Qed.
-(* Functions *)
+(* Function extensionality *)
Lemma ofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
Proof. by unseal. Qed.
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 801608cd705f7fd80e77f93296d92d0dc5947fe6..57d91bc94e298c372cb47dce4b70aae5a3243469 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -28,7 +28,20 @@ Record uPred (M : ucmraT) : Type := IProp {
are monotonous both with respect to the step index and with
respect to x. However, that would essentially require changing
(by making it more complicated) the model of many connectives of
- the logic, which we don't want. *)
+ the logic, which we don't want.
+ This sub-COFE is the sub-COFE of monotonous sProp predicates P
+ such that the following sProp assertion is valid:
+ ∀ x, (V(x) → P(x)) → P(x)
+ Where V is the validity predicate.
+
+ Another way of saying that this is equivalent to this definition of
+ uPred is to notice that our definition of uPred is equivalent to
+ quotienting the COFE of monotonous sProp predicates with the
+ following (sProp) equivalence relation:
+ P1 ≡ P2 := ∀ x, V(x) → (P1(x) ↔ P2(x))
+ whose equivalence classes appear to all have one only canonical
+ representative such that ∀ x, (V(x) → P(x)) → P(x).
+ *)
uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
}.
Arguments uPred_holds {_} _ _ _ : simpl never.
@@ -158,11 +171,11 @@ Hint Resolve uPred_mono uPred_closed : uPred_def.
(** Notations *)
Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
- (at level 99, Q at level 200, right associativity) : C_scope.
-Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
+ (at level 99, Q at level 200, right associativity) : stdpp_scope.
+Notation "(⊢)" := uPred_entails (only parsing) : stdpp_scope.
Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
- (at level 95, no associativity) : C_scope.
-Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
+ (at level 95, no associativity) : stdpp_scope.
+Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : stdpp_scope.
Module uPred.
Section entails.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e3fd5407518ba00c02e012b2e09cb1bae211f8ed..ac4795d5d88be648a1217a05898330597c93ebf1 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -91,7 +91,7 @@ Bind Scope val_scope with val.
Fixpoint of_val (v : val) : expr :=
match v with
- | RecV f x e _ => Rec f x e
+ | RecV f x e => Rec f x e
| LitV l => Lit l
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
@@ -374,7 +374,7 @@ Lemma fill_item_val Ki e :
is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
-Lemma val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
@@ -467,20 +467,18 @@ Lemma subst_rec_ne' f y e x es :
(x ≠f ∨ f = BAnon) → (x ≠y ∨ y = BAnon) →
subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
+
+Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+Proof.
+ split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
+ fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
+Qed.
End heap_lang.
(** Language *)
-Program Instance heap_ectxi_lang :
- EctxiLanguage
- (heap_lang.expr) heap_lang.val heap_lang.ectx_item heap_lang.state := {|
- of_val := heap_lang.of_val; to_val := heap_lang.to_val;
- fill_item := heap_lang.fill_item; head_step := heap_lang.head_step
-|}.
-Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
- heap_lang.val_stuck, heap_lang.fill_item_val, heap_lang.fill_item_no_val_inj,
- heap_lang.head_ctx_step_val.
-
-Canonical Structure heap_lang := ectx_lang (heap_lang.expr).
+Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
+Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
+Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
(* Prefer heap_lang names over ectx_language names. *)
Export heap_lang.
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 9abf0f6e7eff8755d4e0e5451fcc718090cb05a4..9da9bb33f18ab4a625e29d50eb145b0a82a882e1 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -49,7 +49,7 @@ Section proof.
{{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
Proof.
iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
- wp_seq. wp_alloc l as "Hl".
+ wp_lam. wp_alloc l as "Hl".
iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
{ iIntros "!>". iExists false. by iFrame. }
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 4d4d6cba841cbfb687b454444cb7562615f96ab7..7a9f78cd88906256508fae367b401f36579d7ee1 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -153,7 +153,7 @@ Section proof.
wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
- iDestruct "Haown" as "[[Hγo' _]|?]".
+ iDestruct "Haown" as "[[Hγo' _]|Haown]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 2251d52c218f87e4a0ed183c71014a12cf4c189f..5f8120d2974faa612fb57e649f6eacbfc2598452 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -61,16 +61,6 @@ Implicit Types Φ : val → iProp Σ.
Implicit Types efs : list expr.
Implicit Types σ : state.
-(** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
-Lemma wp_bind {s E e} K Φ :
- WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }} ⊢ WP fill K e @ s; E {{ Φ }}.
-Proof. exact: wp_ectx_bind. Qed.
-
-Lemma wp_bindi {s E e} Ki Φ :
- WP e @ s; E {{ v, WP fill_item Ki (of_val v) @ s; E {{ Φ }} }} ⊢
- WP fill_item Ki e @ s; E {{ Φ }}.
-Proof. exact: weakestpre.wp_bind. Qed.
-
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork s E e Φ :
▷ Φ (LitV LitUnit) ∗ ▷ WP e @ s; ⊤ {{ _, True }} ⊢ WP Fork e @ s; E {{ Φ }}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 0f95f3b9f44874d4a0052b39a848528bbda5d076..14ea78575cd670fba6587c31740591cfc6322ff2 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,16 +5,15 @@ From iris.heap_lang Require Export tactics lifting.
Set Default Proof Using "Type".
Import uPred.
-Lemma tac_wp_pure `{heapG Σ} K Δ Δ' s E e1 e2 φ Φ :
+Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2 →
φ →
IntoLaterNEnvs 1 Δ Δ' →
- envs_entails Δ' (WP fill K e2 @ s; E {{ Φ }}) →
- envs_entails Δ (WP fill K e1 @ s; E {{ Φ }}).
+ envs_entails Δ' (WP e2 @ s; E {{ Φ }}) →
+ envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof.
rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
- rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
- by rewrite -ectx_lifting.wp_ectx_bind_inv.
+ rewrite HΔ' -wp_pure_step_later //.
Qed.
Lemma tac_wp_value `{heapG Σ} Δ s E Φ e v :
@@ -27,13 +26,16 @@ Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Tactic Notation "wp_pure" open_constr(efoc) :=
iStartProof;
lazymatch goal with
- | |- envs_entails _ (wp ?s ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
- unify e' efoc;
- eapply (tac_wp_pure K);
- [simpl; apply _ (* PureExec *)
- |try fast_done (* The pure condition for PureExec *)
- |apply _ (* IntoLaters *)
- |simpl_subst; try wp_value_head (* new goal *)])
+ | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
+ let e := eval simpl in e in
+ reshape_expr e ltac:(fun K e' =>
+ unify e' efoc;
+ eapply (tac_wp_pure _ _ _ _ (fill K e'));
+ [apply _ (* PureExec *)
+ |try fast_done (* The pure condition for PureExec *)
+ |apply _ (* IntoLaters *)
+ |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'"
end.
@@ -55,7 +57,7 @@ Tactic Notation "wp_match" := wp_case; wp_let.
Lemma tac_wp_bind `{heapG Σ} K Δ s E Φ e :
envs_entails Δ (WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }})%I →
envs_entails Δ (WP fill K e @ s; 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
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index fd3fcd6354eb251b61d33dab429f74ce51af388e..c4268b60c2fc7eab4379dac5058081a947989dc4 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -39,7 +39,7 @@ Inductive expr :=
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
| Val v e' _ => e'
- | ClosedExpr e _ => e
+ | ClosedExpr e => e
| Var x => heap_lang.Var x
| Rec f x e => heap_lang.Rec f x (to_expr e)
| App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
@@ -100,7 +100,7 @@ Ltac of_expr e :=
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
- | Val _ _ _ | ClosedExpr _ _ => true
+ | Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x ∈ X)
| Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ => true
@@ -147,7 +147,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Val v e H => Val v e H
- | ClosedExpr e H => @ClosedExpr e H
+ | ClosedExpr e => ClosedExpr e
| Var y => if decide (x = y) then es else Var y
| Rec f y e =>
Rec f y $ if decide (BNamed x ≠f ∧ BNamed x ≠y) then subst x es e else e
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 8d7dbf1eeb15478fa570d905eb60019041a804c2..37700ac5152957d9d36ce9547d117a356a501c2b 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -4,9 +4,51 @@ From iris.algebra Require Export base.
From iris.program_logic Require Import language.
Set Default Proof Using "Type".
-(* We need to make those arguments indices that we want canonical structure
- inference to use a keys. *)
-Class EctxLanguage (expr val ectx state : Type) := {
+(* TAKE CARE: When you define an [ectxLanguage] canonical structure for your
+language, you need to also define a corresponding [language] canonical
+structure. Use the coercion [LanguageOfEctx] as defined in the bottom of this
+file for doing that. *)
+
+Section ectx_language_mixin.
+ Context {expr val ectx state : Type}.
+ Context (of_val : val → expr).
+ Context (to_val : expr → option val).
+ Context (empty_ectx : ectx).
+ Context (comp_ectx : ectx → ectx → ectx).
+ Context (fill : ectx → expr → expr).
+ Context (head_step : expr → state → expr → state → list expr → Prop).
+
+ Record EctxLanguageMixin := {
+ mixin_to_of_val v : to_val (of_val v) = Some v;
+ mixin_of_to_val e v : to_val e = Some v → of_val v = e;
+ mixin_val_head_stuck e1 σ1 e2 σ2 efs :
+ head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+
+ mixin_fill_empty e : fill empty_ectx e = e;
+ mixin_fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
+ mixin_fill_inj K : Inj (=) (=) (fill K);
+ mixin_fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e);
+
+ (* There are a whole lot of sensible axioms (like associativity, and left and
+ right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
+ positivity suffices. *)
+ mixin_ectx_positive K1 K2 :
+ comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
+
+ mixin_step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+ fill K e1 = fill K' e1' →
+ to_val e1 = None →
+ head_step e1' σ1 e2 σ2 efs →
+ ∃ K'', K' = comp_ectx K K'';
+ }.
+End ectx_language_mixin.
+
+Structure ectxLanguage := EctxLanguage {
+ expr : Type;
+ val : Type;
+ ectx : Type;
+ state : Type;
+
of_val : val → expr;
to_val : expr → option val;
empty_ectx : ectx;
@@ -14,63 +56,60 @@ Class EctxLanguage (expr val ectx state : Type) := {
fill : ectx → expr → expr;
head_step : expr → state → expr → state → list expr → Prop;
- to_of_val v : to_val (of_val v) = Some v;
- of_to_val e v : to_val e = Some v → of_val v = e;
- val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
-
- fill_empty e : fill empty_ectx e = e;
- fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e;
- fill_inj K :> Inj (=) (=) (fill K);
- fill_not_val K e : to_val e = None → to_val (fill K e) = None;
-
- (* There are a whole lot of sensible axioms (like associativity, and left and
- right identity, we could demand for [comp_ectx] and [empty_ectx]. However,
- positivity suffices. *)
- ectx_positive K1 K2 :
- comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx;
-
- step_by_val K K' e1 e1' σ1 e2 σ2 efs :
- fill K e1 = fill K' e1' →
- to_val e1 = None →
- head_step e1' σ1 e2 σ2 efs →
- exists K'', K' = comp_ectx K K'';
+ ectx_language_mixin :
+ EctxLanguageMixin of_val to_val empty_ectx comp_ectx fill head_step
}.
-Arguments of_val {_ _ _ _ _} _%V.
-Arguments to_val {_ _ _ _ _} _%E.
-Arguments empty_ectx {_ _ _ _ _}.
-Arguments comp_ectx {_ _ _ _ _} _ _.
-Arguments fill {_ _ _ _ _} _ _%E.
-Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
-
-Arguments to_of_val {_ _ _ _ _} _.
-Arguments of_to_val {_ _ _ _ _} _ _ _.
-Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
-Arguments fill_empty {_ _ _ _ _} _.
-Arguments fill_comp {_ _ _ _ _} _ _ _.
-Arguments fill_not_val {_ _ _ _ _} _ _ _.
-Arguments ectx_positive {_ _ _ _ _} _ _ _.
-Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
+Arguments EctxLanguage {_ _ _ _ _ _ _ _ _ _} _.
+Arguments of_val {_} _%V.
+Arguments to_val {_} _%E.
+Arguments empty_ectx {_}.
+Arguments comp_ectx {_} _ _.
+Arguments fill {_} _ _%E.
+Arguments head_step {_} _%E _ _%E _ _.
(* From an ectx_language, we can construct a language. *)
Section ectx_language.
- Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
- Implicit Types (e : expr) (K : ectx).
+ Context {Λ : ectxLanguage}.
+ Implicit Types v : val Λ.
+ Implicit Types e : expr Λ.
+ Implicit Types K : ectx Λ.
+
+ (* Only project stuff out of the mixin that is not also in language *)
+ Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None.
+ Proof. apply ectx_language_mixin. Qed.
+ Lemma fill_empty e : fill empty_ectx e = e.
+ Proof. apply ectx_language_mixin. Qed.
+ Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
+ Proof. apply ectx_language_mixin. Qed.
+ Global Instance fill_inj K : Inj (=) (=) (fill K).
+ Proof. apply ectx_language_mixin. Qed.
+ Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+ Proof. apply ectx_language_mixin. Qed.
+ Lemma ectx_positive K1 K2 :
+ comp_ectx K1 K2 = empty_ectx → K1 = empty_ectx ∧ K2 = empty_ectx.
+ Proof. apply ectx_language_mixin. Qed.
+ Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
+ fill K e1 = fill K' e1' →
+ to_val e1 = None →
+ head_step e1' σ1 e2 σ2 efs →
+ ∃ K'', K' = comp_ectx K K''.
+ Proof. apply ectx_language_mixin. Qed.
- Definition head_reducible (e : expr) (σ : state) :=
+ Definition head_reducible (e : expr Λ) (σ : state Λ) :=
∃ e' σ' efs, head_step e σ e' σ' efs.
- Definition head_irreducible (e : expr) (σ : state) :=
+ Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
∀ e' σ' efs, ¬head_step e σ e' σ' efs.
- Definition head_progressive (e : expr) (σ : state) :=
+ Definition head_progressive (e : expr Λ) (σ : state Λ) :=
is_Some(to_val e) ∨ ∃ K e', e = fill K e' ∧ head_reducible e' σ.
(* All non-value redexes are at the root. In other words, all sub-redexes are
values. *)
- Definition sub_redexes_are_values (e : expr) :=
+ Definition sub_redexes_are_values (e : expr Λ) :=
∀ K e', e = fill K e' → to_val e' = None → K = empty_ectx.
- Inductive prim_step (e1 : expr) (σ1 : state)
- (e2 : expr) (σ2 : state) (efs : list expr) : Prop :=
+ Inductive prim_step (e1 : expr Λ) (σ1 : state Λ)
+ (e2 : expr Λ) (σ2 : state Λ) (efs : list (expr Λ)) : Prop :=
Ectx_step K e1' e2' :
e1 = fill K e1' → e2 = fill K e2' →
head_step e1' σ1 e2' σ2 efs → prim_step e1 σ1 e2 σ2 efs.
@@ -79,24 +118,26 @@ Section ectx_language.
head_step e1 σ1 e2 σ2 efs → prim_step (fill K e1) σ1 (fill K e2) σ2 efs.
Proof. econstructor; eauto. Qed.
- Lemma val_prim_stuck e1 σ1 e2 σ2 efs :
- prim_step e1 σ1 e2 σ2 efs → to_val e1 = None.
- Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_stuck. Qed.
+ Definition ectx_lang_mixin : LanguageMixin of_val to_val prim_step.
+ Proof.
+ split.
+ - apply ectx_language_mixin.
+ - apply ectx_language_mixin.
+ - intros ????? [??? -> -> ?%val_head_stuck].
+ apply eq_None_not_Some. by intros ?%fill_val%eq_None_not_Some.
+ Qed.
- Canonical Structure ectx_lang : language := {|
- language.expr := expr; language.val := val; language.state := state;
- language.of_val := of_val; language.to_val := to_val;
- language.prim_step := prim_step;
- language.to_of_val := to_of_val; language.of_to_val := of_to_val;
- language.val_stuck := val_prim_stuck;
- |}.
+ Canonical Structure ectx_lang : language := Language ectx_lang_mixin.
- Class HeadAtomic (s : stuckness) (e : expr) : Prop :=
+ Class HeadAtomic (s : stuckness) (e : expr Λ) : Prop :=
head_atomic σ e' σ' efs :
head_step e σ e' σ' efs →
if s is not_stuck then irreducible e' σ' else is_Some (to_val e').
(* Some lemmas about this language *)
+ Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
+ Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
+
Lemma head_prim_step e1 σ1 e2 σ2 efs :
head_step e1 σ1 e2 σ2 efs → prim_step e1 σ1 e2 σ2 efs.
Proof. apply Ectx_step with empty_ectx; by rewrite ?fill_empty. Qed.
@@ -115,7 +156,7 @@ Section ectx_language.
reducible e σ → sub_redexes_are_values e → head_reducible e σ.
Proof.
intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
- assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+ assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
rewrite fill_empty /head_reducible; eauto.
Qed.
Lemma prim_head_irreducible e σ :
@@ -136,7 +177,7 @@ Section ectx_language.
HeadAtomic s e → sub_redexes_are_values e → Atomic s e.
Proof.
intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
- assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
+ assert (K = empty_ectx) as -> by eauto 10 using val_head_stuck.
rewrite fill_empty. eapply Hatomic_step. by rewrite fill_empty.
Qed.
@@ -148,14 +189,14 @@ Section ectx_language.
intros (e2''&σ2''&efs''&?) [K e1' e2' -> -> Hstep].
destruct (step_by_val K empty_ectx e1' (fill K e1') σ1 e2'' σ2'' efs'')
as [K' [-> _]%symmetry%ectx_positive];
- eauto using fill_empty, fill_not_val, val_stuck.
+ eauto using fill_empty, fill_not_val, val_head_stuck.
by rewrite !fill_empty.
Qed.
(* Every evaluation context is a context. *)
- Global Instance ectx_lang_ctx K : LanguageCtx ectx_lang (fill K).
+ Global Instance ectx_lang_ctx K : LanguageCtx (fill K).
Proof.
- split.
+ split; simpl.
- eauto using fill_not_val.
- intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
by exists (comp_ectx K K') e1' e2'; rewrite ?Heq1 ?Heq2 ?fill_comp.
@@ -177,6 +218,18 @@ Section ectx_language.
eexists e2', σ2, efs. by apply head_prim_step.
- intros σ1 e2' σ2 efs ? ?%head_reducible_prim_step; eauto.
Qed.
+
+ Global Instance pure_exec_fill K e1 e2 φ :
+ PureExec φ e1 e2 →
+ PureExec φ (fill K e1) (fill K e2).
+ Proof. apply: pure_exec_ctx. Qed.
+
End ectx_language.
-Arguments ectx_lang _ {_ _ _ _}.
+Arguments ectx_lang : clear implicits.
+Coercion ectx_lang : ectxLanguage >-> language.
+
+Definition LanguageOfEctx (Λ : ectxLanguage) : language :=
+ let '@EctxLanguage E V C St of_val to_val empty comp fill head mix := Λ in
+ @Language E V St of_val to_val _
+ (@ectx_lang_mixin (@EctxLanguage E V C St of_val to_val empty comp fill head mix)).
diff --git a/theories/program_logic/ectx_lifting.v b/theories/program_logic/ectx_lifting.v
index a3d0cb7684708402507ad5f82bf25013445236ee..459b467c402e342a95b2ab287cc8135da95c94d1 100644
--- a/theories/program_logic/ectx_lifting.v
+++ b/theories/program_logic/ectx_lifting.v
@@ -4,27 +4,16 @@ From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section wp.
-Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
-Implicit Types Φ : val → iProp Σ.
-Implicit Types v : val.
-Implicit Types e : expr.
+Implicit Types Φ : val Λ → iProp Σ.
+Implicit Types v : val Λ.
+Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve progressive_head_progressive.
-Lemma wp_ectx_bind {s E e} K Φ :
- WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}
- ⊢ WP fill K e @ s; E {{ Φ }}.
-Proof. apply: weakestpre.wp_bind. Qed.
-
-Lemma wp_ectx_bind_inv {s E Φ} K e :
- WP fill K e @ s; E {{ Φ }}
- ⊢ WP e @ s; E {{ v, WP fill K (of_val v) @ s; E {{ Φ }} }}.
-Proof. apply: weakestpre.wp_bind_inv. Qed.
-
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None →
(∀ σ1, state_interp σ1 ={E,∅}=∗
diff --git a/theories/program_logic/ectxi_language.v b/theories/program_logic/ectxi_language.v
index 0e6d4f2e0fb763c03fd9c81224178bfc33888eea..bd73dfc65c8b23534a1d6f6d551d08603850a561 100644
--- a/theories/program_logic/ectxi_language.v
+++ b/theories/program_logic/ectxi_language.v
@@ -4,92 +4,130 @@ From iris.algebra Require Export base.
From iris.program_logic Require Import language ectx_language.
Set Default Proof Using "Type".
-(* We need to make those arguments indices that we want canonical structure
- inference to use a keys. *)
-Class EctxiLanguage (expr val ectx_item state : Type) := {
+(* TAKE CARE: When you define an [ectxiLanguage] canonical structure for your
+language, you need to also define a corresponding [language] and [ectxLanguage]
+canonical structure for canonical structure inference to work properly. You
+should use the coercion [EctxLanguageOfEctxi] and [LanguageOfEctx] for that, and
+not [ectxi_lang] and [ectxi_lang_ectx], otherwise the canonical projections will
+not point to the right terms.
+
+A full concrete example of setting up your language can be found in [heap_lang].
+Below you can find the relevant parts:
+
+ Module heap_lang.
+ (* Your language definition *)
+
+ Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
+ Proof. (* ... *) Qed.
+ End heap_lang.
+
+ Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
+ Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
+ Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
+*)
+
+Section ectxi_language_mixin.
+ Context {expr val ectx_item state : Type}.
+ Context (of_val : val → expr).
+ Context (to_val : expr → option val).
+ Context (fill_item : ectx_item → expr → expr).
+ Context (head_step : expr → state → expr → state → list expr → Prop).
+
+ Record EctxiLanguageMixin := {
+ mixin_to_of_val v : to_val (of_val v) = Some v;
+ mixin_of_to_val e v : to_val e = Some v → of_val v = e;
+ mixin_val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
+
+ mixin_fill_item_inj Ki : Inj (=) (=) (fill_item Ki);
+ mixin_fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
+ mixin_fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+ to_val e1 = None → to_val e2 = None →
+ fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
+
+ mixin_head_ctx_step_val Ki e σ1 e2 σ2 efs :
+ head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
+ }.
+End ectxi_language_mixin.
+
+Structure ectxiLanguage := EctxiLanguage {
+ expr : Type;
+ val : Type;
+ ectx_item : Type;
+ state : Type;
+
of_val : val → expr;
to_val : expr → option val;
fill_item : ectx_item → expr → expr;
head_step : expr → state → expr → state → list expr → Prop;
- to_of_val v : to_val (of_val v) = Some v;
- of_to_val e v : to_val e = Some v → of_val v = e;
- val_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs → to_val e1 = None;
-
- fill_item_inj Ki :> Inj (=) (=) (fill_item Ki);
- fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e);
- fill_item_no_val_inj Ki1 Ki2 e1 e2 :
- to_val e1 = None → to_val e2 = None →
- fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2;
-
- head_ctx_step_val Ki e σ1 e2 σ2 efs :
- head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e);
+ ectxi_language_mixin :
+ EctxiLanguageMixin of_val to_val fill_item head_step
}.
-Arguments of_val {_ _ _ _ _} _%V.
-Arguments to_val {_ _ _ _ _} _%E.
-Arguments fill_item {_ _ _ _ _} _ _%E.
-Arguments head_step {_ _ _ _ _} _%E _ _%E _ _.
-
-Arguments to_of_val {_ _ _ _ _} _.
-Arguments of_to_val {_ _ _ _ _} _ _ _.
-Arguments val_stuck {_ _ _ _ _} _ _ _ _ _ _.
-Arguments fill_item_val {_ _ _ _ _} _ _ _.
-Arguments fill_item_no_val_inj {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments head_ctx_step_val {_ _ _ _ _} _ _ _ _ _ _ _.
-Arguments step_by_val {_ _ _ _ _} _ _ _ _ _ _ _ _ _ _ _.
+Arguments EctxiLanguage {_ _ _ _ _ _ _ _} _.
+Arguments of_val {_} _%V.
+Arguments to_val {_} _%E.
+Arguments fill_item {_} _ _%E.
+Arguments head_step {_} _%E _ _%E _ _.
Section ectxi_language.
- Context {expr val ectx_item state}
- {Λ : EctxiLanguage expr val ectx_item state}.
- Implicit Types (e : expr) (Ki : ectx_item).
- Notation ectx := (list ectx_item).
+ Context {Λ : ectxiLanguage}.
+ Implicit Types (e : expr Λ) (Ki : ectx_item Λ).
+ Notation ectx := (list (ectx_item Λ)).
+
+ (* Only project stuff out of the mixin that is not also in ectxLanguage *)
+ Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+ Proof. apply ectxi_language_mixin. Qed.
+ Lemma fill_item_val Ki e : is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
+ Proof. apply ectxi_language_mixin. Qed.
+ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
+ to_val e1 = None → to_val e2 = None →
+ fill_item Ki1 e1 = fill_item Ki2 e2 → Ki1 = Ki2.
+ Proof. apply ectxi_language_mixin. Qed.
+ Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
+ head_step (fill_item Ki e) σ1 e2 σ2 efs → is_Some (to_val e).
+ Proof. apply ectxi_language_mixin. Qed.
- Definition fill (K : ectx) (e : expr) : expr := foldl (flip fill_item) e K.
+ Definition fill (K : ectx) (e : expr Λ) : expr Λ := foldl (flip fill_item) e K.
Lemma fill_app (K1 K2 : ectx) e : fill (K1 ++ K2) e = fill K2 (fill K1 e).
Proof. apply foldl_app. Qed.
- Instance fill_inj K : Inj (=) (=) (fill K).
- Proof. induction K as [|Ki K IH]; rewrite /Inj; naive_solver. Qed.
-
- Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
+ Definition ectxi_lang_ectx_mixin :
+ EctxLanguageMixin of_val to_val [] (flip (++)) fill head_step.
Proof.
- revert e.
- induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val.
+ assert (fill_val : ∀ K e, is_Some (to_val (fill K e)) → is_Some (to_val e)).
+ { intros K. induction K as [|Ki K IH]=> e //=. by intros ?%IH%fill_item_val. }
+ assert (fill_not_val : ∀ K e, to_val e = None → to_val (fill K e) = None).
+ { intros K e. rewrite !eq_None_not_Some. eauto. }
+ split.
+ - apply ectxi_language_mixin.
+ - apply ectxi_language_mixin.
+ - apply ectxi_language_mixin.
+ - done.
+ - intros K1 K2 e. by rewrite /fill /= foldl_app.
+ - intros K; induction K as [|Ki K IH]; rewrite /Inj; naive_solver.
+ - done.
+ - by intros [] [].
+ - intros K K' e1 e1' σ1 e2 σ2 efs Hfill Hred Hstep; revert K' Hfill.
+ induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
+ destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
+ { rewrite fill_app in Hstep. apply head_ctx_step_val in Hstep.
+ apply fill_val in Hstep. by apply not_eq_None_Some in Hstep. }
+ rewrite !fill_app /= in Hfill.
+ assert (Ki = Ki') as ->.
+ { eapply fill_item_no_val_inj, Hfill; eauto using val_head_stuck.
+ apply fill_not_val. revert Hstep. apply ectxi_language_mixin. }
+ simplify_eq. destruct (IH K') as [K'' ->]; auto.
+ exists K''. by rewrite assoc.
Qed.
+ Canonical Structure ectxi_lang_ectx := EctxLanguage ectxi_lang_ectx_mixin.
+ Canonical Structure ectxi_lang := LanguageOfEctx ectxi_lang_ectx.
+
Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some. eauto using fill_val. Qed.
- (* When something does a step, and another decomposition of the same expression
- has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
- other words, [e] also contains the reducible expression *)
- Lemma step_by_val K K' e1 e1' σ1 e2 σ2 efs :
- fill K e1 = fill K' e1' → to_val e1 = None → head_step e1' σ1 e2 σ2 efs →
- exists K'', K' = K'' ++ K. (* K `prefix_of` K' *)
- Proof.
- intros Hfill Hred Hstep; revert K' Hfill.
- induction K as [|Ki K IH] using rev_ind=> /= K' Hfill; eauto using app_nil_r.
- destruct K' as [|Ki' K' _] using @rev_ind; simplify_eq/=.
- { rewrite fill_app in Hstep.
- exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
- eauto using fill_not_val, head_ctx_step_val. }
- rewrite !fill_app /= in Hfill.
- assert (Ki = Ki') as ->
- by eauto using fill_item_no_val_inj, val_stuck, fill_not_val.
- simplify_eq. destruct (IH K') as [K'' ->]; auto.
- exists K''. by rewrite assoc.
- Qed.
-
- Global Program Instance ectxi_lang_ectx : EctxLanguage expr val ectx state := {|
- ectx_language.of_val := of_val; ectx_language.to_val := to_val;
- empty_ectx := []; comp_ectx := flip (++); ectx_language.fill := fill;
- ectx_language.head_step := head_step |}.
- Solve Obligations with simpl; eauto using to_of_val, of_to_val, val_stuck,
- fill_not_val, fill_app, step_by_val, foldl_app.
- Next Obligation. intros K1 K2 ?%app_eq_nil; tauto. Qed.
-
Lemma ectxi_language_sub_redexes_are_values e :
(∀ Ki e', e = fill_item Ki e' → is_Some (to_val e')) →
sub_redexes_are_values e.
@@ -98,9 +136,17 @@ Section ectxi_language.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
Qed.
- Global Instance ectxi_lang_ctx_item Ki :
- LanguageCtx (ectx_lang expr) (fill_item Ki).
- Proof. change (LanguageCtx _ (fill [Ki])). apply _. Qed.
+ Global Instance ectxi_lang_ctx_item Ki : LanguageCtx (fill_item Ki).
+ Proof. change (LanguageCtx (fill [Ki])). apply _. Qed.
End ectxi_language.
-Arguments fill {_ _ _ _ _} _ _%E.
+Arguments fill {_} _ _%E.
+Arguments ectxi_lang_ectx : clear implicits.
+Arguments ectxi_lang : clear implicits.
+Coercion ectxi_lang_ectx : ectxiLanguage >-> ectxLanguage.
+Coercion ectxi_lang : ectxiLanguage >-> language.
+
+Definition EctxLanguageOfEctxi (Λ : ectxiLanguage) : ectxLanguage :=
+ let '@EctxiLanguage E V C St of_val to_val fill head mix := Λ in
+ @EctxLanguage E V (list C) St of_val to_val _ _ _ _
+ (@ectxi_lang_ectx_mixin (@EctxiLanguage E V C St of_val to_val fill head mix)).
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 629e50a993d4cd04a9e1de83e0212d9454ae6e90..3b4142dc55f6438d22488255f3491b5c0dc6e626 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -10,35 +10,35 @@ Instance: Params (@ht) 5.
Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e @ s ; E {{ Φ } }") : C_scope.
+ format "{{ P } } e @ s ; E {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e @ E {{ Φ } }") : C_scope.
+ format "{{ P } } e @ E {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht maybe_stuck E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e @ E ? {{ Φ } }") : C_scope.
+ format "{{ P } } e @ E ? {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e {{ Φ } }" := (ht not_stuck ⊤ P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e {{ Φ } }") : C_scope.
+ format "{{ P } } e {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck ⊤ P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
- format "{{ P } } e ? {{ Φ } }") : C_scope.
+ format "{{ P } } e ? {{ Φ } }") : stdpp_scope.
Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e @ s ; E {{ v , Q } }") : C_scope.
+ format "{{ P } } e @ s ; E {{ v , Q } }") : stdpp_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e @ E {{ v , Q } }") : C_scope.
+ format "{{ P } } e @ E {{ v , Q } }") : stdpp_scope.
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht maybe_stuck E P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e @ E ? {{ v , Q } }") : C_scope.
+ format "{{ P } } e @ E ? {{ v , Q } }") : stdpp_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht not_stuck ⊤ P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e {{ v , Q } }") : C_scope.
+ format "{{ P } } e {{ v , Q } }") : stdpp_scope.
Notation "{{ P } } e ? {{ v , Q } }" := (ht maybe_stuck ⊤ P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
- format "{{ P } } e ? {{ v , Q } }") : C_scope.
+ format "{{ P } } e ? {{ v , Q } }") : stdpp_scope.
Section hoare.
Context `{irisG Λ Σ}.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 0d2f2bbbfec98d8b63313d0b22170d2403590fb8..2d15d536ae91d4da5584c3c1ea7f45af3ff463e4 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -1,6 +1,19 @@
From iris.algebra Require Export ofe.
Set Default Proof Using "Type".
+Section language_mixin.
+ Context {expr val state : Type}.
+ Context (of_val : val → expr).
+ Context (to_val : expr → option val).
+ Context (prim_step : expr → state → expr → state → list expr → Prop).
+
+ Record LanguageMixin := {
+ mixin_to_of_val v : to_val (of_val v) = Some v;
+ mixin_of_to_val e v : to_val e = Some v → of_val v = e;
+ mixin_val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
+ }.
+End language_mixin.
+
Structure language := Language {
expr : Type;
val : Type;
@@ -8,20 +21,17 @@ Structure language := Language {
of_val : val → expr;
to_val : expr → option val;
prim_step : expr → state → expr → state → list expr → Prop;
- to_of_val v : to_val (of_val v) = Some v;
- of_to_val e v : to_val e = Some v → of_val v = e;
- val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
+ language_mixin : LanguageMixin of_val to_val prim_step
}.
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
Bind Scope expr_scope with expr.
Bind Scope val_scope with val.
+
+Arguments Language {_ _ _ _ _ _} _.
Arguments of_val {_} _.
Arguments to_val {_} _.
Arguments prim_step {_} _ _ _ _ _.
-Arguments to_of_val {_} _.
-Arguments of_to_val {_} _ _ _.
-Arguments val_stuck {_} _ _ _ _ _ _.
Canonical Structure stateC Λ := leibnizC (state Λ).
Canonical Structure valC Λ := leibnizC (val Λ).
@@ -29,7 +39,7 @@ Canonical Structure exprC Λ := leibnizC (expr Λ).
Definition cfg (Λ : language) := (list (expr Λ) * state Λ)%type.
-Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
+Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
fill_not_val e :
to_val e = None → to_val (K e) = None;
fill_step e1 σ1 e2 σ2 efs :
@@ -40,7 +50,7 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
∃ e2', e2 = K e2' ∧ prim_step e1' σ1 e2' σ2 efs
}.
-Instance language_ctx_id Λ : LanguageCtx Λ id.
+Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
Proof. constructor; naive_solver. Qed.
Variant stuckness := not_stuck | maybe_stuck.
@@ -60,6 +70,14 @@ Infix "≤" := stuckness_le : stuckness_scope.
Section language.
Context {Λ : language}.
Implicit Types v : val Λ.
+ Implicit Types e : expr Λ.
+
+ Lemma to_of_val v : to_val (of_val v) = Some v.
+ Proof. apply language_mixin. Qed.
+ Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+ Proof. apply language_mixin. Qed.
+ Lemma val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None.
+ Proof. apply language_mixin. Qed.
Definition reducible (e : expr Λ) (σ : state Λ) :=
∃ e' σ' efs, prim_step e σ e' σ' efs.
@@ -138,6 +156,19 @@ Section language.
PureExec P e1 e2.
Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
+ (* We do not make this an instance because it is awfully general. *)
+ Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
+ PureExec φ e1 e2 →
+ PureExec φ (K e1) (K e2).
+ Proof.
+ intros [Hred Hstep]. split.
+ - unfold reducible in *. naive_solver eauto using fill_step.
+ - intros σ1 e2' σ2 efs ? Hpstep.
+ destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+ + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
+ + edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
+ Qed.
+
(* This is a family of frequent assumptions for PureExec *)
Class IntoVal (e : expr Λ) (v : val Λ) :=
into_val : to_val e = Some v.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index a7c51e14eaeb3c3d53b11f40b21ac72bb55e2e95..a63cb53f3ba3966d42bde7610d187f7429284bf2 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -195,11 +195,10 @@ End lifting.
Section ectx_lifting.
Import ectx_language.
- Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
- Context `{ownPG (ectx_lang expr) Σ} {Hinh : Inhabited state}.
+ Context {Λ : ectxLanguage} `{ownPG Λ Σ} {Hinh : Inhabited (state Λ)}.
Implicit Types s : stuckness.
- Implicit Types Φ : val → iProp Σ.
- Implicit Types e : expr.
+ Implicit Types Φ : val Λ → iProp Σ.
+ Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve progressive_head_progressive.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index efa2340a5475f048539124eeae5843d63a719283..a10f6027558550cca9eba4c2681f723efa7136ed 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -121,47 +121,47 @@ Notation "'{{{' P } } } e @ s ; E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ s; E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ s ; E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e @ E ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e {{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ x .. y , 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _,
P -∗ ▷ (∀ x, .. (∀ y, Q -∗ Φ pat%V) .. ) -∗ WP e ?{{ Φ }})
(at level 20, x closed binder, y closed binder,
- format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e ? {{{ x .. y , RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ s ; E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ s; E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ s ; E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E {{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e @ E ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e @ E ?{{ Φ }})
(at level 20,
- format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e @ E ? {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e {{ Φ }})
(at level 20,
- format "{{{ P } } } e {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e {{{ RET pat ; Q } } }") : stdpp_scope.
Notation "'{{{' P } } } e ? {{{ 'RET' pat ; Q } } }" :=
(∀ Φ : _ → uPred _, P -∗ ▷ (Q -∗ Φ pat%V) -∗ WP e ?{{ Φ }})
(at level 20,
- format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : C_scope.
+ format "{{{ P } } } e ? {{{ RET pat ; Q } } }") : stdpp_scope.
Section wp.
Context `{irisG Λ Σ}.
@@ -275,7 +275,7 @@ Proof.
iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Qed.
-Lemma wp_bind K `{!LanguageCtx Λ K} s E e Φ :
+Lemma wp_bind K `{!LanguageCtx K} s E e Φ :
WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }} ⊢ WP K e @ s; E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
@@ -291,7 +291,7 @@ Proof.
by iApply "IH".
Qed.
-Lemma wp_bind_inv K `{!LanguageCtx Λ K} s E e Φ :
+Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
WP K e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, WP K (of_val v) @ s; E {{ Φ }} }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 1e185e2cdf4d4b2852b6c2b4b043b47a538d128c..9497be34506b4e7f20a132cc2a9f892aeefffdbb 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -49,3 +49,41 @@ Qed.
Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
+
+Module Export ident.
+Inductive ident :=
+ | IAnon : positive → ident
+ | INamed :> string → ident.
+End ident.
+
+Instance maybe_IAnon : Maybe IAnon := λ i,
+ match i with IAnon n => Some n | _ => None end.
+Instance maybe_INamed : Maybe INamed := λ i,
+ match i with INamed s => Some s | _ => None end.
+
+Instance beq_eq_dec : EqDecision ident.
+Proof. solve_decision. Defined.
+
+Definition positive_beq := Eval compute in Pos.eqb.
+
+Lemma positive_beq_true x y : positive_beq x y = true ↔ x = y.
+Proof. apply Pos.eqb_eq. Qed.
+
+Definition ident_beq (i1 i2 : ident) : bool :=
+ match i1, i2 with
+ | IAnon n1, IAnon n2 => positive_beq n1 n2
+ | INamed s1, INamed s2 => string_beq s1 s2
+ | _, _ => false
+ end.
+
+Lemma ident_beq_true i1 i2 : ident_beq i1 i2 = true ↔ i1 = i2.
+Proof.
+ destruct i1, i2; rewrite /= ?string_beq_true ?positive_beq_true; naive_solver.
+Qed.
+
+Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
+Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
+
+Definition option_bind {A B} (f : A → option B) (mx : option A) : option B :=
+ match mx with Some x => f x | None => None end.
+Arguments option_bind _ _ _ !_ /.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5867734c7b2d6c798e0a155377dae77de6391042..a6729546dd29b3baf450cc0664a13ae4d7bda5b3 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,7 +1,6 @@
From iris.base_logic Require Export base_logic.
From iris.base_logic Require Import big_op tactics.
From iris.proofmode Require Export base environments classes.
-From stdpp Require Import stringmap hlist.
Set Default Proof Using "Type".
Import uPred.
Import env_notations.
@@ -36,42 +35,42 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
-Definition envs_dom {M} (Δ : envs M) : list string :=
+Definition envs_dom {M} (Δ : envs M) : list ident :=
env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
-Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
+Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
let (Γp,Γs) := Δ in
match env_lookup i Γp with
| Some P => Some (true, P) | None => P ↠env_lookup i Γs; Some (false, P)
end.
-Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
+Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
let (Γp,Γs) := Δ in
match p with
| true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
end.
-Definition envs_lookup_delete {M} (i : string)
+Definition envs_lookup_delete {M} (i : ident)
(Δ : envs M) : option (bool * uPred M * envs M) :=
let (Γp,Γs) := Δ in
match env_lookup_delete i Γp with
| Some (P,Γp') => Some (true, P, Envs Γp' Γs)
- | None => '(P,Γs') ↠env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
+ | None => ''(P,Γs') ↠env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
end.
-Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
+Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
(Δ : envs M) : option (bool * list (uPred M) * envs M) :=
match js with
| [] => Some (true, [], Δ)
| j :: js =>
- '(p,P,Δ') ↠envs_lookup_delete j Δ;
- let Δ' := if p then (if remove_persistent then Δ' else Δ) else Δ' in
- '(q,Hs,Δ'') ↠envs_lookup_delete_list js remove_persistent Δ';
+ ''(p,P,Δ') ↠envs_lookup_delete j Δ;
+ let Δ' := if p : bool then (if remove_persistent then Δ' else Δ) else Δ' in
+ ''(q,Hs,Δ'') ↠envs_lookup_delete_list js remove_persistent Δ';
Some (p && q, P :: Hs, Δ'')
end.
Definition envs_snoc {M} (Δ : envs M)
- (p : bool) (j : string) (P : uPred M) : envs M :=
+ (p : bool) (j : ident) (P : uPred M) : envs M :=
let (Γp,Γs) := Δ in
if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
@@ -83,7 +82,7 @@ Definition envs_app {M} (p : bool)
| false => _ ↠env_app Γ Γp; Γs' ↠env_app Γ Γs; Some (Envs Γp Γs')
end.
-Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
+Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
(Δ : envs M) : option (envs M) :=
let (Γp,Γs) := Δ in
match p with
@@ -91,7 +90,7 @@ Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
| false => _ ↠env_app Γ Γp; Γs' ↠env_replace i Γ Γs; Some (Envs Γp Γs')
end.
-Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
+Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
(Δ : envs M) : option (envs M) :=
if eqb p q then envs_simple_replace i p Γ Δ
else envs_app q Γ (envs_delete i p Δ).
@@ -106,19 +105,19 @@ Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
Envs Enil (env_spatial Δ).
Fixpoint envs_split_go {M}
- (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
+ (js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
match js with
| [] => Some (Δ1, Δ2)
| j :: js =>
- '(p,P,Δ1') ↠envs_lookup_delete j Δ1;
- if p then envs_split_go js Δ1 Δ2 else
+ ''(p,P,Δ1') ↠envs_lookup_delete j Δ1;
+ if p : bool then envs_split_go js Δ1 Δ2 else
envs_split_go js Δ1' (envs_snoc Δ2 false j P)
end.
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {M} (d : direction)
- (js : list string) (Δ : envs M) : option (envs M * envs M) :=
- '(Δ1,Δ2) ↠envs_split_go js Δ (envs_clear_spatial Δ);
+ (js : list ident) (Δ : envs M) : option (envs M * envs M) :=
+ ''(Δ1,Δ2) ↠envs_split_go js Δ (envs_clear_spatial Δ);
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
(* Coq versions of the tactics *)
@@ -224,11 +223,11 @@ Proof.
apply wand_intro_l; destruct p; simpl.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
- intros j; destruct (string_beq_reflect j i); naive_solver.
+ intros j; destruct (ident_beq_reflect j i); naive_solver.
+ by rewrite persistently_sep assoc.
- apply sep_intro_True_l; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
- intros j; destruct (string_beq_reflect j i); naive_solver.
+ intros j; destruct (ident_beq_reflect j i); naive_solver.
+ solve_sep_entails.
Qed.
@@ -298,7 +297,7 @@ Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
Lemma envs_lookup_envs_clear_spatial Δ j :
envs_lookup j (envs_clear_spatial Δ)
- = '(p,P) ↠envs_lookup j Δ; if p then Some (p,P) else None.
+ = ''(p,P) ↠envs_lookup j Δ; if p : bool then Some (p,P) else None.
Proof.
rewrite /envs_lookup /envs_clear_spatial.
destruct Δ as [Γp Γs]; simpl; destruct (Γp !! j) eqn:?; simplify_eq/=; auto.
@@ -362,7 +361,7 @@ Proof.
destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
apply envs_split_go_sound in HΔ as ->; last first.
{ intros j P. by rewrite envs_lookup_envs_clear_spatial=> ->. }
- destruct d; simplify_eq; solve_sep_entails.
+ destruct d; simplify_eq/=; solve_sep_entails.
Qed.
Global Instance envs_Forall2_refl (R : relation (uPred M)) :
@@ -641,7 +640,7 @@ Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
IntoWand false R P1 P2 → ElimModal P1' P1 Q Q →
- ('(Δ1,Δ2) ↠envs_split (if neg is true then Right else Left) js Δ';
+ (''(Δ1,Δ2) ↠envs_split (if neg is true then Right else Left) js Δ';
Δ2' ↠envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 5236e5e0966557afc25087ebfa81a07a0e1c26eb..d980e776fed0384f999a229883869dceb507f82d 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,29 +1,25 @@
-From stdpp Require Export strings.
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
-From stdpp Require Import stringmap.
Set Default Proof Using "Type".
Inductive env (A : Type) : Type :=
| Enil : env A
- | Esnoc : env A → string → A → env A.
+ | Esnoc : env A → ident → A → env A.
Arguments Enil {_}.
-Arguments Esnoc {_} _ _%string _.
+Arguments Esnoc {_} _ _ _.
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
-Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
+Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
match Γ with
| Enil => None
- | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
+ | Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
end.
Module env_notations.
- Notation "x ↠y ; z" := (match y with Some x => z | None => None end).
- Notation "' ( x1 , x2 ) ↠y ; z" :=
- (match y with Some (x1,x2) => z | None => None end).
- Notation "' ( x1 , x2 , x3 ) ↠y ; z" :=
- (match y with Some (x1,x2,x3) => z | None => None end).
+ Notation "y ≫= f" := (option_bind f y).
+ Notation "x ↠y ; z" := (y ≫= λ x, z).
+ Notation "' x1 .. xn ↠y ; z" := (y ≫= (λ x1, .. (λ xn, z) .. )).
Notation "Γ !! j" := (env_lookup j Γ).
End env_notations.
Import env_notations.
@@ -37,7 +33,7 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
Coercion env_to_list : env >-> list.
Instance: Params (@env_to_list) 1.
-Fixpoint env_dom {A} (Γ : env A) : list string :=
+Fixpoint env_dom {A} (Γ : env A) : list ident :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
@@ -48,29 +44,29 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
end.
-Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
+Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
- if string_beq i j then env_app Γi Γ else
+ if ident_beq i j then env_app Γi Γ else
match Γi !! j with
| None => Γ' ↠env_replace i Γi Γ; Some (Esnoc Γ' j x)
| Some _ => None
end
end.
-Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
+Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
match Γ with
| Enil => Enil
- | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
+ | Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
end.
-Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
+Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
- if string_beq i j then Some (x,Γ)
- else '(y,Γ') ↠env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
+ if ident_beq i j then Some (x,Γ)
+ else ''(y,Γ') ↠env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
end.
Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop :=
@@ -88,15 +84,17 @@ Inductive env_subenv {A} : relation (env A) :=
Section env.
Context {A : Type}.
Implicit Types Γ : env A.
-Implicit Types i : string.
+Implicit Types i : ident.
Implicit Types x : A.
Hint Resolve Esnoc_wf Enil_wf.
Ltac simplify :=
repeat match goal with
| _ => progress simplify_eq/=
- | H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
- | |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
+ | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
+ | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
+ | H : context [option_bind _ ?x] |- _ => destruct x eqn:?
+ | |- context [option_bind _ ?x] => destruct x eqn:?
| _ => case_match
end.
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index d36317e05e53835f8157b24c214dae57b9531f16..cc8feb04a746f5b61ad54dca1d413536c283167c 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tokens sel_patterns.
Set Default Proof Using "Type".
Inductive intro_pat :=
- | IName : string → intro_pat
+ | IIdent : ident → intro_pat
| IAnom : intro_pat
| IDrop : intro_pat
| IFrame : intro_pat
@@ -39,9 +39,9 @@ Fixpoint close_list (k : stack)
| SList :: k => Some (SPat (IList (ps :: pss)) :: k)
| SPat pat :: k => close_list k (pat :: ps) pss
| SAlwaysElim :: k =>
- '(p,ps) ↠maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
+ ''(p,ps) ↠maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
| SModalElim :: k =>
- '(p,ps) ↠maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
+ ''(p,ps) ↠maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
| SBar :: k => close_list k [] (ps :: pss)
| _ => None
end.
@@ -73,7 +73,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with
| [] => Some k
| TName "_" :: ts => parse_go ts (SPat IDrop :: k)
- | TName s :: ts => parse_go ts (SPat (IName s) :: k)
+ | TName s :: ts => parse_go ts (SPat (IIdent s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TBracketL :: ts => parse_go ts (SList :: k)
@@ -98,11 +98,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
end
with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
- | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
+ | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
| TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
- | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
+ | TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
| TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
@@ -114,8 +114,8 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
match k with
| [] => Some ps
| SPat pat :: k => close k (pat :: ps)
- | SAlwaysElim :: k => '(p,ps) ↠maybe2 (::) ps; close k (IAlwaysElim p :: ps)
- | SModalElim :: k => '(p,ps) ↠maybe2 (::) ps; close k (IModalElim p :: ps)
+ | SAlwaysElim :: k => ''(p,ps) ↠maybe2 (::) ps; close k (IAlwaysElim p :: ps)
+ | SModalElim :: k => ''(p,ps) ↠maybe2 (::) ps; close k (IModalElim p :: ps)
| _ => None
end.
@@ -134,6 +134,7 @@ Ltac parse s :=
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid list intro_pat" s
end
+ | ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X
end.
Ltac parse_one s :=
@@ -165,6 +166,7 @@ Ltac intro_pat_persistent p :=
| string =>
let pat := intro_pat.parse p in
eval cbv in (forallb intro_pat_persistent pat)
+ | ident => false
| bool => p
| ?X => fail "intro_pat_persistent:" p "has unexpected type" X
end.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index bf7dd0f005da2b6bea4c7c1a7636ae7573ac42d2..09722191074d25d98729684cf5380cb7bb6e4ab2 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -8,22 +8,25 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
Notation "" := Enil (only printing) : proof_scope.
-Notation "Γ H : P" := (Esnoc Γ H P)
+Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
+Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
+ (at level 1, P at level 200,
+ left associativity, format "Γ '_' : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
- C_scope.
+ stdpp_scope.
Notation "Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Enil Δ) Q%I)
(at level 1, Q at level 200, left associativity,
- format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
+ format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
Notation "Γ '--------------------------------------' □ Q" :=
(envs_entails (Envs Γ Enil) Q%I)
(at level 1, Q at level 200, left associativity,
- format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : C_scope.
+ format "Γ '--------------------------------------' □ '//' Q '//'", only printing) : stdpp_scope.
Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
- (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
+ (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : stdpp_scope.
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 6fa4129af1736a2e6473014339bb2f716d5f5522..6d7710d6e3aaf5442c9a425abe79681723dd2e01 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -6,7 +6,7 @@ Inductive sel_pat :=
| SelPure
| SelPersistent
| SelSpatial
- | SelName : string → sel_pat.
+ | SelIdent : ident → sel_pat.
Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
match ps with
@@ -19,7 +19,7 @@ Module sel_pat.
Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
match ts with
| [] => Some (reverse k)
- | TName s :: ts => parse_go ts (SelName s :: k)
+ | TName s :: ts => parse_go ts (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TAlways :: ts => parse_go ts (SelPersistent :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
@@ -32,7 +32,9 @@ Ltac parse s :=
lazymatch type of s with
| sel_pat => constr:([s])
| list sel_pat => s
- | list string => eval vm_compute in (SelName <$> s)
+ | ident => constr:([SelIdent s])
+ | list ident => eval vm_compute in (SelIdent <$> s)
+ | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 691ba64d586d36fd621abf7b1fa22b1fe374e97a..64201daf270d2f560a1a6356fe8682588c4e990a 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,5 +1,5 @@
From stdpp Require Export strings.
-From iris.proofmode Require Import tokens.
+From iris.proofmode Require Import base tokens.
Set Default Proof Using "Type".
Inductive goal_kind := GSpatial | GModal | GPersistent.
@@ -7,14 +7,14 @@ Inductive goal_kind := GSpatial | GModal | GPersistent.
Record spec_goal := SpecGoal {
spec_goal_kind : goal_kind;
spec_goal_negate : bool;
- spec_goal_frame : list string;
- spec_goal_hyps : list string;
+ spec_goal_frame : list ident;
+ spec_goal_hyps : list ident;
spec_goal_done : bool
}.
Inductive spec_pat :=
| SForall : spec_pat
- | SName : string → spec_pat
+ | SIdent : ident → spec_pat
| SPureGoal : bool → spec_pat
| SGoal : spec_goal → spec_pat
| SAutoFrame : goal_kind → spec_pat.
@@ -36,7 +36,7 @@ Inductive state :=
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
match ts with
| [] => Some (reverse k)
- | TName s :: ts => parse_go ts (SName s :: k)
+ | TName s :: ts => parse_go ts (SIdent s :: k)
| TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GPersistent :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
@@ -52,14 +52,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| _ => None
end
with parse_goal (ts : list token)
- (ki : goal_kind) (neg : bool) (frame hyps : list string)
+ (ki : goal_kind) (neg : bool) (frame hyps : list ident)
(k : list spec_pat) : option (list spec_pat) :=
match ts with
| TMinus :: ts =>
guard (¬neg ∧ frame = [] ∧ hyps = []);
parse_goal ts ki true frame hyps k
- | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
- | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
+ | TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
+ | TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
| TDone :: TBracketR :: ts =>
parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
| TBracketR :: ts =>
@@ -76,11 +76,4 @@ Ltac parse s :=
| Some ?pats => pats | _ => fail "invalid list spec_pat" s
end
end.
-Ltac parse_one s :=
- lazymatch type of s with
- | spec_pat => s
- | string => lazymatch eval vm_compute in (parse s) with
- | Some [?pat] => pat | _ => fail "invalid spec_pat" s
- end
- end.
End spec_pat.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 40277672d4a238e346fac91e236ce8e8c01349c1..36b2006c69cf4e84e586c22de6f0ae4b7bcf3f90 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -3,11 +3,13 @@ From iris.proofmode Require Import base intro_patterns spec_patterns sel_pattern
From iris.base_logic Require Export base_logic big_op.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
-From stdpp Require Import stringmap hlist.
+From stdpp Require Import hlist pretty.
Set Default Proof Using "Type".
+Export ident.
Declare Reduction env_cbv := cbv [
- beq ascii_beq string_beq
+ option_bind
+ beq ascii_beq string_beq positive_beq ident_beq
env_lookup env_lookup_delete env_delete env_app env_replace env_dom
env_persistent env_spatial env_spatial_is_nil envs_dom
envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
@@ -20,16 +22,19 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
(** * Misc *)
(* Tactic Notation tactics cannot return terms *)
-Ltac iFresh' H :=
+Ltac iFresh :=
lazymatch goal with
|- envs_entails ?Δ _ =>
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
- eval vm_compute in (fresh_string_of_set H (of_list Hs))
- | _ => H
+ eval vm_compute in
+ (IAnon (match Hs with
+ | [] => 1
+ | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
+ end))%positive
+ | _ => constr:(IAnon 1)
end.
-Ltac iFresh := iFresh' "~".
Ltac iMissingHyps Hs :=
let Δ :=
@@ -83,7 +88,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
Local Inductive esel_pat :=
| ESelPure
- | ESelName : bool → string → esel_pat.
+ | ESelIdent : bool → ident → esel_pat.
Ltac iElaborateSelPat pat :=
let rec go pat Δ Hs :=
@@ -93,14 +98,14 @@ Ltac iElaborateSelPat pat :=
| SelPersistent :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
- go pat Δ' ((ESelName true <$> Hs') ++ Hs)
+ go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
| SelSpatial :: ?pat =>
let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
- go pat Δ' ((ESelName false <$> Hs') ++ Hs)
- | SelName ?H :: ?pat =>
+ go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
+ | SelIdent ?H :: ?pat =>
lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
- | Some (?p,_,?Δ') => go pat Δ' (ESelName p H :: Hs)
+ | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
| None => fail "iElaborateSelPat:" H "not found"
end
end in
@@ -109,14 +114,16 @@ Ltac iElaborateSelPat pat :=
let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
end.
+Local Ltac iClearHyp H :=
+ eapply tac_clear with _ H _ _; (* (i:=H) *)
+ [env_reflexivity || fail "iClear:" H "not found"|].
+
Tactic Notation "iClear" constr(Hs) :=
let rec go Hs :=
lazymatch Hs with
| [] => idtac
| ESelPure :: ?Hs => clear; go Hs
- | ESelName _ ?H :: ?Hs =>
- eapply tac_clear with _ H _ _; (* (i:=H) *)
- [env_reflexivity || fail "iClear:" H "not found"|go Hs]
+ | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
end in
let Hs := iElaborateSelPat Hs in go Hs.
@@ -260,7 +267,7 @@ Tactic Notation "iFrame" constr(Hs) :=
| SelPure :: ?Hs => iFrameAnyPure; go Hs
| SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
| SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
- | SelName ?H :: ?Hs => iFrameHyp H; go Hs
+ | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
end
in let Hs := sel_pat.parse Hs in go Hs.
Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
@@ -406,7 +413,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
| SForall :: ?pats =>
idtac "the * specialization pattern is deprecated because it is applied implicitly";
go H1 pats
- | SName ?H2 :: ?pats =>
+ | SIdent ?H2 :: ?pats =>
eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
[env_reflexivity || fail "iSpecialize:" H2 "not found"
|env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -486,12 +493,17 @@ defaults to [false] (i.e. spatial hypotheses are not preserved). *)
Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
let p := intro_pat_persistent p in
let t :=
- match type of t with string => constr:(ITrm t hnil "") | _ => t end in
+ match type of t with
+ | string => constr:(ITrm (INamed t) hnil "")
+ | ident => constr:(ITrm t hnil "")
+ | _ => t
+ end in
lazymatch t with
| ITrm ?H ?xs ?pat =>
let pat := spec_pat.parse pat in
+ let H := lazymatch type of H with string => constr:(INamed H) | _ => H end in
lazymatch type of H with
- | string =>
+ | ident =>
(* The lemma [tac_specialize_persistent_helper] allows one to use all
spatial hypotheses for both proving the premises of the lemma we
specialize as well as those of the remaining goal. We can only use it when
@@ -553,8 +565,8 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
"as" constr(p) constr(lazy_tc) tactic(tac) :=
try iStartProof;
let Htmp := iFresh in
- let t :=
- lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
+ let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
+ let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
let spec_tac _ :=
lazymatch lem with
| ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
@@ -562,7 +574,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
end in
let go goal_tac :=
lazymatch type of t with
- | string =>
+ | ident =>
eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
[env_reflexivity || fail "iPoseProof:" t "not found"
|env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
@@ -618,7 +630,7 @@ Tactic Notation "iRevert" constr(Hs) :=
| ESelPure :: ?Hs =>
repeat match goal with x : _ |- _ => revert x end;
go Hs
- | ESelName _ ?H :: ?Hs =>
+ | ESelIdent _ ?H :: ?Hs =>
eapply tac_revert with _ H _ _; (* (i:=H2) *)
[env_reflexivity || fail "iRevert:" H "not found"
|env_cbv; go Hs]
@@ -705,6 +717,7 @@ Tactic Notation "iSplit" :=
Tactic Notation "iSplitL" constr(Hs) :=
iStartProof;
let Hs := words Hs in
+ let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
@@ -717,6 +730,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
Tactic Notation "iSplitR" constr(Hs) :=
iStartProof;
let Hs := words Hs in
+ let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
[apply _ ||
let P := match goal with |- FromAnd _ ?P _ _ => P end in
@@ -748,6 +762,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
+ let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_combine with _ _ Hs _ _ H _;
[env_reflexivity ||
let Hs := iMissingHyps Hs in
@@ -844,10 +859,14 @@ Tactic Notation "iModCore" constr(H) :=
Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let rec go Hz pat :=
lazymatch pat with
- | IAnom => idtac
- | IDrop => iClear Hz
- | IFrame => iFrame Hz
- | IName ?y => iRename Hz into y
+ | IAnom =>
+ lazymatch Hz with
+ | IAnon _ => idtac
+ | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
+ end
+ | IDrop => iClearHyp Hz
+ | IFrame => iFrameHyp Hz
+ | IIdent ?y => iRename Hz into y
| IList [[]] => iExFalso; iExact Hz
| IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
| IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
@@ -919,9 +938,9 @@ Tactic Notation "iIntros" constr(pat) :=
| [] => idtac
(* Optimizations to avoid generating fresh names *)
| IPureElim :: ?pats => iIntro (?); go pats
- | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
+ | IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; go pats
| IDrop :: ?pats => iIntro _; go pats
- | IName ?H :: ?pats => iIntro H; go pats
+ | IIdent ?H :: ?pats => iIntro H; go pats
(* Introduction patterns that can only occur at the top-level *)
| IPureIntro :: ?pats => iPureIntro; go pats
| IAlwaysIntro :: ?pats => iAlways; go pats
@@ -1153,10 +1172,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
- | ESelName ?p ?H :: ?Hs =>
+ | ESelIdent ?p ?H :: ?Hs =>
iRevert H; go Hs;
let H' :=
- match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
+ match p with true => constr:([IAlwaysElim (IIdent H)]) | false => H end in
iIntros H'
end in
try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
@@ -1226,14 +1245,17 @@ Instance copy_destruct_persistently {M} (P : uPred M) :
CopyDestruct P → CopyDestruct (□ P).
Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
- let hyp_name :=
+ let ident :=
lazymatch type of lem with
- | string => constr:(Some lem)
+ | ident => constr:(Some lem)
+ | string => constr:(Some (INamed lem))
| iTrm =>
lazymatch lem with
- | @iTrm string ?H _ _ => constr:(Some H) | _ => constr:(@None string)
+ | @iTrm ident ?H _ _ => constr:(Some H)
+ | @iTrm string ?H _ _ => constr:(Some (INamed H))
+ | _ => constr:(@None ident)
end
- | _ => constr:(@None string)
+ | _ => constr:(@None ident)
end in
let intro_destruct n :=
let rec go n' :=
@@ -1242,7 +1264,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
| 1 => repeat iIntroForall; let H := iFresh in iIntro H; tac H
| S ?n' => repeat iIntroForall; let H := iFresh in iIntro H; go n'
end in
- intros; iStartProof; go n in
+ intros; go n in
lazymatch type of lem with
| nat => intro_destruct lem
| Z => (* to make it work in Z_scope. We should just be able to bind
@@ -1253,7 +1275,8 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
Also, rule out cases in which it does not make sense to copy, namely when
destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
(which cannot be kept). *)
- lazymatch hyp_name with
+ iStartProof;
+ lazymatch ident with
| None => iPoseProofCore lem as p false tac
| Some ?H =>
lazymatch iTypeOf H with
@@ -1357,17 +1380,22 @@ result in the following actions:
- Introduce the proofmode hypotheses [Hs]
*)
Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
- let rec fix_ihs :=
+ let rec fix_ihs rev_tac :=
lazymatch goal with
| H : context [envs_entails _ _] |- _ =>
eapply (tac_revert_ih _ _ _ H _);
- [reflexivity
- || fail "iInduction: spatial context not empty, this should not happen"|];
- clear H; fix_ihs;
- let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
- | _ => idtac
+ [env_reflexivity
+ || fail "iInduction: spatial context not empty, this should not happen"
+ |clear H];
+ fix_ihs ltac:(fun j =>
+ let IH' := eval vm_compute in
+ match j with 0%N => IH | _ => IH +:+ pretty j end in
+ iIntros [IAlwaysElim (IIdent IH')];
+ let j := eval vm_compute in (1 + j)%N in
+ rev_tac j)
+ | _ => rev_tac 0%N
end in
- induction x as pat; fix_ihs.
+ induction x as pat; fix_ihs ltac:(fun _ => idtac).
Ltac iHypsContaining x :=
let rec go Γ x Hs :=
@@ -1381,7 +1409,7 @@ Ltac iHypsContaining x :=
end in
let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
- let Hs := go Γp x (@nil string) in go Γs x Hs.
+ let Hs := go Γp x (@nil ident) in go Γs x Hs.
Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
iRevertIntros Hs with (
@@ -1634,7 +1662,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
fail "iRewrite:" P "not an equality"
|iRewriteFindPred
- |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
+ |intros ??? ->; reflexivity|lazy beta; iClearHyp Heq]).
Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
@@ -1649,7 +1677,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
fail "iRewrite:" P "not an equality"
|iRewriteFindPred
|intros ??? ->; reflexivity
- |env_reflexivity|lazy beta; iClear Heq]).
+ |env_reflexivity|lazy beta; iClearHyp Heq]).
Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
iRewriteCore Right lem in H.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 748c1951233ad99fa745bd02b3176a30666f6ebd..b1cd8665d3aafe92c53bf0d5587d09d877d8478b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -30,7 +30,7 @@ Proof.
iRight.
iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
iPoseProof "Hc" as "foo".
- iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
+ iRevert (a b) "Ha Hb". iIntros (b a) "? {foo} Ha".
iAssert (uPred_ownM (a â‹… core a)) with "[Ha]" as "[Ha #Hac]".
{ by rewrite cmra_core_r. }
iIntros "{$Hac $Ha}".
@@ -98,7 +98,7 @@ Lemma test_very_fast_iIntros P :
Proof. by iIntros. Qed.
Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
-Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
+Proof. iIntros "[H [? _]]". by iFrame. Qed.
Lemma test_iFrame_pure (x y z : M) :
✓ x → ⌜y ≡ z⌠-∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
@@ -116,7 +116,7 @@ Qed.
Lemma test_iSpecialize_auto_frame P Q R :
(P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
-Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
+Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
(* Check coercions *)
Lemma test_iExist_coercion (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.
diff --git a/theories/tests/tree_sum.v b/theories/tests/tree_sum.v
index d4609d5bbef731404e2dfd227bd87c39e3a22fdc..28f75f6c8a26e77a3c6ceea613114910dac6c48e 100644
--- a/theories/tests/tree_sum.v
+++ b/theories/tests/tree_sum.v
@@ -40,8 +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Φ".
- iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
- destruct t as [n'|tl tr]; simpl in *.
+ iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]").
@@ -49,7 +48,7 @@ Proof.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
- wp_apply ("IH" with "Hl Htr"). iIntros "[Hl Htr]".
+ wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
iExists ll, lr, vl, vr. by iFrame.