fancy_updates_from_vs.v 2.71 KB
Newer Older
1 2 3 4
(* This file shows that the fancy update can be encoded in terms of the
view shift, and that the laws of the fancy update can be derived from the
laws of the view shift. *)
From stdpp Require Export coPset.
5 6
From iris.proofmode Require Import tactics.
From iris.base_logic Require Export base_logic.
7 8 9 10 11 12 13
Set Default Proof Using "Type*".

Section fupd.
Context {M} (vs : coPset  coPset  uPred M  uPred M  uPred M).

Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
  (at level 99, E1,E2 at level 50, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
14
   format "P  ={ E1 , E2 }=>  Q") : bi_scope.
15 16

Context (vs_ne :  E1 E2, NonExpansive2 (vs E1 E2)).
17
Context (vs_persistent :  E1 E2 P Q, Persistent (P ={E1,E2}=> Q)).
18 19 20 21 22

Context (vs_impl :  E P Q,  (P  Q)  P ={E,E}=> Q).
Context (vs_transitive :  E1 E2 E3 P Q R,
  (P ={E1,E2}=> Q)  (Q ={E2,E3}=> R)  P ={E1,E3}=> R).
Context (vs_mask_frame_r :  E1 E2 Ef P Q,
23
  E1 ## Ef  (P ={E1,E2}=> Q)  P ={E1  Ef,E2  Ef}=> Q).
24 25 26 27
Context (vs_frame_r :  E1 E2 P Q R, (P ={E1,E2}=> Q)  P  R ={E1,E2}=> Q  R).
Context (vs_exists :  {A} E1 E2 (Φ : A  uPred M) Q,
  ( x, Φ x ={E1,E2}=> Q)  ( x, Φ x) ={E1,E2}=> Q).
Context (vs_persistent_intro_r :  E1 E2 P Q R,
28
  Persistent R 
29 30 31 32 33 34 35
  (R - (P ={E1,E2}=> Q))  P  R ={E1,E2}=> Q).

Definition fupd (E1 E2 : coPset) (P : uPred M) : uPred M :=
  ( R, R  vs E1 E2 R P)%I.

Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
  (at level 99, E1, E2 at level 50, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
36
   format "|={ E1 , E2 }=>  Q") : bi_scope.
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59

Global Instance fupd_ne E1 E2 : NonExpansive (@fupd E1 E2).
Proof. solve_proper. Qed.

Lemma fupd_intro E P : P  |={E,E}=> P.
Proof. iIntros "HP". iExists P. iFrame "HP". iApply vs_impl; auto. Qed.

Lemma fupd_mono E1 E2 P Q : (P  Q)  (|={E1,E2}=> P)  |={E1,E2}=> Q.
Proof.
  iIntros (HPQ); iDestruct 1 as (R) "[HR Hvs]".
  iExists R; iFrame "HR". iApply (vs_transitive with "[$Hvs]").
  iApply vs_impl. iIntros "!# HP". by iApply HPQ.
Qed.

Lemma fupd_trans E1 E2 E3 P : (|={E1,E2}=> |={E2,E3}=> P)  |={E1,E3}=> P.
Proof.
  iDestruct 1 as (R) "[HR Hvs]". iExists R. iFrame "HR".
  iApply (vs_transitive with "[$Hvs]"). clear R.
  iApply vs_exists; iIntros (R). iApply vs_persistent_intro_r; iIntros "Hvs".
  iApply (vs_transitive with "[$Hvs]"). iApply vs_impl; auto.
Qed.

Lemma fupd_mask_frame_r E1 E2 Ef P :
60
  E1 ## Ef  (|={E1,E2}=> P)  |={E1  Ef,E2  Ef}=> P.
61 62 63 64 65 66 67 68 69 70
Proof.
  iIntros (HE); iDestruct 1 as (R) "[HR Hvs]". iExists R; iFrame "HR".
  by iApply vs_mask_frame_r.
Qed.

Lemma fupd_frame_r E1 E2 P Q : (|={E1,E2}=> P)  Q  |={E1,E2}=> P  Q.
Proof.
  iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
  iExists (R  Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed.
71
End fupd.