Commit 1d9878b7 authored by David Swasey's avatar David Swasey
Browse files

Merge branch 'master' into swasey/progress2

parents 018cf38c 1262a001
......@@ -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
......
......@@ -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}
......
......@@ -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}
......
......@@ -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) \\
......
......@@ -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") }
]
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.
......@@ -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.
......
......@@ -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.
......
......@@ -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'.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......@@ -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.
......
......@@ -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.
......
......@@ -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 Σ}.
......
......@@ -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
......
......@@ -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.
......
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.
......@@ -16,10 +16,10 @@ Notation "P ={ E }=> Q" := (P ={E,E}=> Q)%I