Commit 99cbb525 authored by Ralf Jung's avatar Ralf Jung

new notation for pure assertions

parent d04287bc
......@@ -19,6 +19,9 @@ Coq development, but not every API-breaking change is listed. Changes marked
* Renaming and moving things around: uPred and the rest of the base logic are
in `base_logic`, while `program_logic` is for everything involving the
general Iris notion of a language.
* Changed notation for embedding Coq assertions into Iris. The new notation
is ⌜φ⌝. Also removed `=` and `⊥` from the Iris scope.
(The old notations are provided in `base_logic.deprecated`.)
* With invariants and the physical state being handled in the logic, there
is no longer any reason to demand the CMRA unit to be discrete.
* The language can now fork off multiple threads at once.
......
......@@ -68,6 +68,7 @@ base_logic/big_op.v
base_logic/hlist.v
base_logic/soundness.v
base_logic/double_negation.v
base_logic/deprecated.v
base_logic/lib/iprop.v
base_logic/lib/own.v
base_logic/lib/saved_prop.v
......
......@@ -252,7 +252,7 @@ Section list.
Lemma big_sepL_forall Φ l :
( k x, PersistentP (Φ k x))
([ list] kx l, Φ k x) ⊣⊢ ( k x, l !! k = Some x Φ k x).
([ list] kx l, Φ k x) ⊣⊢ ( k x, l !! k = Some x Φ k x).
Proof.
intros HΦ. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
......@@ -265,7 +265,7 @@ Section list.
Qed.
Lemma big_sepL_impl Φ Ψ l :
( k x, l !! k = Some x Φ k x Ψ k x) ([ list] kx l, Φ k x)
( k x, l !! k = Some x Φ k x Ψ k x) ([ list] kx l, Φ k x)
[ list] kx l, Ψ k x.
Proof.
rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
......@@ -376,7 +376,7 @@ Section gmap.
Lemma big_sepM_forall Φ m :
( k x, PersistentP (Φ k x))
([ map] kx m, Φ k x) ⊣⊢ ( k x, m !! k = Some x Φ k x).
([ map] kx m, Φ k x) ⊣⊢ ( k x, m !! k = Some x Φ k x).
Proof.
intros. apply (anti_symm _).
{ apply forall_intro=> k; apply forall_intro=> x.
......@@ -392,7 +392,7 @@ Section gmap.
Qed.
Lemma big_sepM_impl Φ Ψ m :
( k x, m !! k = Some x Φ k x Ψ k x) ([ map] kx m, Φ k x)
( k x, m !! k = Some x Φ k x Ψ k x) ([ map] kx m, Φ k x)
[ map] kx m, Ψ k x.
Proof.
rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
......@@ -473,7 +473,7 @@ Section gset.
Proof. apply: big_opS_singleton. Qed.
Lemma big_sepS_filter (P : A Prop) `{ x, Decision (P x)} Φ X :
([ set] y filter P X, Φ y) ⊣⊢ ([ set] y X, P y Φ y).
([ set] y filter P X, Φ y) ⊣⊢ ([ set] y X, P y Φ y).
Proof.
induction X as [|x X ? IH] using collection_ind_L.
{ by rewrite filter_empty_L !big_sepS_empty. }
......@@ -500,7 +500,7 @@ Section gset.
Proof. apply (big_opS_commute _). Qed.
Lemma big_sepS_forall Φ X :
( x, PersistentP (Φ x)) ([ set] x X, Φ x) ⊣⊢ ( x, (x X) Φ x).
( x, PersistentP (Φ x)) ([ set] x X, Φ x) ⊣⊢ ( x, x X Φ x).
Proof.
intros. apply (anti_symm _).
{ apply forall_intro=> x.
......@@ -514,7 +514,7 @@ Section gset.
Qed.
Lemma big_sepS_impl Φ Ψ X :
( x, (x X) Φ x Ψ x) ([ set] x X, Φ x) [ set] x X, Ψ x.
( x, x X Φ x Ψ x) ([ set] x X, Φ x) [ set] x X, Ψ x.
Proof.
rewrite always_and_sep_l always_forall.
setoid_rewrite always_impl; setoid_rewrite always_pure.
......
From iris.base_logic Require Import primitive.
(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
Notation "■ φ" := (uPred_pure φ%C%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.
(* Deprecated 2016-11-22. Use ⌜x ⊥ y ⌝ instead. *)
Notation "x ⊥ y" := (uPred_pure (x%C%type y%C%type)) (only parsing) : uPred_scope.
......@@ -212,53 +212,53 @@ Proof.
- apply or_elim; apply exist_elim=> a; rewrite -(exist_intro a); auto.
Qed.
Lemma pure_mono φ1 φ2 : (φ1 φ2) φ1 φ2.
Lemma pure_mono φ1 φ2 : (φ1 φ2) ⌜φ1 ⌜φ2.
Proof. intros; apply pure_elim with φ1; eauto. Qed.
Global Instance pure_mono' : Proper (impl ==> ()) (@uPred_pure M).
Proof. intros φ1 φ2; apply pure_mono. Qed.
Lemma pure_iff φ1 φ2 : (φ1 φ2) φ1 ⊣⊢ φ2.
Lemma pure_iff φ1 φ2 : (φ1 φ2) ⌜φ1 ⊣⊢ ⌜φ2.
Proof. intros [??]; apply (anti_symm _); auto using pure_mono. Qed.
Lemma pure_intro_l φ Q R : φ ( φ Q R) Q R.
Lemma pure_intro_l φ Q R : φ (⌜φ⌝ Q R) Q R.
Proof. intros ? <-; auto using pure_intro. Qed.
Lemma pure_intro_r φ Q R : φ (Q φ R) Q R.
Lemma pure_intro_r φ Q R : φ (Q ⌜φ⌝ R) Q R.
Proof. intros ? <-; auto. Qed.
Lemma pure_intro_impl φ Q R : φ (Q φ R) Q R.
Lemma pure_intro_impl φ Q R : φ (Q ⌜φ⌝ R) Q R.
Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
Lemma pure_elim_l φ Q R : (φ Q R) φ Q R.
Lemma pure_elim_l φ Q R : (φ Q R) ⌜φ⌝ Q R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_r φ Q R : (φ Q R) Q φ R.
Lemma pure_elim_r φ Q R : (φ Q R) Q ⌜φ⌝ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_True (φ : Prop) : φ φ ⊣⊢ True.
Lemma pure_True (φ : Prop) : φ ⌜φ⌝ ⊣⊢ True.
Proof. intros; apply (anti_symm _); auto. Qed.
Lemma pure_False (φ : Prop) : ¬φ φ ⊣⊢ False.
Lemma pure_False (φ : Prop) : ¬φ ⌜φ⌝ ⊣⊢ False.
Proof. intros; apply (anti_symm _); eauto using pure_elim. Qed.
Lemma pure_and φ1 φ2 : (φ1 φ2) ⊣⊢ φ1 φ2.
Lemma pure_and φ1 φ2 : ⌜φ1 φ2 ⊣⊢ ⌜φ1 ⌜φ2.
Proof.
apply (anti_symm _).
- eapply pure_elim=> // -[??]; auto.
- eapply (pure_elim φ1); [auto|]=> ?. eapply (pure_elim φ2); auto.
Qed.
Lemma pure_or φ1 φ2 : (φ1 φ2) ⊣⊢ φ1 φ2.
Lemma pure_or φ1 φ2 : ⌜φ1 φ2 ⊣⊢ ⌜φ1 ⌜φ2.
Proof.
apply (anti_symm _).
- eapply pure_elim=> // -[?|?]; auto.
- apply or_elim; eapply pure_elim; eauto.
Qed.
Lemma pure_impl φ1 φ2 : (φ1 φ2) ⊣⊢ ( φ1 φ2).
Lemma pure_impl φ1 φ2 : ⌜φ1 φ2 ⊣⊢ (⌜φ1 ⌜φ2).
Proof.
apply (anti_symm _).
- apply impl_intro_l. rewrite -pure_and. apply pure_mono. naive_solver.
- rewrite -pure_forall_2. apply forall_intro=> ?.
by rewrite -(left_id True uPred_and (__))%I (pure_True φ1) // impl_elim_r.
Qed.
Lemma pure_forall {A} (φ : A Prop) : ( x, φ x) ⊣⊢ x, φ x.
Lemma pure_forall {A} (φ : A Prop) : ⌜∀ x, φ x ⊣⊢ x, ⌜φ x.
Proof.
apply (anti_symm _); auto using pure_forall_2.
apply forall_intro=> x. eauto using pure_mono.
Qed.
Lemma pure_exist {A} (φ : A Prop) : ( x, φ x) ⊣⊢ x, φ x.
Lemma pure_exist {A} (φ : A Prop) : ⌜∃ x, φ x ⊣⊢ x, ⌜φ x.
Proof.
apply (anti_symm _).
- eapply pure_elim=> // -[x ?]. rewrite -(exist_intro x); auto.
......@@ -273,13 +273,13 @@ Proof. by intros ->. Qed.
Lemma internal_eq_sym {A : ofeT} (a b : A) : a b b a.
Proof. apply (internal_eq_rewrite a b (λ b, b a)%I); auto. solve_proper. Qed.
Lemma pure_impl_forall φ P : ( φ P) ⊣⊢ ( _ : φ, P).
Lemma pure_impl_forall φ P : (⌜φ⌝ P) ⊣⊢ ( _ : φ, P).
Proof.
apply (anti_symm _).
- apply forall_intro=> ?. by rewrite pure_True // left_id.
- apply impl_intro_l, pure_elim_l=> Hφ. by rewrite (forall_elim Hφ).
Qed.
Lemma pure_alt φ : φ ⊣⊢ _ : φ, True.
Lemma pure_alt φ : ⌜φ⌝ ⊣⊢ _ : φ, True.
Proof.
apply (anti_symm _).
- eapply pure_elim; eauto=> H. rewrite -(exist_intro H); auto.
......@@ -406,9 +406,9 @@ Lemma sep_and P Q : (P ∗ Q) ⊢ (P ∧ Q).
Proof. auto. Qed.
Lemma impl_wand P Q : (P Q) P - Q.
Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
Lemma pure_elim_sep_l φ Q R : (φ Q R) φ Q R.
Lemma pure_elim_sep_l φ Q R : (φ Q R) ⌜φ⌝ Q R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Lemma pure_elim_sep_r φ Q R : (φ Q R) Q φ R.
Lemma pure_elim_sep_r φ Q R : (φ Q R) Q ⌜φ⌝ R.
Proof. intros; apply pure_elim with φ; eauto. Qed.
Global Instance sep_False : LeftAbsorb (⊣⊢) False%I (@uPred_sep M).
......@@ -452,7 +452,7 @@ Proof. intros P Q; apply always_mono. Qed.
Lemma always_intro' P Q : ( P Q) P Q.
Proof. intros <-. apply always_idemp. Qed.
Lemma always_pure φ : φ ⊣⊢ φ.
Lemma always_pure φ : ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. apply (anti_symm _); auto using always_pure_2. Qed.
Lemma always_forall {A} (Ψ : A uPred M) : ( a, Ψ a) ⊣⊢ ( a, Ψ a).
Proof.
......@@ -560,7 +560,7 @@ Proof. destruct p; simpl; auto using always_elim. Qed.
Lemma always_elim_if p P : P ?p P.
Proof. destruct p; simpl; auto using always_elim. Qed.
Lemma always_if_pure p φ : ?p φ ⊣⊢ φ.
Lemma always_if_pure p φ : ?p ⌜φ⌝ ⊣⊢ ⌜φ⌝.
Proof. destruct p; simpl; auto using always_pure. Qed.
Lemma always_if_and p P Q : ?p (P Q) ⊣⊢ ?p P ?p Q.
Proof. destruct p; simpl; auto using always_and. Qed.
......@@ -663,7 +663,7 @@ Proof.
Qed.
(* Timeless instances *)
Global Instance pure_timeless φ : TimelessP ( φ : uPred M)%I.
Global Instance pure_timeless φ : TimelessP (⌜φ⌝ : uPred M)%I.
Proof.
rewrite /TimelessP pure_alt later_exist_false. by setoid_rewrite later_True.
Qed.
......@@ -725,7 +725,7 @@ Proof.
Qed.
(* Persistence *)
Global Instance pure_persistent φ : PersistentP ( φ : uPred M)%I.
Global Instance pure_persistent φ : PersistentP (⌜φ⌝ : uPred M)%I.
Proof. by rewrite /PersistentP always_pure. Qed.
Global Instance always_persistent P : PersistentP ( P).
Proof. by intros; apply always_intro'. Qed.
......
......@@ -36,7 +36,7 @@ Implicit Types x : M.
Import uPred.
(* Helper lemmas about iterated later modalities *)
Lemma laterN_big n a x φ: {n} x a n (^a ( φ))%I n x φ.
Lemma laterN_big n a x φ: {n} x a n (^a ⌜φ⌝)%I n x φ.
Proof.
induction 2 as [| ?? IHle].
- induction a; repeat (rewrite //= || uPred.unseal).
......@@ -46,7 +46,7 @@ Proof.
eapply uPred_closed; eauto using cmra_validN_S.
Qed.
Lemma laterN_small n a x φ: {n} x n < a (^a ( φ))%I n x.
Lemma laterN_small n a x φ: {n} x n < a (^a ⌜φ⌝)%I n x.
Proof.
induction 2.
- induction n as [| n IHn]; [| move: IHn];
......@@ -85,7 +85,7 @@ Proof.
by rewrite -assoc wand_elim_r wand_elim_l.
Qed.
Lemma nnupd_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x =n=> y, Φ y uPred_ownM y.
x ~~>: Φ uPred_ownM x =n=> y, ⌜Φ y uPred_ownM y.
Proof.
intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
intros n y ? Hown a.
......@@ -306,7 +306,7 @@ End classical.
we establish adequacy without axioms? Unfortunately not, because adequacy for
nnupd would imply double negation elimination, which is classical: *)
Lemma nnupd_dne φ: True (|=n=> ((¬¬ φ φ)): uPred M)%I.
Lemma nnupd_dne φ: True (|=n=> ⌜¬¬ φ φ⌝: uPred M)%I.
Proof.
rewrite /uPred_nnupd. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id.
......@@ -358,9 +358,9 @@ Proof.
eapply IHn; eauto.
Qed.
Lemma adequacy φ n : (True Nat.iter n (λ P, |=n=> P) ( φ)) ¬¬ φ.
Lemma adequacy φ n : (True Nat.iter n (λ P, |=n=> P) ⌜φ⌝) ¬¬ φ.
Proof.
cut ( x, {S n} x Nat.iter n (λ P, |=n=> P)%I ( φ)%I (S n) x ¬¬φ).
cut ( x, {S n} x Nat.iter n (λ P, |=n=> P)%I ⌜φ⌝%I (S n) x ¬¬φ).
{ intros help H. eapply (help ); eauto using ucmra_unit_validN.
eapply H; try unseal; eauto using ucmra_unit_validN. red; rewrite //=. }
destruct n.
......
......@@ -92,7 +92,7 @@ Section auth.
Proof. intros a1 a2. apply auth_own_mono. Qed.
Lemma auth_alloc_strong N E t (G : gset gname) :
(f t) φ t ={E}= γ, (γ G) auth_ctx γ N f φ auth_own γ (f t).
(f t) φ t ={E}= γ, ⌜γ G auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
iMod (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
......@@ -114,8 +114,8 @@ Section auth.
Lemma auth_acc E γ a :
auth_inv γ f φ auth_own γ a ={E}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={E}= auth_inv γ f φ auth_own γ b.
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
......@@ -130,8 +130,8 @@ Section auth.
Lemma auth_open E N γ a :
nclose N E
auth_ctx γ N f φ auth_own γ a ={E,EN}= t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={EN,E}= auth_own γ b.
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={EN,E}= auth_own γ b.
Proof.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
......
......@@ -55,7 +55,7 @@ Global Instance slice_persistent γ P : PersistentP (slice N γ P).
Proof. apply _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
......@@ -86,7 +86,7 @@ Proof.
Qed.
Lemma box_insert E f P Q :
box N f P ={E}= γ, f !! γ = None
box N f P ={E}= γ, f !! γ = None
slice N γ Q box N (<[γ:=false]> f) (Q P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
......
......@@ -69,7 +69,7 @@ Proof.
Qed.
Lemma fupd_mask_frame_r' E1 E2 Ef P :
E1 Ef (|={E1,E2}=> E2 Ef P) ={E1 Ef,E2 Ef}= P.
E1 Ef (|={E1,E2}=> E2 Ef P) ={E1 Ef,E2 Ef}= P.
Proof.
intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
iMod ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
......
......@@ -6,7 +6,7 @@ Import uPred.
(** Derived forms and lemmas about them. *)
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, (i nclose N) ownI i P)%I.
( i, i nclose N ownI i P)%I.
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
Definition inv {Σ i} := proj1_sig inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := proj2_sig inv_aux.
......
......@@ -86,10 +86,10 @@ Proof. rewrite !own_eq /own_def; apply _. Qed.
(* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris
assertion. However, the map_updateP_alloc does not suffice to show this. *)
Lemma own_alloc_strong a (G : gset gname) :
a True == γ, (γ G) own γ a.
a True == γ, ⌜γ G own γ a.
Proof.
intros Ha.
rewrite -(bupd_mono ( m, ( γ, γ G m = iRes_singleton γ a) uPred_ownM m)%I).
rewrite -(bupd_mono ( m, ⌜∃ γ, γ G m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite ownM_empty.
eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
......@@ -104,10 +104,10 @@ Proof.
Qed.
(** ** Frame preserving updates *)
Lemma own_updateP P γ a : a ~~>: P own γ a == a', P a' own γ a'.
Lemma own_updateP P γ a : a ~~>: P own γ a == a', P a' own γ a'.
Proof.
intros Ha. rewrite !own_eq.
rewrite -(bupd_mono ( m, ( a', m = iRes_singleton γ a' P a') uPred_ownM m)%I).
rewrite -(bupd_mono ( m, ⌜∃ a', m = iRes_singleton γ a' P a' uPred_ownM m)%I).
- eapply bupd_ownM_updateP, iprod_singleton_updateP;
first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
naive_solver.
......
......@@ -26,7 +26,7 @@ Section saved_prop.
Proof. rewrite /saved_prop_own; apply _. Qed.
Lemma saved_prop_alloc_strong x (G : gset gname) :
True == γ, (γ G) saved_prop_own γ x.
True == γ, ⌜γ G saved_prop_own γ x.
Proof. by apply own_alloc_strong. Qed.
Lemma saved_prop_alloc x : True == γ, saved_prop_own γ x.
......
......@@ -94,8 +94,8 @@ Section sts.
Lemma sts_accS E γ S T :
sts_inv γ φ sts_ownS γ S T ={E}= s,
(s S) φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
Proof.
iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own.
iDestruct "Hinv" as (s) "[>Hγ Hφ]".
......@@ -112,15 +112,15 @@ Section sts.
Lemma sts_acc E γ s0 T :
sts_inv γ φ sts_own γ s0 T ={E}= s,
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={E}= sts_inv γ φ sts_own γ s' T'.
Proof. by apply sts_accS. Qed.
Lemma sts_openS E N γ S T :
nclose N E
sts_ctx γ N φ sts_ownS γ S T ={E,EN}= s,
(s S) φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
s S φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof.
iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
......@@ -137,7 +137,7 @@ Section sts.
Lemma sts_open E N γ s0 T :
nclose N E
sts_ctx γ N φ sts_own γ s0 T ={E,EN}= s,
(sts.frame_steps T s0 s) φ s s' T',
(sts.steps (s, T) (s', T')) φ s' ={EN,E}= sts_own γ s' T'.
sts.frame_steps T s0 s φ s s' T',
sts.steps (s, T) (s', T') φ s' ={EN,E}= sts_own γ s' T'.
Proof. by apply sts_openS. Qed.
End sts.
......@@ -16,7 +16,7 @@ Section defs.
own tid (CoPset E, ).
Definition tl_inv (tid : thread_id) (N : namespace) (P : iProp Σ) : iProp Σ :=
( i, (i nclose N)
( i, i nclose N
inv tlN (P own tid (, GSet {[i]}) tl_own tid {[i]}))%I.
End defs.
......@@ -40,7 +40,7 @@ Section proofs.
Lemma tl_alloc : True == tid, tl_own tid .
Proof. by apply own_alloc. Qed.
Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 tl_own tid E2 (E1 E2).
Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 tl_own tid E2 E1 E2.
Proof.
rewrite /tl_own -own_op own_valid -coPset_disj_valid_op. by iIntros ([? _]).
Qed.
......
......@@ -56,9 +56,9 @@ Lemma ownE_empty : True ==∗ ownE ∅.
Proof. by rewrite (own_empty (coPset_disjUR) enabled_name). Qed.
Lemma ownE_op E1 E2 : E1 E2 ownE (E1 E2) ⊣⊢ ownE E1 ownE E2.
Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
Lemma ownE_disjoint E1 E2 : ownE E1 ownE E2 E1 E2.
Lemma ownE_disjoint E1 E2 : ownE E1 ownE E2 E1 E2.
Proof. rewrite /ownE -own_op own_valid. by iIntros (?%coPset_disj_valid_op). Qed.
Lemma ownE_op' E1 E2 : E1 E2 ownE (E1 E2) ⊣⊢ ownE E1 ownE E2.
Lemma ownE_op' E1 E2 : E1 E2 ownE (E1 E2) ⊣⊢ ownE E1 ownE E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownE_op|].
iIntros "HE". iDestruct (ownE_disjoint with "HE") as %?.
......@@ -71,9 +71,9 @@ Lemma ownD_empty : True ==∗ ownD ∅.
Proof. by rewrite (own_empty (gset_disjUR positive) disabled_name). Qed.
Lemma ownD_op E1 E2 : E1 E2 ownD (E1 E2) ⊣⊢ ownD E1 ownD E2.
Proof. intros. by rewrite /ownD -own_op gset_disj_union. Qed.
Lemma ownD_disjoint E1 E2 : ownD E1 ownD E2 E1 E2.
Lemma ownD_disjoint E1 E2 : ownD E1 ownD E2 E1 E2.
Proof. rewrite /ownD -own_op own_valid. by iIntros (?%gset_disj_valid_op). Qed.
Lemma ownD_op' E1 E2 : E1 E2 ownD (E1 E2) ⊣⊢ ownD E1 ownD E2.
Lemma ownD_op' E1 E2 : E1 E2 ownD (E1 E2) ⊣⊢ ownD E1 ownD E2.
Proof.
iSplit; [iIntros "[% ?]"; by iApply ownD_op|].
iIntros "HE". iDestruct (ownD_disjoint with "HE") as %?.
......@@ -85,7 +85,7 @@ Proof. rewrite ownD_disjoint. iIntros (?); set_solver. Qed.
Lemma invariant_lookup (I : gmap positive (iProp Σ)) i P :
own invariant_name ( (invariant_unfold <$> I : gmap _ _))
own invariant_name ( {[i := invariant_unfold P]})
Q, I !! i = Some Q (Q P).
Q, I !! i = Some Q (Q P).
Proof.
rewrite -own_op own_valid auth_validI /=. iIntros "[#HI #HvI]".
iDestruct "HI" as (I') "HI". rewrite gmap_equivI gmap_validI.
......@@ -123,7 +123,7 @@ Qed.
Lemma ownI_alloc φ P :
( E : gset positive, i, i E φ i)
wsat P == i, (φ i) wsat ownI i P.
wsat P == i, ⌜φ i wsat ownI i P.
Proof.
iIntros (Hfresh) "[Hw HP]". iDestruct "Hw" as (I) "[? HI]".
iMod (own_empty (gset_disjUR positive) disabled_name) as "HE".
......
......@@ -155,10 +155,9 @@ Definition uPred_bupd_aux : { x | x = @uPred_bupd_def }. by eexists. Qed.
Definition uPred_bupd {M} := proj1_sig uPred_bupd_aux M.
Definition uPred_bupd_eq : @uPred_bupd = @uPred_bupd_def := proj2_sig uPred_bupd_aux.
Notation "■ φ" := (uPred_pure φ%C%type)
(at level 20, right associativity) : uPred_scope.
Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
Notation "x ⊥ y" := (uPred_pure (x%C%type y%C%type)) : uPred_scope.
(* Latest notation *)
Notation "'⌜' φ '⌝'" := (uPred_pure φ%C%type)
(at level 1, φ at level 200, format "⌜ φ ⌝") : uPred_scope.
Notation "'False'" := (uPred_pure False) : uPred_scope.
Notation "'True'" := (uPred_pure True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope.
......@@ -317,13 +316,13 @@ Qed.
Global Instance bupd_proper : Proper (() ==> ()) (@uPred_bupd M) := ne_proper _.
(** Introduction and elimination rules *)
Lemma pure_intro φ P : φ P φ.
Lemma pure_intro φ P : φ P ⌜φ⌝.
Proof. by intros ?; unseal; split. Qed.
Lemma pure_elim φ Q R : (Q φ) (φ Q R) Q R.
Lemma pure_elim φ Q R : (Q ⌜φ⌝) (φ Q R) Q R.
Proof.
unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
Qed.
Lemma pure_forall_2 {A} (φ : A Prop) : ( x : A, φ x) ( x : A, φ x).
Lemma pure_forall_2 {A} (φ : A Prop) : ( x : A, ⌜φ x) ⌜∀ x : A, φ x.
Proof. by unseal. Qed.
Lemma and_elim_l P Q : P Q P.
......@@ -426,7 +425,7 @@ Qed.
Lemma always_idemp P : P P.
Proof. unseal; split=> n x ?? /=. by rewrite cmra_core_idemp. Qed.
Lemma always_pure_2 φ : φ φ.
Lemma always_pure_2 φ : ⌜φ⌝ ⌜φ⌝.
Proof. by unseal. Qed.
Lemma always_forall_2 {A} (Ψ : A uPred M) : ( a, Ψ a) ( a, Ψ a).
Proof. by unseal. Qed.
......@@ -542,7 +541,7 @@ Proof.
apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Lemma bupd_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x == y, Φ y uPred_ownM y.
x ~~>: Φ uPred_ownM x == y, ⌜Φ y uPred_ownM y.
Proof.
unseal=> Hup; split=> n x2 ? [x3 Hx] k yf ??.
destruct (Hup k (Some (x3 yf))) as (y&?&?); simpl in *.
......@@ -562,9 +561,9 @@ Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y)
Proof. by unseal. Qed.
(* Discrete *)
Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : a ⊣⊢ a.
Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : a ⊣⊢ ⌜✓ a.
Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
Lemma timeless_eq {A : ofeT} (a b : A) : Timeless a a b ⊣⊢ (a b).
Lemma timeless_eq {A : ofeT} (a b : A) : Timeless a a b ⊣⊢ a b.
Proof.
unseal=> ?. apply (anti_symm ()); split=> n x ?; by apply (timeless_iff n).
Qed.
......
......@@ -16,7 +16,7 @@ Instance subG_heapPreG {Σ} : subG heapΣ Σ → heapPreG Σ.
Proof. intros [? ?]%subG_inv. split; apply _. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, heap_ctx WP e {{ v, φ v }})
( `{heapG Σ}, heap_ctx WP e {{ v, ⌜φ v }})
adequate e σ φ.
Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
......
......@@ -85,7 +85,7 @@ Section heap.
Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 ⊣⊢ v1 = v2 l {q1+q2} v1.
l {q1} v1 l {q2} v2 ⊣⊢ v1 = v2 l {q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_True // left_id. }
......@@ -96,15 +96,15 @@ Section heap.
Qed.
Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 v1 = v2 l {q1+q2} v1.
l {q1} v1 l {q2} v2 v1 = v2 l {q1+q2} v1.
Proof. by rewrite heap_mapsto_op. Qed.
Lemma heap_mapsto_op_half l q v1 v2 :
l {q/2} v1 l {q/2} v2 ⊣⊢ v1 = v2 l {q} v1.
l {q/2} v1 l {q/2} v2 ⊣⊢ v1 = v2 l {q} v1.
Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
</