fancy_updates.v 7.89 KB
Newer Older
1 2 3 4 5 6 7 8
From iris.program_logic Require Export iris.
From iris.program_logic Require Import wsat.
From iris.algebra Require Import upred_big_op gmap.
From iris.proofmode Require Import tactics classes.
Import uPred.

Program Definition fupd_def `{irisG Λ Σ}
    (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
9
  (wsat  ownE E1 ==  (wsat  ownE E2  P))%I.
10 11 12 13 14 15 16 17 18 19 20 21
Definition fupd_aux : { x | x = @fupd_def }. by eexists. Qed.
Definition fupd := proj1_sig fupd_aux.
Definition fupd_eq : @fupd = @fupd_def := proj2_sig fupd_aux.
Arguments fupd {_ _ _} _ _ _%I.
Instance: Params (@fupd) 5.

Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q") : uPred_scope.
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.
22
Notation "P ={ E1 , E2 }=★ Q" := (P  |={E1,E2}=> Q)
23 24 25 26 27 28 29 30
  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : C_scope.

Notation "|={ E }=> Q" := (fupd E E Q)
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q") : uPred_scope.
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.
31
Notation "P ={ E }=★ Q" := (P  |={E}=> Q)
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
  (at level 99, E at level 50, Q at level 200, only parsing) : C_scope.

Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }▷=>  Q") : uPred_scope.
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q") : uPred_scope.

Section fupd.
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.

Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Λ Σ _ E1 E2).
Proof. rewrite fupd_eq. solve_proper. Qed.
Global Instance fupd_proper E1 E2 : Proper (() ==> ()) (@fupd Λ Σ _ E1 E2).
Proof. apply ne_proper, _. Qed.

Lemma fupd_intro_mask E1 E2 P : E2  E1  P  |={E1,E2}=> |={E2,E1}=> P.
Proof.
  intros (E1''&->&?)%subseteq_disjoint_union_L.
  rewrite fupd_eq /fupd_def ownE_op //. iIntros "H ($ & $ & HE) !==>".
  iApply except_last_intro. iIntros "[$ $] !==>" . iApply except_last_intro.
  by iFrame.
Qed.

58
Lemma except_last_fupd E1 E2 P :  (|={E1,E2}=> P) ={E1,E2}= P.
59 60 61 62
Proof.
  rewrite fupd_eq. iIntros "H [Hw HE]". iTimeless "H". iApply "H"; by iFrame.
Qed.

63
Lemma bupd_fupd E P : (|==> P) ={E}= P.
64 65 66 67 68
Proof.
  rewrite fupd_eq /fupd_def. iIntros "H [$ $]"; iUpd "H".
  iUpdIntro. by iApply except_last_intro.
Qed.

69
Lemma fupd_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
70 71 72 73 74
Proof.
  rewrite fupd_eq /fupd_def. iIntros (HPQ) "HP HwE".
  rewrite -HPQ. by iApply "HP".
Qed.

75
Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P) ={E1,E3}= P.
76 77 78 79 80 81
Proof.
  rewrite fupd_eq /fupd_def. iIntros "HP HwE".
  iUpd ("HP" with "HwE") as ">(Hw & HE & HP)". iApply "HP"; by iFrame.
Qed.

Lemma fupd_mask_frame_r' E1 E2 Ef P :
82
  E1  Ef  (|={E1,E2}=> E2  Ef  P) ={E1  Ef,E2  Ef}= P.
83 84 85 86 87 88 89
Proof.
  intros. rewrite fupd_eq /fupd_def ownE_op //. iIntros "Hvs (Hw & HE1 &HEf)".
  iUpd ("Hvs" with "[Hw HE1]") as ">($ & HE2 & HP)"; first by iFrame.
  iDestruct (ownE_op' with "[HE2 HEf]") as "[? $]"; first by iFrame.
  iUpdIntro; iApply except_last_intro. by iApply "HP".
Qed.

90
Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q ={E1,E2}= P  Q.
91 92 93 94 95 96 97 98 99
Proof. rewrite fupd_eq /fupd_def. by iIntros "[HwP $]". Qed.

(** * Derived rules *)
Global Instance fupd_mono' E1 E2 : Proper (() ==> ()) (@fupd Λ Σ _ E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.
Global Instance fupd_flip_mono' E1 E2 :
  Proper (flip () ==> flip ()) (@fupd Λ Σ _ E1 E2).
Proof. intros P Q; apply fupd_mono. Qed.

100
Lemma fupd_intro E P : P ={E}= P.
101 102 103
Proof. iIntros "HP". by iApply bupd_fupd. Qed.
Lemma fupd_intro_mask' E1 E2 : E2  E1  True  |={E1,E2}=> |={E2,E1}=> True.
Proof. exact: fupd_intro_mask. Qed.
104
Lemma fupd_except_last E1 E2 P : (|={E1,E2}=>  P) ={E1,E2}= P.
105 106
Proof. by rewrite {1}(fupd_intro E2 P) except_last_fupd fupd_trans. Qed.

107
Lemma fupd_frame_l E1 E2 P Q : (P  |={E1,E2}=> Q) ={E1,E2}= P  Q.
108
Proof. rewrite !(comm _ P); apply fupd_frame_r. Qed.
109
Lemma fupd_wand_l E1 E2 P Q : (P - Q)  (|={E1,E2}=> P) ={E1,E2}= Q.
110
Proof. by rewrite fupd_frame_l wand_elim_l. Qed.
111
Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P)  (P - Q) ={E1,E2}= Q.
112 113 114
Proof. by rewrite fupd_frame_r wand_elim_r. Qed.

Lemma fupd_trans_frame E1 E2 E3 P Q :
115
  ((Q ={E2,E3}= True)  |={E1,E2}=> (Q  P)) ={E1,E3}= P.
116 117 118 119 120 121
Proof.
  rewrite fupd_frame_l assoc -(comm _ Q) wand_elim_r.
  by rewrite fupd_frame_r left_id fupd_trans.
Qed.

Lemma fupd_mask_frame_r E1 E2 Ef P :
122
  E1  Ef  (|={E1,E2}=> P) ={E1  Ef,E2  Ef}= P.
123 124 125 126
Proof.
  iIntros (?) "H". iApply fupd_mask_frame_r'; auto.
  iApply fupd_wand_r; iFrame "H"; eauto.
Qed.
127
Lemma fupd_mask_mono E1 E2 P : E1  E2  (|={E1}=> P) ={E2}= P.
128 129 130 131
Proof.
  intros (Ef&->&?)%subseteq_disjoint_union_L. by apply fupd_mask_frame_r.
Qed.

132
Lemma fupd_sep E P Q : (|={E}=> P)  (|={E}=> Q) ={E}= P  Q.
133 134
Proof. by rewrite fupd_frame_r fupd_frame_l fupd_trans. Qed.
Lemma fupd_big_sepM `{Countable K} {A} E (Φ : K  A  iProp Σ) (m : gmap K A) :
135
  ([ map] kx  m, |={E}=> Φ k x) ={E}= [ map] kx  m, Φ k x.
136
Proof.
137
  apply (big_opM_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
138 139 140
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
Lemma fupd_big_sepS `{Countable A} E (Φ : A  iProp Σ) X :
141
  ([ set] x  X, |={E}=> Φ x) ={E}= [ set] x  X, Φ x.
142
Proof.
143
  apply (big_opS_forall (λ P Q, P ={E}= Q)); auto using fupd_intro.
144 145 146 147 148 149 150 151 152 153 154 155 156
  intros P1 P2 HP Q1 Q2 HQ. by rewrite HP HQ -fupd_sep.
Qed.
End fupd.

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.

  Global Instance from_pure_fupd E P φ : FromPure P φ  FromPure (|={E}=> P) φ.
  Proof. rewrite /FromPure. intros <-. apply fupd_intro. Qed.

  Global Instance from_assumption_fupd E p P Q :
157
    FromAssumption p P (|==> Q)  FromAssumption p P (|={E}=> Q)%I.
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
  Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.

  Global Instance into_wand_fupd E1 E2 R P Q :
    IntoWand R P Q  IntoWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
  Proof. rewrite /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r. Qed.

  Global Instance from_sep_fupd E P Q1 Q2 :
    FromSep P Q1 Q2  FromSep (|={E}=> P) (|={E}=> Q1) (|={E}=> Q2).
  Proof. rewrite /FromSep=><-. apply fupd_sep. Qed.

  Global Instance or_split_fupd E1 E2 P Q1 Q2 :
    FromOr P Q1 Q2  FromOr (|={E1,E2}=> P) (|={E1,E2}=> Q1) (|={E1,E2}=> Q2).
  Proof. rewrite /FromOr=><-. apply or_elim; apply fupd_mono; auto with I. Qed.

  Global Instance exists_split_fupd {A} E1 E2 P (Φ : A  iProp Σ) :
    FromExist P Φ  FromExist (|={E1,E2}=> P) (λ a, |={E1,E2}=> Φ a)%I.
  Proof.
    rewrite /FromExist=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
  Qed.

  Global Instance frame_fupd E1 E2 R P Q :
    Frame R P Q  Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
  Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.

  Global Instance is_except_last_fupd E1 E2 P : IsExceptLast (|={E1,E2}=> P).
  Proof. by rewrite /IsExceptLast except_last_fupd. Qed.

  Global Instance from_upd_fupd E P : FromUpd (|={E}=> P) P.
  Proof. by rewrite /FromUpd -bupd_fupd. Qed.

  Global Instance elim_upd_bupd_fupd E1 E2 P Q :
189
    ElimUpd (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
190 191 192 193 194 195 196 197
  Proof. by rewrite /ElimUpd (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans. Qed.
  Global Instance elim_upd_fupd_fupd E1 E2 E3 P Q :
    ElimUpd (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
  Proof. by rewrite /ElimUpd fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.

Hint Extern 2 (coq_tactics.of_envs _  _) =>
  match goal with |- _  |={_}=> _ => iUpdIntro end.