pviewshifts.v 6.63 KB
Newer Older
1 2
Require Export program_logic.ownership prelude.co_pset.
Require Import program_logic.wsat.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5 6 7 8 9
Local Hint Extern 10 (_  _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
Local Hint Extern 10 ({_} _) =>
  repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end;
  solve_validN.

10
Program Definition pvs {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
11 12 13 14 15
  {| uPred_holds n r1 :=  rf k Ef σ,
       1 < k  n  (E1  E2)  Ef =  
       wsat k (E1  Ef) σ (r1  rf) 
        r2, P k r2  wsat k (E2  Ef) σ (r2  rf) |}.
Next Obligation.
16
  intros Λ Σ E1 E2 P r1 r2 n HP Hr rf k Ef σ ?? Hwsat; simpl in *.
Robbert Krebbers's avatar
Robbert Krebbers committed
17 18
  apply HP; auto. by rewrite (dist_le _ _ _ _ Hr); last lia.
Qed.
19
Next Obligation. intros Λ Σ E1 E2 P r rf k Ef σ; simpl in *; lia. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Next Obligation.
21
  intros Λ Σ E1 E2 P r1 r2 n1 n2 HP [r3 ?] Hn ? rf k Ef σ ?? Hws; setoid_subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23
  destruct (HP (r3rf) k Ef σ) as (r'&?&Hws'); rewrite ?(associative op); auto.
  exists (r'  r3); rewrite -(associative _); split; last done.
24
  apply uPred_weaken with r' k; eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
25
Qed.
26 27
Arguments pvs {_ _} _ _ _%I : simpl never.
Instance: Params (@pvs) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
28 29

Section pvs.
30 31 32
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types m : iGst Λ Σ.
33
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
34

35
Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38 39 40
Proof.
  intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
    destruct (HP rf k Ef σ) as (r2&?&?); auto;
    exists r2; split_ands; auto; apply HPQ; eauto.
Qed.
41
Global Instance pvs_proper E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
Proof. apply ne_proper, _. Qed.

Lemma pvs_intro E P : P  pvs E E P.
Proof.
  intros r n ? HP rf k Ef σ ???; exists r; split; last done.
  apply uPred_weaken with r n; eauto.
Qed.
Lemma pvs_mono E1 E2 P Q : P  Q  pvs E1 E2 P  pvs E1 E2 Q.
Proof.
  intros HPQ r n ? HP rf k Ef σ ???.
  destruct (HP rf k Ef σ) as (r2&?&?); eauto; exists r2; eauto.
Qed.
Lemma pvs_timeless E P : TimelessP P  ( P)  pvs E E P.
Proof.
  rewrite uPred.timelessP_spec=> HP r [|n] ? HP' rf k Ef σ ???; first lia.
  exists r; split; last done.
58
  apply HP, uPred_weaken with r n; eauto using cmra_validN_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80
Qed.
Lemma pvs_trans E1 E2 E3 P :
  E2  E1  E3  pvs E1 E2 (pvs E2 E3 P)  pvs E1 E3 P.
Proof.
  intros ? r1 n ? HP1 rf k Ef σ ???.
  destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto.
Qed.
Lemma pvs_mask_frame E1 E2 Ef P :
  Ef  (E1  E2) =   pvs E1 E2 P  pvs (E1  Ef) (E2  Ef) P.
Proof.
  intros ? r n ? HP rf k Ef' σ ???.
  destruct (HP rf k (EfEf') σ) as (r'&?&?); rewrite ?(associative_L _); eauto.
  by exists r'; rewrite -(associative_L _).
Qed.
Lemma pvs_frame_r E1 E2 P Q : (pvs E1 E2 P  Q)  pvs E1 E2 (P  Q).
Proof.
  intros r n ? (r1&r2&Hr&HP&?) rf k Ef σ ???.
  destruct (HP (r2  rf) k Ef σ) as (r'&?&?); eauto.
  { by rewrite (associative _) -(dist_le _ _ _ _ Hr); last lia. }
  exists (r'  r2); split; last by rewrite -(associative _).
  exists r', r2; split_ands; auto; apply uPred_weaken with r2 n; auto.
Qed.
81
Lemma pvs_open i P : ownI i P  pvs {[ i ]}  ( P).
Robbert Krebbers's avatar
Robbert Krebbers committed
82 83 84 85 86 87
Proof.
  intros r [|n] ? Hinv rf [|k] Ef σ ???; try lia.
  apply inv_spec in Hinv; last auto.
  destruct (wsat_open k Ef σ (r  rf) i P) as (rP&?&?); auto.
  { rewrite lookup_wld_op_l ?Hinv; eauto; apply dist_le with (S n); eauto. }
  exists (rP  r); split; last by rewrite (left_id_L _ _) -(associative _).
88
  eapply uPred_weaken with rP (S k); eauto using cmra_included_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90
Lemma pvs_close i P : (ownI i P   P)  pvs  {[ i ]} True.
Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94 95 96 97 98
Proof.
  intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ; split; [done|].
  rewrite (left_id _ _); apply wsat_close with P r.
  * apply inv_spec, uPred_weaken with r (S n); auto.
  * solve_elem_of +HE.
  * by rewrite -(left_id_L  () Ef).
  * apply uPred_weaken with r n; auto.
Qed.
99
Lemma pvs_updateP E m (P : iGst Λ Σ  Prop) :
100
  m ~~>: P  ownG m  pvs E E ( m',  P m'  ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
102 103
  intros Hup%option_updateP' r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
  destruct (wsat_update_gst k (E  Ef) σ r rf (Some m) P) as (m'&?&?); eauto.
104
  { apply cmra_includedN_le with (S n); auto. }
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107 108 109 110 111 112 113 114 115 116 117
Lemma pvs_updateP_empty `{Empty (iGst Λ Σ), !CMRAIdentity (iGst Λ Σ)}
    E (P : iGst Λ Σ  Prop) :
   ~~>: P  True  pvs E E ( m',  P m'  ownG m').
Proof.
  intros Hup r [|n] ? _ rf [|k] Ef σ ???; try lia.
  destruct (wsat_update_gst k (E  Ef) σ r rf  P) as (m'&?&?); eauto.
  { apply cmra_empty_leastN. }
  { apply cmra_updateP_compose_l with (Some ), option_updateP with P;
      auto using option_update_None. }
  by exists (update_gst m' r); split; [exists m'; split; [|apply ownG_spec]|].
Qed.
118
Lemma pvs_alloc E P : ¬set_finite E   P  pvs E E ( i,  (i  E)  ownI i P).
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120 121 122 123 124 125 126 127
Proof.
  intros ? r [|n] ? HP rf [|k] Ef σ ???; try lia.
  destruct (wsat_alloc k E Ef σ rf P r) as (i&?&?&?); auto.
  { apply uPred_weaken with r n; eauto. }
  exists (Res {[ i  to_agree (Later (iProp_unfold P)) ]}  ).
  by split; [by exists i; split; rewrite /uPred_holds /=|].
Qed.

(* Derived rules *)
128
Opaque uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Import uPred.
130
Global Instance pvs_mono' E1 E2 : Proper (() ==> ()) (@pvs Λ Σ E1 E2).
Robbert Krebbers's avatar
Robbert Krebbers committed
131 132 133 134 135
Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_trans' E P : pvs E E (pvs E E P)  pvs E E P.
Proof. apply pvs_trans; solve_elem_of. Qed.
Lemma pvs_frame_l E1 E2 P Q : (P  pvs E1 E2 Q)  pvs E1 E2 (P  Q).
Proof. rewrite !(commutative _ P); apply pvs_frame_r. Qed.
136 137 138 139 140 141
Lemma pvs_always_l E1 E2 P Q `{!AlwaysStable P} :
  (P  pvs E1 E2 Q)  pvs E1 E2 (P  Q).
Proof. by rewrite !always_and_sep_l' pvs_frame_l. Qed.
Lemma pvs_always_r E1 E2 P Q `{!AlwaysStable Q} :
  (pvs E1 E2 P  Q)  pvs E1 E2 (P  Q).
Proof. by rewrite !always_and_sep_r' pvs_frame_r. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
142 143 144 145 146 147 148 149
Lemma pvs_impl_l E1 E2 P Q : ( (P  Q)  pvs E1 E2 P)  pvs E1 E2 Q.
Proof. by rewrite pvs_always_l always_elim impl_elim_l. Qed.
Lemma pvs_impl_r E1 E2 P Q : (pvs E1 E2 P   (P  Q))  pvs E1 E2 Q.
Proof. by rewrite (commutative _) pvs_impl_l. Qed.
Lemma pvs_mask_weaken E1 E2 P : E1  E2  pvs E1 E1 P  pvs E2 E2 P.
Proof.
  intros; rewrite (union_difference_L E1 E2) //; apply pvs_mask_frame; auto.
Qed.
150
Lemma pvs_update E m m' : m ~~> m'  ownG m  pvs E E (ownG m').
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
152
  intros; rewrite (pvs_updateP E _ (m' =)); last by apply cmra_update_updateP.
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154 155
  by apply pvs_mono, uPred.exist_elim=> m''; apply uPred.const_elim_l=> ->.
Qed.
End pvs.