Commit 243fdd13 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Validity coercion from iProp to Prop. Magic wand that works at the Prop level.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
parent c1951443
......@@ -8,13 +8,13 @@ CMRA structure on uPred. *)
Section cmra.
Context {M : ucmraT}.
Instance uPred_valid : Valid (uPred M) := λ P, n x, {n} x P n x.
Instance uPred_validN : ValidN (uPred M) := λ n P,
Instance uPred_valid_inst : Valid (uPred M) := λ P, n x, {n} x P n x.
Instance uPred_validN_inst : ValidN (uPred M) := λ n P,
n' x, n' n {n'} x P n' x.
Instance uPred_op : Op (uPred M) := uPred_sep.
Instance uPred_pcore : PCore (uPred M) := λ _, Some True%I.
Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN n).
Instance uPred_validN_ne n : Proper (dist n ==> iff) (uPred_validN_inst n).
Proof. intros P Q HPQ; split=> H n' x ??; by apply HPQ, H. Qed.
Lemma uPred_validN_alt n (P : uPred M) : {n} P P {n} True%I.
......@@ -467,7 +467,7 @@ Section gset.
Proof. apply: big_opS_delete. Qed.
Lemma big_sepS_elem_of Φ X x : x X ([ set] y X, Φ y) Φ x.
Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
Proof. intros. apply uPred_included. by apply: big_opS_elem_of. Qed.
Lemma big_sepS_singleton Φ x : ([ set] y {[ x ]}, Φ y) Φ x.
Proof. apply: big_opS_singleton. Qed.
......
......@@ -67,10 +67,10 @@ Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
Proof. intros; apply impl_elim with Q; auto. Qed.
Lemma impl_elim_r' P Q R : (Q P R) P Q R.
Proof. intros; apply impl_elim with P; auto. Qed.
Lemma impl_entails P Q : (True P Q) P Q.
Lemma impl_entails P Q : (P Q)%I P Q.
Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
Lemma entails_impl P Q : (P Q) True P Q.
Proof. auto using impl_intro_l. Qed.
Lemma entails_impl P Q : (P Q) (P Q)%I.
Proof. intro. apply impl_intro_l. auto. Qed.
Lemma and_mono P P' Q Q' : (P Q) (P' Q') P P' Q Q'.
Proof. auto. Qed.
......@@ -308,12 +308,12 @@ Global Instance iff_proper :
Lemma iff_refl Q P : Q P P.
Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
Lemma iff_equiv P Q : (True P Q) (P Q).
Lemma iff_equiv P Q : (P Q)%I (P Q).
Proof.
intros HPQ; apply (anti_symm ());
apply impl_entails; rewrite HPQ /uPred_iff; auto.
apply impl_entails; rewrite /uPred_valid HPQ /uPred_iff; auto.
Qed.
Lemma equiv_iff P Q : (P Q) True P Q.
Lemma equiv_iff P Q : (P Q) (P Q)%I.
Proof. intros ->; apply iff_refl. Qed.
Lemma internal_eq_iff P Q : P Q P Q.
Proof.
......@@ -362,13 +362,13 @@ Proof. intros ->; apply sep_elim_l. Qed.
Lemma sep_elim_r' P Q R : (Q R) P Q R.
Proof. intros ->; apply sep_elim_r. Qed.
Hint Resolve sep_elim_l' sep_elim_r'.
Lemma sep_intro_True_l P Q R : (True P) (R Q) R P Q.
Lemma sep_intro_True_l P Q R : P%I (R Q) R P Q.
Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
Lemma sep_intro_True_r P Q R : (R P) (True Q) R P Q.
Lemma sep_intro_True_r P Q R : (R P) Q%I R P Q.
Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
Lemma sep_elim_True_l P Q R : (True P) (P R Q) R Q.
Lemma sep_elim_True_l P Q R : P (P R Q) R Q.
Proof. by intros HP; rewrite -HP left_id. Qed.
Lemma sep_elim_True_r P Q R : (True P) (R P Q) R Q.
Lemma sep_elim_True_r P Q R : P (R P Q) R Q.
Proof. by intros HP; rewrite -HP right_id. Qed.
Lemma wand_intro_l P Q R : (Q P R) P Q - R.
Proof. rewrite comm; apply wand_intro_r. Qed.
......@@ -392,14 +392,14 @@ Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
Lemma wand_True P : (True - P) P.
Proof.
apply (anti_symm _); last by auto using wand_intro_l.
eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
eapply sep_elim_True_l; last by apply wand_elim_r. done.
Qed.
Lemma wand_entails P Q : (True P - Q) P Q.
Lemma wand_entails P Q : (P - Q)%I P Q.
Proof.
intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
Qed.
Lemma entails_wand P Q : (P Q) True P - Q.
Proof. auto using wand_intro_l. Qed.
Lemma entails_wand P Q : (P Q) (P - Q)%I.
Proof. intro. apply wand_intro_l. auto. Qed.
Lemma wand_curry P Q R : (P - Q - R) (P Q - R).
Proof.
apply (anti_symm _).
......@@ -636,7 +636,7 @@ Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
Lemma ownM_empty' : uPred_ownM True.
Proof. apply (anti_symm _); auto using ownM_empty. Qed.
Proof. apply (anti_symm _); first by auto. apply ownM_empty. Qed.
Lemma always_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
intros; apply (anti_symm _); first by apply:always_elim.
......@@ -781,4 +781,5 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
Lemma always_entails_r P Q `{!PersistentP Q} : (P Q) P P Q.
Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
End derived.
End uPred_derived.
......@@ -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 φ: (|=n=> ¬¬ φ φ⌝: uPred M)%I.
Proof.
rewrite /uPred_nnupd. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id.
......@@ -358,7 +358,7 @@ Proof.
eapply IHn; eauto.
Qed.
Lemma adequacy φ n : (True Nat.iter n (λ P, |=n=> P) ⌜φ⌝) ¬¬ φ.
Lemma adequacy φ n : Nat.iter n (λ P, |=n=> P)%I ⌜φ⌝%I ¬¬ φ.
Proof.
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.
......
......@@ -109,7 +109,7 @@ Section auth.
iMod (auth_alloc_strong N E t with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : True == auth_own γ .
Lemma auth_empty γ : (|==> auth_own γ )%I.
Proof. by rewrite /auth_own -own_empty. Qed.
Lemma auth_acc E γ a :
......
......@@ -70,7 +70,7 @@ Proof.
Qed.
Lemma box_own_agree γ Q1 Q2 :
(box_own_prop γ Q1 box_own_prop γ Q2) (Q1 Q2).
box_own_prop γ Q1 box_own_prop γ Q2 (Q1 Q2).
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_r.
rewrite option_validI /= agree_validI agree_equivI later_equivI /=.
......@@ -78,7 +78,7 @@ Proof.
iRewrite "HQ". by rewrite iProp_fold_unfold.
Qed.
Lemma box_alloc : True box N True.
Lemma box_alloc : box N True%I.
Proof.
iIntros; iExists (λ _, True)%I; iSplit.
- iNext. by rewrite big_sepM_empty.
......
......@@ -50,7 +50,7 @@ Section proofs.
iMod (inv_alloc N _ (P own γ 1%Qp)%I with "[HP]"); eauto.
Qed.
Lemma cinv_cancel E N γ P : N E cinv N γ P cinv_own γ 1 ={E}= P.
Lemma cinv_cancel E N γ P : N E cinv N γ P - cinv_own γ 1 ={E}= P.
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose"; first iApply "Hclose"; eauto.
......@@ -59,7 +59,7 @@ Section proofs.
Lemma cinv_open E N γ p P :
N E
cinv N γ P cinv_own γ p ={E,E∖↑N}= P cinv_own γ p ( P ={E∖↑N,E}= True).
cinv N γ P - cinv_own γ p ={E,E∖↑N}= P cinv_own γ p ( P ={E∖↑N,E}= True).
Proof.
rewrite /cinv. iIntros (?) "#Hinv Hγ".
iInv N as "[$|>Hγ']" "Hclose".
......
......@@ -13,13 +13,13 @@ Module savedprop. Section savedprop.
Context (sprop : Type) (saved : sprop iProp iProp).
Hypothesis sprop_persistent : i P, PersistentP (saved i P).
Hypothesis sprop_alloc_dep :
(P : sprop iProp), True == ( i, saved i (P i)).
(P : sprop iProp), (|==> ( i, saved i (P i)))%I.
Hypothesis sprop_agree : i P Q, saved i P saved i Q (P Q).
(** A bad recursive reference: "Assertion with name [i] does not hold" *)
Definition A (i : sprop) : iProp := P, ¬ P saved i P.
Lemma A_alloc : True == i, saved i (A i).
Lemma A_alloc : (|==> i, saved i (A i))%I.
Proof. by apply sprop_alloc_dep. Qed.
Lemma saved_NA i : saved i (A i) ¬ A i.
......@@ -85,7 +85,7 @@ Module inv. Section inv.
Context (gname : Type).
Context (start finished : gname iProp).
Hypothesis sts_alloc : True fupd M0 ( γ, start γ).
Hypothesis sts_alloc : fupd M0 ( γ, start γ).
Hypotheses start_finish : γ, start γ fupd M0 (finished γ).
Hypothesis finished_not_start : γ, start γ finished γ False.
......@@ -93,7 +93,7 @@ Module inv. Section inv.
Hypothesis finished_dup : γ, finished γ finished γ finished γ.
(** We assume that we cannot update to false. *)
Hypothesis consistency : ¬ (True fupd M1 False).
Hypothesis consistency : ¬ (fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
Lemma inv_open' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
......@@ -110,7 +110,7 @@ Module inv. Section inv.
intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
Lemma fupd_frame_r E P Q : (fupd E P Q) fupd E (P Q).
Lemma fupd_frame_r E P Q : fupd E P Q fupd E (P Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
Global Instance elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
......@@ -133,7 +133,7 @@ Module inv. Section inv.
i, inv i (start γ (finished γ P)).
Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
Lemma saved_alloc (P : gname iProp) : True fupd M1 ( γ, saved γ (P γ)).
Lemma saved_alloc (P : gname iProp) : fupd M1 ( γ, saved γ (P γ)).
Proof.
iIntros "". iMod (sts_alloc) as (γ) "Hs".
iMod (inv_alloc (start γ (finished γ (P γ))) with "[Hs]") as (i) "#Hi".
......@@ -166,7 +166,7 @@ Module inv. Section inv.
Definition A i : iProp := P, ¬P saved i P.
Global Instance A_persistent i : PersistentP (A i) := _.
Lemma A_alloc : True fupd M1 ( i, saved i (A i)).
Lemma A_alloc : fupd M1 ( i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
Lemma saved_NA i : saved i (A i) ¬A i.
......
......@@ -22,7 +22,7 @@ Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
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)
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.
Notation "|={ E }=> Q" := (fupd E E Q)
......@@ -31,7 +31,7 @@ Notation "|={ E }=> Q" := (fupd E E Q)
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)
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Section fupd.
......@@ -56,13 +56,13 @@ Proof. rewrite fupd_eq. iIntros ">H [Hw HE]". iApply "H"; by iFrame. Qed.
Lemma bupd_fupd E P : (|==> P) ={E}= P.
Proof. rewrite fupd_eq /fupd_def. by iIntros ">? [$ $] !> !>". Qed.
Lemma fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) ={E1,E2}= Q.
Lemma fupd_mono E1 E2 P Q : (P Q) (|={E1,E2}=> P) |={E1,E2}=> Q.
Proof.
rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
rewrite -HPQ. by iApply "HP".
Qed.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}= P.
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) |={E1,E3}=> P.
Proof.
rewrite fupd_eq /fupd_def. iIntros "HP HwE".
iMod ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
......@@ -89,7 +89,7 @@ Proof. intros P Q; apply fupd_mono. Qed.
Lemma fupd_intro E P : P ={E}= P.
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
Lemma fupd_intro_mask' E1 E2 : E2 E1 True |={E1,E2}=> |={E2,E1}=> True.
Lemma fupd_intro_mask' E1 E2 : E2 E1 (|={E1,E2}=> |={E2,E1}=> True)%I.
Proof. exact: fupd_intro_mask. Qed.
Lemma fupd_except_0 E1 E2 P : (|={E1,E2}=> P) ={E1,E2}= P.
Proof. by rewrite {1}(fupd_intro E2 P) except_0_fupd fupd_trans. Qed.
......
......@@ -68,9 +68,9 @@ Proof.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
Qed.
Lemma own_valid_2 γ a1 a2 : own γ a1 own γ a2 - (a1 a2).
Lemma own_valid_2 γ a1 a2 : own γ a1 - own γ a2 - (a1 a2).
Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 own γ a2 - own γ a3 - (a1 a2 a3).
Lemma own_valid_3 γ a1 a2 a3 : own γ a1 - own γ a2 - own γ a3 - (a1 a2 a3).
Proof. do 2 apply wand_intro_r. by rewrite -!own_op own_valid. Qed.
Lemma own_valid_r γ a : own γ a own γ a a.
Proof. apply (uPred.always_entails_r _ _). apply own_valid. Qed.
......@@ -86,20 +86,20 @@ 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 (|==> γ, ⌜γ G own γ a)%I.
Proof.
intros Ha.
rewrite -(bupd_mono ( m, γ, γ G m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite ownM_empty.
- rewrite /uPred_valid ownM_empty.
eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
naive_solver.
- apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
Qed.
Lemma own_alloc a : a True == γ, own γ a.
Lemma own_alloc a : a (|==> γ, own γ a)%I.
Proof.
intros Ha. rewrite (own_alloc_strong a ) //; [].
intros Ha. rewrite /uPred_valid (own_alloc_strong a ) //; [].
apply bupd_mono, exist_mono=>?. eauto with I.
Qed.
......@@ -121,10 +121,10 @@ Proof.
by apply bupd_mono, exist_elim=> a''; apply pure_elim_l=> ->.
Qed.
Lemma own_update_2 γ a1 a2 a' :
a1 a2 ~~> a' own γ a1 own γ a2 == own γ a'.
a1 a2 ~~> a' own γ a1 - own γ a2 == own γ a'.
Proof. intros. apply wand_intro_r. rewrite -own_op. by apply own_update. Qed.
Lemma own_update_3 γ a1 a2 a3 a' :
a1 a2 a3 ~~> a' own γ a1 own γ a2 - own γ a3 == own γ a'.
a1 a2 a3 ~~> a' own γ a1 - own γ a2 - own γ a3 == own γ a'.
Proof. intros. do 2 apply wand_intro_r. rewrite -!own_op. by apply own_update. Qed.
End global.
......@@ -138,9 +138,9 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_empty A `{inG Σ (A:ucmraT)} γ : True == own γ .
Lemma own_empty A `{inG Σ (A:ucmraT)} γ : (|==> own γ )%I.
Proof.
rewrite ownM_empty !own_eq /own_def.
rewrite /uPred_valid ownM_empty !own_eq /own_def.
apply bupd_ownM_update, iprod_singleton_update_empty.
apply (alloc_unit_singleton_update (cmra_transport inG_prf )); last done.
- apply cmra_transport_valid, ucmra_unit_valid.
......
......@@ -26,10 +26,10 @@ 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.
(|==> γ, ⌜γ G saved_prop_own γ x)%I.
Proof. by apply own_alloc_strong. Qed.
Lemma saved_prop_alloc x : True == γ, saved_prop_own γ x.
Lemma saved_prop_alloc x : (|==> γ, saved_prop_own γ x)%I.
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ x y :
......
......@@ -37,7 +37,7 @@ Section proofs.
Global Instance tl_inv_persistent tid N P : PersistentP (tl_inv tid N P).
Proof. rewrite /tl_inv; apply _. Qed.
Lemma tl_alloc : True == tid, tl_own tid .
Lemma tl_alloc : (|==> tid, tl_own tid )%I.
Proof. by apply own_alloc. Qed.
Lemma tl_own_disjoint tid E1 E2 : tl_own tid E1 tl_own tid E2 E1 E2.
......@@ -71,7 +71,7 @@ Section proofs.
Lemma tl_inv_open tid tlE E N P :
tlN tlE N E
tl_inv tid N P tl_own tid E ={tlE}= P tl_own tid (E∖↑N)
tl_inv tid N P - tl_own tid E ={tlE}= P tl_own tid (E∖↑N)
( P tl_own tid (E∖↑N) ={tlE}= tl_own tid E).
Proof.
rewrite /tl_inv. iIntros (??) "#Htlinv Htoks".
......
......@@ -13,10 +13,10 @@ 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.
Notation "P ={ E1 , E2 }=> Q" := (True P ={E1,E2}=> 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.
Notation "P ={ E }=> Q" := (True P ={E}=> Q)%I
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.
......
......@@ -52,8 +52,8 @@ Qed.
Global Instance ownI_persistent i P : PersistentP (ownI i P).
Proof. rewrite /ownI. apply _. Qed.
Lemma ownE_empty : True == ownE .
Proof. by rewrite (own_empty (coPset_disjUR) enabled_name). Qed.
Lemma ownE_empty : (|==> ownE )%I.
Proof. by rewrite /uPred_valid (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.
......@@ -67,8 +67,8 @@ Qed.
Lemma ownE_singleton_twice i : ownE {[i]} ownE {[i]} False.
Proof. rewrite ownE_disjoint. iIntros (?); set_solver. Qed.
Lemma ownD_empty : True == ownD .
Proof. by rewrite (own_empty (gset_disjUR positive) disabled_name). Qed.
Lemma ownD_empty : (|==> ownD )%I.
Proof. by rewrite /uPred_valid (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.
......
......@@ -188,6 +188,10 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q)
Notation "P ==∗ Q" := (P - |==> Q)%I
(at level 99, Q at level 200, format "P ==∗ Q") : uPred_scope.
Coercion uPred_valid {M} (P : uPred M) : Prop := True%I P.
Notation "P -∗ Q" := (P Q)
(at level 99, Q at level 200, right associativity, only parsing) : C_scope.
Module uPred_primitive.
Definition unseal :=
(uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
......@@ -314,6 +318,10 @@ Proof.
exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
Qed.
Global Instance bupd_proper : Proper (() ==> ()) (@uPred_bupd M) := ne_proper _.
Global Instance uPred_valid_proper : Proper (() ==> iff) (@uPred_valid M).
Proof. solve_proper. Qed.
Global Instance uPred_valid_mono : Proper (() ==> impl) (@uPred_valid M).
Proof. solve_proper. Qed.
(** Introduction and elimination rules *)
Lemma pure_intro φ P : φ P ⌜φ⌝.
......@@ -355,7 +363,7 @@ Proof. unseal; split=> n x ??; by exists a. Qed.
Lemma exist_elim {A} (Φ : A uPred M) Q : ( a, Φ a Q) ( a, Φ a) Q.
Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
Lemma internal_eq_refl {A : ofeT} (a : A) : True a a.
Lemma internal_eq_refl {A : ofeT} (a : A) : uPred_valid (M:=M) (a a).
Proof. unseal; by split=> n x ??; simpl. Qed.
Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A uPred M) P
{HΨ : n, Proper (dist n ==> dist n) Ψ} : (P a b) (P Ψ a) P Ψ b.
......@@ -491,7 +499,7 @@ Lemma always_ownM_core (a : M) : uPred_ownM a ⊢ □ uPred_ownM (core a).
Proof.
split=> n x /=; unseal; intros Hx. simpl. by apply cmra_core_monoN.
Qed.
Lemma ownM_empty : True uPred_ownM .
Lemma ownM_empty : uPred_valid (M:=M) (uPred_ownM ).
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
Lemma later_ownM a : uPred_ownM a b, uPred_ownM b (a b).
Proof.
......@@ -506,7 +514,7 @@ Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
Proof.
unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
Qed.
Lemma cmra_valid_intro {A : cmraT} (a : A) : a True a.
Lemma cmra_valid_intro {A : cmraT} (a : A) : a uPred_valid (M:=M) ( a).
Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
Lemma cmra_valid_elim {A : cmraT} (a : A) : ¬ {0} a a False.
Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
......
From iris.base_logic Require Export primitive.
From iris.base_logic Require Export primitive derived.
Import uPred_entails uPred_primitive.
Section adequacy.
Context {M : ucmraT}.
(** Consistency and adequancy statements *)
Lemma soundness φ n : (True Nat.iter n (λ P, |==> P) (@uPred_pure M φ)) φ.
Lemma soundness φ n : (Nat.iter n (λ P, |==> P) (@uPred_pure M φ))%I φ.
Proof.
cut ( x, {n} x Nat.iter n (λ P, |==> P)%I (@uPred_pure M φ) n x φ).
{ intros help H. eapply (help ); eauto using ucmra_unit_validN.
......@@ -16,9 +16,9 @@ Proof.
Qed.
Corollary consistency_modal n :
¬ (True Nat.iter n (λ P, |==> P) (False : uPred M)).
¬ (Nat.iter n (λ P, |==> P) (False : uPred M))%I.
Proof. exact (soundness False n). Qed.
Corollary consistency : ¬ (True False : uPred M).
Corollary consistency : ¬ (False : uPred M)%I.
Proof. exact (consistency_modal 0). Qed.
End adequacy.
......@@ -189,7 +189,7 @@ Proof.
- iExists γ, P, R2, i2. iFrame; auto.
Qed.
Lemma recv_weaken l P1 P2 : (P1 - P2) recv l P1 - recv l P2.
Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2.
Proof.
rewrite /recv.
iIntros "HP HP1"; iDestruct "HP1" as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
......
......@@ -38,7 +38,7 @@ Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
(* Allocation *)
Lemma wsat_alloc `{invPreG Σ} : True == _ : invG Σ, wsat ownE .
Lemma wsat_alloc `{invPreG Σ} : (|==> _ : invG Σ, wsat ownE )%I.
Proof.
iIntros.
iMod (own_alloc ( ( : gmap _ _))) as (γI) "HI"; first done.
......@@ -50,7 +50,7 @@ Proof.
Qed.
Lemma iris_alloc `{irisPreG' Λstate Σ} σ :
True == _ : irisG' Λstate Σ, wsat ownE ownP_auth σ ownP σ.
(|==> _ : irisG' Λstate Σ, wsat ownE ownP_auth σ ownP σ)%I.
Proof.
iIntros.
iMod wsat_alloc as (?) "[Hws HE]".
......
......@@ -7,29 +7,17 @@ Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
( (P - WP e @ E {{ Φ }}))%I.
Instance: Params (@ht) 4.
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : uPred_scope.
Notation "{{ P } } e {{ Φ } }" := (ht P e%E Φ)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : uPred_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (True ht E P e%E Φ)
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e @ E {{ Φ } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (True ht P e%E Φ)
Notation "{{ P } } e {{ Φ } }" := (ht P%I e%E Φ%I)
(at level 20, P, e, Φ at level 200,
format "{{ P } } e {{ Φ } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e @ E {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht P e%E (λ v, Q))
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : uPred_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (True ht E P e%E (λ v, Q))
Notation "{{ P } } e @ E {{ v , Q } }" := (ht 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.
Notation "{{ P } } e {{ v , Q } }" := (True ht P e%E (λ v, Q))
Notation "{{ P } } e {{ v , Q } }" := (ht P%I e%E (λ v, Q)%I)
(at level 20, P, e, Q at level 200,
format "{{ P } } e {{ v , Q } }") : C_scope.
......
......@@ -89,20 +89,20 @@ Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
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.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
( Φ : _ uPred _,
P ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
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.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P (Q - Φ pat%V) - WP e {{ Φ }})
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e {{ Φ }})
(at level 20,
format "{{{ P } } } e {{{ RET pat ; Q } } }") : C_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
( Φ : _ uPred _, P (Q - Φ pat%V) - WP e @ E {{ Φ }})
( Φ : _ uPred _, P - (Q - Φ pat%V) - WP e @ E {{ Φ }})
(at level 20,
format "{{{ P } } } e @ E {{{ RET pat ; Q } } }") : C_scope.
......@@ -276,7 +276,7 @@ Lemma wp_frame_step_r' E e Φ R :
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.
Lemma wp_wand E e Φ Ψ :
WP e @ E {{ Φ }} ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}.
WP e @