Commit a3ef69f2 authored by Robbert Krebbers's avatar Robbert Krebbers

Better notations for raw view shifts.

parent 652a3623
......@@ -310,8 +310,12 @@ Notation "▷ P" := (uPred_later P)
(at level 20, right associativity) : uPred_scope.
Infix "≡" := uPred_eq : uPred_scope.
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Notation "|==r> Q" := (uPred_rvs Q)
(at level 99, Q at level 200, format "|==r> Q") : uPred_scope.
Notation "|=r=> Q" := (uPred_rvs Q)
(at level 99, Q at level 200, format "|=r=> Q") : uPred_scope.
Notation "P =r=> Q" := (P |=r=> Q)
(at level 99, Q at level 200, only parsing) : C_scope.
Notation "P =r=★ Q" := (P - |=r=> Q)%I
(at level 99, Q at level 200, format "P =r=★ Q") : uPred_scope.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
Instance: Params (@uPred_iff) 1.
......@@ -1167,27 +1171,27 @@ Proof.
Qed.
(* Viewshifts *)
Lemma rvs_intro P : P |==r> P.
Lemma rvs_intro P : P =r=> P.
Proof.
unseal. split=> n x ? HP k yf ?; exists x; split; first done.
apply uPred_closed with n; eauto using cmra_validN_op_l.
Qed.
Lemma rvs_mono P Q : (P Q) (|==r> P) |==r> Q.
Lemma rvs_mono P Q : (P Q) (|=r=> P) =r=> Q.
Proof.
unseal. intros HPQ; split=> n x ? HP k yf ??.
destruct (HP k yf) as (x'&?&?); eauto.
exists x'; split; eauto using uPred_in_entails, cmra_validN_op_l.
Qed.
Lemma rvs_timeless P : TimelessP P P |==r> P.
Lemma rvs_timeless P : TimelessP P P =r=> P.
Proof.
unseal. rewrite timelessP_spec=> HP.
split=> -[|n] x ? HP' k yf ??; first lia.
exists x; split; first done.
apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
Lemma rvs_trans P : (|==r> |==r> P) |==r> P.
Lemma rvs_trans P : (|=r=> |=r=> P) =r=> P.
Proof. unseal; split; naive_solver. Qed.
Lemma rvs_frame_r P R : (|==r> P) R |==r> P R.
Lemma rvs_frame_r P R : (|=r=> P) R =r=> P R.
Proof.
unseal; split; intros n x ? (x1&x2&Hx&HP&?) k yf ??.
destruct (HP k (x2 yf)) as (x'&?&?); eauto.
......@@ -1197,7 +1201,7 @@ Proof.
apply uPred_closed with n; eauto 3 using cmra_validN_op_l, cmra_validN_op_r.
Qed.
Lemma rvs_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x |==r> y, Φ y uPred_ownM y.
x ~~>: Φ uPred_ownM x =r=> y, Φ y uPred_ownM y.
Proof.
unseal=> Hup; split=> -[|n] x2 ? [x3 Hx] [|k] yf ??; try lia.
destruct (Hup (S k) (Some (x3 yf))) as (y&?&?); simpl in *.
......@@ -1211,17 +1215,15 @@ Global Instance rvs_mono' : Proper ((⊢) ==> (⊢)) (@uPred_rvs M).
Proof. intros P Q; apply rvs_mono. Qed.
Global Instance rvs_flip_mono' : Proper (flip () ==> flip ()) (@uPred_rvs M).
Proof. intros P Q; apply rvs_mono. Qed.
Lemma rvs_strip_rvs P Q : (P |==r> Q) (|==r> P) (|==r> Q).
Proof. move=>->. by rewrite rvs_trans. Qed.
Lemma rvs_frame_l R Q : (R |==r> Q) |==r> R Q.
Lemma rvs_frame_l R Q : (R |=r=> Q) =r=> R Q.
Proof. rewrite !(comm _ R); apply rvs_frame_r. Qed.
Lemma rvs_wand_l P Q : (P - Q) (|==r> P) |==r> Q.
Lemma rvs_wand_l P Q : (P - Q) (|=r=> P) =r=> Q.
Proof. by rewrite rvs_frame_l wand_elim_l. Qed.
Lemma rvs_wand_r P Q : (|==r> P) (P - Q) |==r> Q.
Lemma rvs_wand_r P Q : (|=r=> P) (P - Q) =r=> Q.
Proof. by rewrite rvs_frame_r wand_elim_r. Qed.
Lemma rvs_sep P Q : (|==r> P) (|==r> Q) |==r> P Q.
Lemma rvs_sep P Q : (|=r=> P) (|=r=> Q) =r=> P Q.
Proof. by rewrite rvs_frame_r rvs_frame_l rvs_trans. Qed.
Lemma rvs_ownM_update x y : x ~~> y uPred_ownM x |==r> uPred_ownM y.
Lemma rvs_ownM_update x y : x ~~> y uPred_ownM x |=r=> uPred_ownM y.
Proof.
intros; rewrite (rvs_ownM_updateP _ (y =)); last by apply cmra_update_updateP.
by apply rvs_mono, exist_elim=> y'; apply pure_elim_l=> ->.
......
......@@ -17,7 +17,7 @@ Global Instance from_assumption_always_r P Q :
FromAssumption true P Q FromAssumption true P ( Q).
Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
Global Instance from_assumption_rvs p P Q :
FromAssumption p P Q FromAssumption p P (|==r> Q)%I.
FromAssumption p P Q FromAssumption p P (|=r=> Q)%I.
Proof. rewrite /FromAssumption=>->. apply rvs_intro. Qed.
Class IntoPure (P : uPred M) (φ : Prop) := into_pure : P φ.
......@@ -38,7 +38,7 @@ Global Instance from_pure_eq {A : cofeT} (a b : A) : FromPure (a ≡ b) (a ≡ b
Proof. intros ->. apply eq_refl. Qed.
Global Instance from_pure_valid {A : cmraT} (a : A) : FromPure ( a) ( a).
Proof. intros ?. by apply valid_intro. Qed.
Global Instance from_pure_rvs P φ : FromPure P φ FromPure (|==r> P) φ.
Global Instance from_pure_rvs P φ : FromPure P φ FromPure (|=r=> P) φ.
Proof. intros ??. by rewrite -rvs_intro (from_pure P). Qed.
Class IntoPersistentP (P Q : uPred M) := into_persistentP : P Q.
......@@ -111,7 +111,7 @@ Proof. apply and_elim_r', impl_wand. Qed.
Global Instance into_wand_always R P Q : IntoWand R P Q IntoWand ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
Global Instance into_wand_rvs R P Q :
IntoWand R P Q IntoWand R (|==r> P) (|==r> Q) | 100.
IntoWand R P Q IntoWand R (|=r=> P) (|=r=> Q) | 100.
Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite rvs_wand_r. Qed.
Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 Q2 P.
......@@ -144,7 +144,7 @@ Global Instance from_sep_later P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.
Global Instance from_sep_rvs P Q1 Q2 :
FromSep P Q1 Q2 FromSep (|==r> P) (|==r> Q1) (|==r> Q2).
FromSep P Q1 Q2 FromSep (|=r=> P) (|=r=> Q1) (|=r=> Q2).
Proof. rewrite /FromSep=><-. apply rvs_sep. Qed.
Global Instance from_sep_ownM (a b : M) :
......@@ -293,7 +293,7 @@ Global Instance frame_forall {A} R (Φ Ψ : A → uPred M) :
( a, Frame R (Φ a) (Ψ a)) Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Global Instance frame_rvs R P Q : Frame R P Q Frame R (|==r> P) (|==r> Q).
Global Instance frame_rvs R P Q : Frame R P Q Frame R (|=r=> P) (|=r=> Q).
Proof. rewrite /Frame=><-. by rewrite rvs_frame_l. Qed.
Class FromOr (P Q1 Q2 : uPred M) := from_or : Q1 Q2 P.
......@@ -301,7 +301,7 @@ Global Arguments from_or : clear implicits.
Global Instance from_or_or P1 P2 : FromOr (P1 P2) P1 P2.
Proof. done. Qed.
Global Instance from_or_rvs P Q1 Q2 :
FromOr P Q1 Q2 FromOr (|==r> P) (|==r> Q1) (|==r> Q2).
FromOr P Q1 Q2 FromOr (|=r=> P) (|=r=> Q1) (|=r=> Q2).
Proof. rewrite /FromOr=><-. apply or_elim; apply rvs_mono; auto with I. Qed.
Class IntoOr P Q1 Q2 := into_or : P Q1 Q2.
......@@ -318,7 +318,7 @@ Global Arguments from_exist {_} _ _ {_}.
Global Instance from_exist_exist {A} (Φ: A uPred M): FromExist ( a, Φ a) Φ.
Proof. done. Qed.
Global Instance from_exist_rvs {A} P (Φ : A uPred M) :
FromExist P Φ FromExist (|==r> P) (λ a, |==r> Φ a)%I.
FromExist P Φ FromExist (|=r=> P) (λ a, |=r=> Φ a)%I.
Proof.
rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
......@@ -337,7 +337,7 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
Class TimelessElim (Q : uPred M) :=
timeless_elim `{!TimelessP P} : P (P - Q) Q.
Global Instance timeless_elim_rvs Q : TimelessElim (|==r> Q).
Global Instance timeless_elim_rvs Q : TimelessElim (|=r=> Q).
Proof.
intros P ?. by rewrite (rvs_timeless P) rvs_frame_r wand_elim_r rvs_trans.
Qed.
......
......@@ -465,7 +465,7 @@ Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
Global Arguments into_assert _ _ _ {_}.
Lemma into_assert_default P Q : IntoAssert P Q P.
Proof. by rewrite /IntoAssert wand_elim_r. Qed.
Global Instance to_assert_rvs P Q : IntoAssert P (|==r> Q) (|==r> P).
Global Instance to_assert_rvs P Q : IntoAssert P (|=r=> Q) (|=r=> P).
Proof. by rewrite /IntoAssert rvs_frame_r wand_elim_r rvs_trans. Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
......
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