Commit 388fadb9 authored by Ralf Jung's avatar Ralf Jung

use "inv" for the invariants in namespaces

parent 7f179d5b
Require Export algebra.base prelude.countable prelude.co_pset.
Require Export program_logic.ownership program_logic.pviewshifts.
Definition namespace := list positive.
Definition nnil : namespace := nil.
Definition ndot `{Countable A} (I : namespace) (x : A) : namespace :=
encode x :: I.
Definition nclose (I : namespace) : coPset := coPset_suffixes (encode I).
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
encode x :: N.
Definition nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Coercion nclose : namespace >-> coPset.
Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _).
Proof. by intros I1 x1 I2 x2 ?; simplify_equality. Qed.
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
Lemma encode_nclose I : encode I nclose I.
Lemma encode_nclose N : encode N nclose N.
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
Lemma nclose_subseteq `{Countable A} I x : nclose (ndot I x) nclose I.
Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) nclose N.
Proof.
intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
destruct (list_encode_suffix I (ndot I x)) as [q' ?]; [by exists [encode x]|].
destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal.
Qed.
Lemma ndot_nclose `{Countable A} I x : encode (ndot I x) nclose I.
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) nclose N.
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
Lemma nclose_disjoint `{Countable A} I (x y : A) :
x y nclose (ndot I x) nclose (ndot I y) = .
Lemma nclose_disjoint `{Countable A} N (x y : A) :
x y nclose (ndot N x) nclose (ndot N y) = .
Proof.
intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot.
rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
......@@ -30,4 +32,9 @@ Proof.
rewrite !(associative_L _) (injective_iff (++ _)%positive) /=.
generalize (encode_nat (encode y)).
induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
Qed.
\ No newline at end of file
Qed.
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
ownI (encode N) P.
(* TODO: Add lemmas about inv here. *)
Require Export program_logic.model.
Definition inv {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
uPred_own (Res {[ i to_agree (Later (iProp_unfold P)) ]} ).
Arguments inv {_ _} _ _%I.
Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := uPred_own (Res (Excl σ) ).
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_own (Res (Some m)).
Instance: Params (@inv) 3.
Instance: Params (@ownI) 3.
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Typeclasses Opaque inv ownG ownP.
Typeclasses Opaque ownI ownG ownP.
Section ownership.
Context {Λ : language} {Σ : iFunctor}.
......@@ -19,20 +19,20 @@ Implicit Types P : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
(* Invariants *)
Global Instance inv_contractive i : Contractive (@inv Λ Σ i).
Global Instance inv_contractive i : Contractive (@ownI Λ Σ i).
Proof.
intros n P Q HPQ.
apply (_: Proper (_ ==> _) iProp_unfold), Later_contractive in HPQ.
by unfold inv; rewrite HPQ.
by unfold ownI; rewrite HPQ.
Qed.
Lemma always_inv i P : ( inv i P)%I inv i P.
Lemma always_inv i P : ( ownI i P)%I ownI i P.
Proof.
apply uPred.always_own.
by rewrite Res_unit !cmra_unit_empty map_unit_singleton.
Qed.
Global Instance inv_always_stable i P : AlwaysStable (inv i P).
Global Instance inv_always_stable i P : AlwaysStable (ownI i P).
Proof. by rewrite /AlwaysStable always_inv. Qed.
Lemma inv_sep_dup i P : inv i P (inv i P inv i P)%I.
Lemma inv_sep_dup i P : ownI i P (ownI i P ownI i P)%I.
Proof. apply (uPred.always_sep_dup' _). Qed.
(* physical state *)
......@@ -65,7 +65,7 @@ Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *)
Lemma inv_spec r n i P :
{n} r
(inv i P) n r wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
(ownI i P) n r wld r !! i ={n}= Some (to_agree (Later (iProp_unfold P))).
Proof.
intros [??]; rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
* intros [(P'&Hi&HP) _]; rewrite Hi.
......
......@@ -78,7 +78,7 @@ Proof.
exists (r' r2); split; last by rewrite -(associative _).
exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto.
Qed.
Lemma pvs_open i P : inv i P pvs {[ i ]} ( P).
Lemma pvs_open i P : ownI i P pvs {[ i ]} ( P).
Proof.
intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia.
apply inv_spec in Hinv; last auto.
......@@ -87,7 +87,7 @@ Proof.
exists (rP r); split; last by rewrite (left_id_L _ _) -(associative _).
eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
Qed.
Lemma pvs_close i P : (inv i P P) pvs {[ i ]} True.
Lemma pvs_close i P : (ownI i P P) pvs {[ i ]} True.
Proof.
intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ; split; [done|].
rewrite (left_id _ _); apply wsat_close with P r.
......@@ -115,7 +115,7 @@ Proof.
auto using option_update_None. }
by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
Lemma pvs_alloc E P : ¬set_finite E P pvs E E ( i, (i E) inv i P).
Lemma pvs_alloc E P : ¬set_finite E P pvs E E ( i, (i E) ownI i P).
Proof.
intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
......
......@@ -72,16 +72,16 @@ Proof.
Qed.
Lemma vs_mask_frame' E Ef P Q : Ef E = P >{E}> Q P >{E Ef}> Q.
Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
Lemma vs_open i P : inv i P >{{[i]},}> P.
Lemma vs_open i P : ownI i P >{{[i]},}> P.
Proof. intros; apply vs_alt, pvs_open. Qed.
Lemma vs_open' E i P : i E inv i P >{{[i]} E,E}> P.
Lemma vs_open' E i P : i E ownI i P >{{[i]} E,E}> P.
Proof.
intros; rewrite -{2}(left_id_L () E) -vs_mask_frame; last solve_elem_of.
apply vs_open.
Qed.
Lemma vs_close i P : (inv i P P) >{,{[i]}}> True.
Lemma vs_close i P : (ownI i P P) >{,{[i]}}> True.
Proof. intros; apply vs_alt, pvs_close. Qed.
Lemma vs_close' E i P : i E (inv i P P) >{E,{[i]} E}> True.
Lemma vs_close' E i P : i E (ownI i P P) >{E,{[i]} E}> True.
Proof.
intros; rewrite -{1}(left_id_L () E) -vs_mask_frame; last solve_elem_of.
apply vs_close.
......@@ -95,6 +95,6 @@ Lemma vs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
Proof. by intros; apply vs_alt, pvs_updateP_empty. Qed.
Lemma vs_update E m m' : m ~~> m' ownG m >{E}> ownG m'.
Proof. by intros; apply vs_alt, pvs_update. Qed.
Lemma vs_alloc E P : ¬set_finite E P >{E}> ( i, (i E) inv i P).
Lemma vs_alloc E P : ¬set_finite E P >{E}> ( i, (i E) ownI i P).
Proof. by intros; apply vs_alt, pvs_alloc. Qed.
End vs.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment