Commit 8e793079 authored by Joseph Tassarotti's avatar Joseph Tassarotti
Browse files

Update for dependencies; fix ownership (except unresolved issue of ATimeless...

Update for dependencies; fix ownership (except unresolved issue of ATimeless and some other modality interactions).
parent 5a8e79e8
......@@ -21,9 +21,11 @@ theories/algebra/dec_agree.v
theories/algebra/excl.v
theories/algebra/iprod.v
theories/algebra/upred.v
theories/algebra/upred_bi.v
theories/algebra/upred_tactics.v
theories/algebra/upred_big_op.v
theories/algebra/upred_hlist.v
theories/algebra/base_logic.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
......
......@@ -6,6 +6,6 @@ install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/fri" ]
depends: [
"coq" { >= "8.7" }
"coq-stdpp" { (>= "1.1.0") | (= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-01-11.3" ) }
"coq-stdpp" { (>= "1.1.0") | (>= "dev") }
"coq-iris" { (= "branch.gen_proofmode.2018-02-08.1") }
]
From iris.bi Require Export bi.
From iris.proofmode Require Import tactics.
(*
From iris.algebra Require Import proofmode_classes.
*)
From fri.algebra Require Export upred_bi.
Module Import uPred.
Export upred.uPred.
Export bi.
End uPred.
(* Hint DB for the logic *)
Hint Resolve pure_intro : I.
Hint Resolve or_elim or_intro_l' or_intro_r' : I.
Hint Resolve and_intro and_elim_l' and_elim_r' : I.
Hint Resolve persistently_mono : I.
Hint Resolve sep_mono : I. (* sep_elim_l' sep_elim_r' *)
Hint Immediate True_intro False_elim : I.
Hint Immediate iff_refl internal_eq_refl : I.
(* Setup of the proof mode *)
Hint Extern 1 (coq_tactics.envs_entails _ (|==> _)) => iModIntro.
\ No newline at end of file
From fri.algebra Require Export cmra.
From iris.bi Require derived_connectives updates.
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etrans; [|eassumption].
(* Local Hint Extern 1 (_ {_} _) => reflexivity. *)
......@@ -17,6 +18,7 @@ Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Delimit Scope uPred_scope with I.
Delimit Scope uPred_scope with IP.
Bind Scope uPred_scope with uPred.
Arguments uPred_holds {_} _%I _ _ _.
......@@ -445,12 +447,24 @@ Class UnlimitedP {M} (P : uPred M) := {
}.
Module uPred.
Definition unseal :=
Module Unseal.
Definition unseal_eqs :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_relevant_eq, uPred_affine_eq,
uPred_later_eq, uPred_ownM_eq, uPred_ownMl_eq, uPred_valid_eq, uPred_emp_eq, uPred_stopped_eq,
uPred_plainly_eq, uPred_persistent_eq).
Ltac unseal := rewrite !unseal /=.
uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq,
uPred_plainly_eq, uPred_persistent_eq, uPred_later_eq, uPred_ownM_eq,
uPred_valid_eq, uPred_relevant_eq, uPred_affine_eq, uPred_ownMl_eq, uPred_emp_eq, uPred_stopped_eq).
Import iris.bi.derived_connectives.
Ltac unfold_bi := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl;
unfold (* uPred_emp, *) bi_pure, bi_and, bi_or, bi_impl, bi_forall, bi_exist,
bi_sep, bi_wand, bi_plainly, bi_persistently, bi_affinely, sbi_later; simpl;
unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
sbi_internal_eq, sbi_sep, sbi_wand, sbi_plainly, sbi_persistently; simpl.
Ltac unseal := unfold_bi; rewrite !unseal_eqs /=.
Ltac try_unseal := unfold_bi; rewrite ?unseal_eqs /=.
End Unseal.
Include Unseal.
Section uPred_logic.
Context {M : ucmraT}.
......@@ -690,7 +704,7 @@ Qed.
Lemma affine_equiv P: P ⊣⊢ (P Emp).
Proof.
unseal; apply (anti_symm ()); split=> n x y ??; naive_solver.
uPred.unseal; apply (anti_symm ()); split=> n x y ?? => //=; naive_solver.
Qed.
(* Derived logical stuff *)
......@@ -1926,11 +1940,11 @@ Lemma option_equivI {A : ofeT} (mx my : option A) :
| Some x, Some y => x y | None, None => True | _, _ => False
end.
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
Qed.
Lemma option_validI {A : cmraT} (mx : option A) :
mx ⊣⊢ match mx with Some x => x | None => True end.
Proof. uPred.unseal. by destruct mx. Qed.
Proof. unseal. by destruct mx. Qed.
(* Timeless *)
Lemma timelessP_spec P : TimelessP P n x y, {n} x {n} y P 0 x y P n x y.
......
From fri.algebra Require Import upred.
From iris Require Import bi.
From iris.bi Require Export bi.
Import uPred.
Lemma uPred_bi_mixin (M : ucmraT) : BiMixin (ofe_mixin_of (uPred M))
Lemma uPred_bi_mixin (M : ucmraT) : BiMixin
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_eq M)
(@uPred_forall M) (@uPred_exist M)
uPred_sep uPred_wand uPred_plainly uPred_persistent.
Proof.
split; try apply _; eauto with I.
......@@ -22,13 +22,6 @@ Proof.
- intros; by apply forall_elim.
- intros; by apply exist_intro.
- intros; by apply exist_elim.
- (* a b Ψ a Ψ b *)
intros A a b Ψ Hnonexp.
unseal; split=> n x ? Hab n' x' y' ????? HΨ. eapply Hnonexp with n a; auto.
- by unseal.
- by unseal.
- (* Discrete a a b ⊣⊢ a b *)
intros A a b ?. unseal; split=> n x y ??; by apply (discrete_iff n).
- intros; by rewrite left_id.
- intros; by rewrite left_id.
- intros; by rewrite comm.
......@@ -44,7 +37,6 @@ Proof.
- admit.
- admit.
- admit.
- admit.
- intros P Q.
unseal=> HPQ.
split=> n x y ?? ?.
......@@ -72,3 +64,124 @@ Proof.
rewrite /uPred_holds//=.
* done.
Admitted.
Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin (ofe_mixin_of (uPred M))
uPred_entails uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M)
uPred_sep uPred_plainly uPred_persistent (@uPred_eq M)
uPred_later.
Proof.
split; try apply _; eauto with I.
- (* a b Ψ a Ψ b *)
intros A a b Ψ Hnonexp.
unseal; split=> n x ? Hab n' x' y' ????? HΨ. eapply Hnonexp with n a; auto.
- by unseal.
- by unseal.
- (* Discrete a a b ⊣⊢ a b *)
intros A a b ?. unseal; split=> n x y ??; by apply (discrete_iff n).
- admit.
- by unseal.
- by unseal.
- apply later_mono.
- apply löb.
- intros. by rewrite later_forall.
- intros A Φ. unseal; split=> -[|[|n]] x y ?? Hsat /=; eauto.
* by left.
* destruct Hsat as (a&?). right. by exists a.
* destruct Hsat as (a&?). right. by exists a.
- intros; by rewrite later_sep.
- intros; by rewrite later_sep.
- admit.
- admit.
- by unseal.
- by unseal.
- (* P False ( False P) *)
intros P. unseal; split=> -[|n] x y ?? /= HP; [by left|right].
intros [|n'] x' y' ????; [|done].
eapply (uPred_mono _ _ _ x); eauto.
eapply (uPred_closed _ _ n); eauto.
* omega.
* eapply cmra_validN_le; eauto.
* by apply cmra_included_includedN.
Admitted.
Canonical Structure uPredI (M : ucmraT) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
Canonical Structure uPredSI (M : ucmraT) : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of (uPred M);
sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
Global Instance ownM_persistent {M: ucmraT} (a : M) :
cmra.Persistent a Persistent (uPred_ownM a).
Proof.
intros HPa. rewrite /Persistent. unseal.
split=> n x y ?? [a' Hx].
eapply uPred_mono with a y; eauto.
- exists (core a). by rewrite cmra_core_r persistent_core.
- by eexists.
Qed.
Global Notation "■ φ" := (uPred_pure φ%stdpp%type)
(at level 20, right associativity) : bi_scope.
Global Notation "⧆ P" := (bi_affinely P%I)
(at level 20, right associativity) : bi_scope.
Global Notation "⧈ P" := (bi_affinely (bi_persistently P%I))
(at level 20, right associativity) : uPred_scope.
Global Notation "✓ x" := (uPred_valid x) (at level 20) : bi_scope.
Infix "★" := bi_sep : bi_scope.
Lemma ownM_op {M: ucmraT} (a1 a2 : M) :
uPred_ownM (a1 a2) ⊣⊢ uPred_ownM a1 uPred_ownM a2.
Proof.
unseal; split=> n x y ??; split.
- intros [z ?]; exists a1, (a2 z), y, (core y);
split_and!; [by rewrite (assoc op)| by rewrite cmra_core_r | |].
* by exists (core a1); rewrite cmra_core_r.
* by exists z.
- intros (y1&y2&q1&q2&Hx&Hy&[z1 Hy1]&[z2 Hy2]); exists (z1 z2).
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Lemma ownM_op'' {M: ucmraT} (a1 a2 : M) :
uPred_ownM (a1 a2) ⊣⊢ ( uPred_ownM a1 uPred_ownM a2).
Proof.
unseal; split=> n x y ??; split.
- unseal. intros [Heqy [z ?]]. exists a1, (a2 z), y, ( : M) ;
split_and!; [by rewrite (assoc op)| by rewrite right_id | |].
* rewrite Heqy; split; auto; unfold uPred_holds => //=.
* split; auto; unfold uPred_holds => //=.
by exists z.
- unseal. intros (y1&y2&q1&q2&Hx&Hy&(Hq1&[z1 Hy1])&(Hq2&[z2 Hy2])).
split.
* rewrite Hy Hq1 Hq2 right_id //=. unfold uPred_holds => //=.
* exists (z1 z2).
by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
Qed.
Global Instance ownM_timeless {M: ucmraT} (a : M) : Discrete a Timeless (uPred_ownM a).
Proof.
intros. rewrite /Timeless.
unseal. split=> n x y ?? HP.
destruct n => //=; rewrite /sbi_except_0; unseal => //=.
* left. auto.
* right. apply cmra_included_includedN, cmra_timeless_included_l; eauto.
** eapply cmra_validN_le; eauto. omega.
** destruct HP as (x'&?). apply cmra_includedN_le with n.
*** exists x'. eauto.
*** omega.
Qed.
Lemma ownM_empty {M: ucmraT} : emp uPred_ownM (: M).
Proof. unseal; split=> n x ????. unseal. split; auto; exists x. by rewrite left_id. Qed.
Lemma ownMl_valid {M: ucmraT} (a : M) : uPred_ownMl a (uPred_ownMl a ⧆✓ a).
Proof.
unseal; split=> n x y Hv //= ? Heq.
exists x, (core x), y, ( : M). rewrite ?cmra_core_r ?right_id. split_and!; auto.
unseal. split; rewrite /uPred_holds //= in Heq *. by ofe_subst.
Qed.
Lemma ownMl_empty {M: ucmraT} : emp ⊣⊢ uPred_ownMl (: M).
Proof. unseal; split=> n x y ??. rewrite /uPred_holds //=. Qed.
\ No newline at end of file
(*
From fri.program_logic Require Import ownership.
From fri.program_logic Require Export namespaces.
From fri.proofmode Require Import pviewshifts.
From fri.algebra Require Export base_logic updates.
From iris.proofmode Require Import tactics.
*)
From stdpp Require Export coPset.
From fri.algebra Require Export upred_big_op updates.
From fri.program_logic Require Export model.
From fri.program_logic Require Import ownership wsat.
From fri.program_logic Require Export namespaces pviewshifts.
From iris.proofmode Require Import tactics.
Import uPred.
(** Derived forms and lemmas about them. *)
......@@ -23,11 +31,19 @@ Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
Proof.
rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
Qed.
Global Instance inv_relevant N P : RelevantP (inv N P).
Global Instance inv_relevant N P : Persistent (inv N P).
Proof.
rewrite inv_eq /inv /RelevantP. rewrite relevant_exist.
eapply exist_mono=>i. rewrite relevant_relevant'. auto.
rewrite inv_eq /inv /Persistent. rewrite persistently_exist.
eapply exist_mono=>i. apply persistently_intro.
Print Instances Persistent.
apply and_persistent.
apply affinely_persistent.
apply pure_persistent.
Print ownI.
app
apply _.
apply _. repeat unfold_bi. Print uPred_pure. rewrite /uPred_pure. rewrite relevant_relevant'. auto.
Qed.
Global Instance inv_affine N P : AffineP (inv N P).
Proof.
......@@ -38,8 +54,14 @@ Qed.
Lemma always_inv N P : inv N P ⊣⊢ inv N P.
Proof. by rewrite relevant_relevant'. Qed.
*)
Print pvs.
Print Instances FUpd.
Lemma inv_alloc N E P : nclose N E ⧆▷ P pvs E E (inv N P).
Lemma inv_alloc N E P : nclose N E ⧆▷ P |={E}=> inv N P.
Lemma inv_alloc N E P : nclose N E ⧆▷ P (|={E,E}=> inv N P).
Proof.
intros. rewrite -(pvs_mask_weaken N) //.
rewrite inv_eq /inv (pvs_allocI N); last apply nclose_infinite.
......
From fri.algebra Require Export upred.
From fri.algebra Require Export base_logic upred.
From fri.program_logic Require Export resources.
From fri.algebra Require cofe_solver.
......@@ -20,7 +20,7 @@ Definition iRes Λ Σ := res Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := option (excl (state Λ)).
Definition iProp (Λ : language) (Σ : iFunctor) : ofeT := uPredC (iResUR Λ Σ).
Definition iProp (Λ : language) (Σ : iFunctor) : ofeT := upred.uPredC (iResUR Λ Σ).
Parameter iProp_unfold: {Λ Σ}, iProp Λ Σ -n> iPreProp Λ Σ.
Parameter iProp_fold: {Λ Σ}, iPreProp Λ Σ -n> iProp Λ Σ.
......@@ -33,7 +33,7 @@ End iProp_solution_sig.
Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver.
Definition iProp_result (Λ : language) (Σ : iFunctor) :
solution (uPredCF (resURF Λ ( ) Σ)) := solver.result _.
solution (upred.uPredCF (resURF Λ ( ) Σ)) := solver.result _.
Definition iPreProp (Λ : language) (Σ : iFunctor) : ofeT := iProp_result Λ Σ.
Definition iGst (Λ : language) (Σ : iFunctor) : ucmraT := Σ (iPreProp Λ Σ).
......@@ -42,7 +42,7 @@ Definition iResUR Λ Σ := resUR Λ (laterC (iPreProp Λ Σ)) (iGst Λ Σ).
Definition iWld Λ Σ := gmap positive (agree (laterC (iPreProp Λ Σ))).
Definition iPst Λ := option (excl (state Λ)).
Definition iProp (Λ : language) (Σ : iFunctor) : ofeT := uPredC (iResUR Λ Σ).
Definition iProp (Λ : language) (Σ : iFunctor) : ofeT := upred.uPredC (iResUR Λ Σ).
Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ :=
solution_fold (iProp_result Λ Σ).
Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
......
From fri.algebra Require Export upred_big_op updates.
From fri.program_logic Require Export model.
From iris.proofmode Require Import tactics.
Import uPred.
Definition ownI {Λ Σ} (i : positive) (P : iProp Λ Σ) : iProp Λ Σ :=
( (uPred_ownM (Res {[ i := to_agree (Next (iProp_unfold P)) ]} )))%I.
......@@ -24,59 +27,70 @@ Implicit Types m : iGst Λ Σ.
Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i).
Proof.
intros n P Q HPQ. rewrite /ownI.
apply uPred.affine_ne, uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
unfold_bi.
apply and_ne => //.
apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne.
apply Next_contractive. destruct n => //=; rewrite //= in HPQ; rewrite HPQ //=.
Qed.
(*
Global Instance ownI_relevant i P : RelevantP (ownI i P).
Proof. rewrite /ownI. unfold_bi. apply _. Qed.
*)
Global Instance ownI_persistent i P : Persistent (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Global Instance ownI_affine i P : AffineP (ownI i P).
Global Instance ownI_affine i P : Affine (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
(* physical state *)
Lemma ownP_twice σ1 σ2 : ownP σ1 ownP σ2 (False : iProp Λ Σ).
Lemma ownP_twice σ1 σ2 : ownP σ1 ownP σ2 (False : iProp Λ Σ).
Proof.
rewrite /ownP uPred.sep_affine_1 -uPred.ownM_op Res_op.
rewrite /ownP.
iIntros "(H1&H2)". iCombine "H1" "H2" as "H".
rewrite -upred_bi.ownM_op Res_op.
rewrite uPred.ownM_invalid; eauto with I.
by intros (_&?&_).
Qed.
Global Instance ownP_affine σ : AffineP (@ownP Λ Σ σ).
Global Instance ownP_affine σ : Affine (@ownP Λ Σ σ).
Proof. rewrite /ownP. apply _. Qed.
(*
Global Instance ownP_atimeless σ : ATimelessP (@ownP Λ Σ σ).
Proof. rewrite /ownP. apply _. Qed.
Proof. Print Timeless. Print ATimelessP. rewrite /ownP. apply _. Qed.
*)
(* ghost state *)
Global Instance ownG_ne n : Proper (dist n ==> dist n) (@ownG Λ Σ).
Proof. solve_proper. Qed.
Global Instance ownG_affine m : AffineP (ownG m).
Proof. intros ??. rewrite /ownG. intros ->. done. Qed.
Global Instance ownG_affine m : Affine (ownG m).
Proof. rewrite /ownG. apply _. Qed.
Global Instance ownG_proper : Proper (() ==> (⊣⊢)) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 m2) ⊣⊢ ownG m1 ownG m2.
Proof. by rewrite /ownG -uPred.ownM_op'' Res_op !left_id. Qed.
Lemma ownG_op m1 m2 : ownG (m1 m2) ⊣⊢ ownG m1 ownG m2.
Proof. by rewrite /ownG -upred_bi.ownM_op'' Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with typeclass_instances I. Qed.
Lemma ownG_valid m : ownG m ⧆✓ m.
Proof. rewrite /ownG uPred.ownM_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownG_valid_r m : ownG m ownG m ⧆✓ m.
Proof. apply (uPred.relevant_entails_r _ _), ownG_valid. Qed.
Lemma ownG_empty : Emp (ownG : iProp Λ Σ).
Proof. apply: uPred.ownM_empty'. Qed.
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with *. Qed.
Lemma ownG_valid m : ownG m ( m).
Proof. rewrite /ownG uPred.ownM_valid res_validI /=. rewrite ?affinely_and; auto with *. Qed.
Lemma ownG_empty : emp (ownG : iProp Λ Σ).
Proof. rewrite /ownG. by apply @upred_bi.ownM_empty. Qed.
(*
Global Instance ownG_timeless m : Discrete m ATimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
Global Instance ownG_relevant m : Persistent m RelevantP (ownG m).
Proof. rewrite /ownG; apply _. Qed.
*)
(* linear ghost state *)
Global Instance ownGl_ne n : Proper (dist n ==> dist n) (@ownGl Λ Σ).
Proof. solve_proper. Qed.
Proof. intros P Q HPQ. rewrite /ownGl. rewrite HPQ. done. Qed.
Global Instance ownGl_proper : Proper (() ==> (⊣⊢)) (@ownGl Λ Σ) := ne_proper _.
Lemma ownGl_op m1 m2 : ownGl (m1 m2) ⊣⊢ (ownGl m1 ownGl m2).
Proof. by rewrite /ownGl -uPred.ownMl_op Res_op !left_id. Qed.
Proof. by rewrite /ownGl; unfold_bi; rewrite -uPred.ownMl_op Res_op !left_id. Qed.
Lemma ownGl_valid_r m : ownGl m (ownGl m ⧆✓ m).
Proof. rewrite /ownGl {1}uPred.ownMl_valid res_validI /= ?uPred.affine_and; auto with I. Qed.
Lemma ownGl_empty : Emp (ownGl : iProp Λ Σ).
Proof. by rewrite /ownGl uPred.ownMl_empty. Qed.
Proof. rewrite /ownGl {1}upred_bi.ownMl_valid res_validI /= !affinely_and; auto with I. Qed.
Lemma ownGl_empty : emp (ownGl : iProp Λ Σ).
Proof. by rewrite /ownGl upred_bi.ownMl_empty. Qed.
(*
Global Instance ownGl_relevant m : Persistent m RelevantP (ownGl m).
Proof. rewrite /ownGl; apply _. Qed.
*)
(* inversion lemmas *)
Lemma ownI_spec n r r' i P :
......@@ -84,9 +98,9 @@ Lemma ownI_spec n r r' i P :
{n} r'
(ownI i P) n r r' wld r !! i {n} Some (to_agree (Next (iProp_unfold P))) r' {n} .
Proof.
intros (?&?&?) (?&?&?). rewrite /ownI; uPred.unseal.
intros (?&?&?) (?&?&?). rewrite /ownI; do 2 unseal.
rewrite /uPred_holds/=/uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [((P'&Hi&HP)&_) ?]; rewrite Hi.
- intros [? ((P'&Hi&HP)&_)]; rewrite Hi.
split; auto. constructor; symmetry; apply agree_valid_includedN.
+ by apply lookup_validN_Some with (wld r) i.
+ by destruct HP as [?| ->].
......@@ -94,19 +108,19 @@ Proof.
Qed.
Lemma ownP_spec n r r' σ : {n} r {n} r' (ownP σ) n r r' pst r Excl' σ r' {n} .
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
intros (?&?&?) (?&?&?). rewrite /ownP; do 2 unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (discrete_iff n). naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownP_spec' n r r' σ : {n} r {n} r' (ownP σ) n r r' pst r Excl' σ.
Proof.
intros (?&?&?) (?&?&?). rewrite /ownP; uPred.unseal.
intros (?&?&?) (?&?&?). rewrite /ownP; do 2 unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (discrete_iff n). naive_solver (apply cmra_unit_leastN).
Qed.
Lemma ownG_spec n r r' m : (ownG m) n r r' m {n} gst r r' {n} .
Proof.
rewrite /ownG; uPred.unseal.
rewrite /ownG; do 2 unseal.
rewrite /uPred_holds /= /uPred_holds /= res_includedN; naive_solver (apply ucmra_unit_leastN).
Qed.
Lemma ownGl_spec n r r' m : (ownGl m) n r r' Res m {n} r'.
......
......@@ -9,6 +9,7 @@ Local Hint Extern 10 (✓{_} _) =>
repeat match goal with
| H : wsat _ _ _ _ _ |- _ => apply wsat_valid in H; last omega
end; solve_validN.
Import uPred.
Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
{| uPred_holds n r1 rl := k Ef σ rf rfl ,
......@@ -33,6 +34,10 @@ Definition pvs_eq : @pvs = @pvs_def := proj2_sig pvs_aux.
Arguments pvs {_ _} _ _ _%I.
Instance: Params (@pvs) 4.
Global Instance pvs_FUpd {Λ Σ} : FUpd _ := @pvs Λ Σ.
Global Instance pvs_BUpd {Λ Σ} : BUpd _ := @pvs Λ Σ .
(*
Notation "|={ E1 , E2 }=> Q" := (pvs E1 E2 Q%I)
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }=> Q") : uPred_scope.
......@@ -42,17 +47,21 @@ Notation "|={ E }=> Q" := (pvs E E Q%I)
Notation "|==> Q" := (pvs Q%I)
(at level 99, Q at level 200, format "|==> 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) : stdpp_scope.
Notation "P ={ E }=> Q" := (P |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
Notation "P ={ E1 , E2 }=★ Q" := (P - |={E1,E2}=> Q)%I
(*
Infix "-∗" := bi_wand.
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 ={ E }= Q" := (P ={E,E}= Q)%I
format "P ={ E1 , E2 }= Q") : bi_scope.
Notation "P ={ E }= Q" := (P ={E,E}= Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ={ E }=★ Q") : uPred_scope.
format "P ={ E }=∗ Q") : uPred_scope.
*)
Section pvs.
Context {Λ : language} {Σ : iFunctor}.
......@@ -74,51 +83,49 @@ Proof. apply ne_proper, _. Qed.
Lemma pvs_intro E P : P ={E}=> P.
Proof.
rewrite pvs_eq. split=> n r ? HP k Ef σ rf ???; exists r; split; last done.
rewrite /pvs_FUpd pvs_eq. split=> n r ? HP k Ef σ rf ???; exists r; split; last done.
apply uPred_closed with n; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}=> Q.
Proof.
rewrite pvs_eq. intros HPQ; split=> n r rl ? ? HP k Ef σ rf rfl ???.
rewrite /pvs_FUpd pvs_eq. intros HPQ; split=> n r rl ? ? HP k Ef σ rf rfl ???.
destruct (HP k Ef σ rf rfl) as (r2&?&?); eauto.
exists r2; eauto using uPred_in_entails.
Qed.
Lemma pvs_timeless E P : TimelessP P P ={E}=> P.
Proof.
rewrite pvs_eq uPred.timelessP_spec=> HP.
rewrite /pvs_FUpd pvs_eq uPred.timelessP_spec=> HP.
rewrite /pvs_FUpd.
uPred.unseal; split=>-[|n] r ? HP' k Ef σ rf ???; first lia.
exists r; split; last done.
apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
Lemma pvs_timeless_affine E P : ATimelessP P ⧆▷ P ={E}=> P.
Proof.
rewrite pvs_eq uPred.atimelessP_spec=> HP.
uPred.unseal; split=>-[|n] r rl ?? [HP' Haff] rf ? k Ef σ ???; first lia.
rewrite /pvs_FUpd pvs_eq uPred.atimelessP_spec=> HP.
repeat unseal; split=>-[|n] r rl ?? [Haff HP'] k Ef σ ???; first lia.