U.v 3.34 KB
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1 2
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
Dan Frumin's avatar
Dan Frumin committed
3
From iris_c.lib Require Import locking_heap.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
From iris.proofmode Require Import modalities classes.
Dan Frumin's avatar
Dan Frumin committed
5

6
Section U.
Dan Frumin's avatar
Dan Frumin committed
7
  Context `{heapG Σ, locking_heapG Σ}.
Dan Frumin's avatar
Dan Frumin committed
8 9

  (** * Unlocking modality *)
Robbert Krebbers's avatar
Robbert Krebbers committed
10
  Definition U_def (P : iProp Σ) : iProp Σ :=
11 12 13
    ( ls : gmultiset (cloc * (frac * val)),
      ([ mset] x  ls, x.1 C[LLvl]{x.2.1} x.2.2) 
      (([ mset] x  ls, x.1 C{x.2.1} x.2.2) - P))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16
  Definition U_aux : seal (@U_def). by eexists. Qed.
  Definition U := unseal U_aux.
  Definition U_eq : @U = @U_def := seal_eq U_aux.
Dan Frumin's avatar
Dan Frumin committed
17

Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20 21 22 23 24 25
  Global Instance U_ne : NonExpansive U.
  Proof. rewrite U_eq. solve_proper. Qed.
  Global Instance U_proper : Proper (() ==> ()) U.
  Proof. rewrite U_eq. solve_proper. Qed.
  Global Instance U_mono' : Proper (() ==> ()) U.
  Proof. rewrite U_eq. solve_proper. Qed.
  Global Instance U_flip_mono' : Proper (flip () ==> flip ()) U.
  Proof. rewrite U_eq. solve_proper. Qed.
Dan Frumin's avatar
Dan Frumin committed
26 27

  Lemma U_intro P : P  U P.
28
  Proof. iIntros "HP". rewrite U_eq. iExists . eauto. Qed.
Dan Frumin's avatar
Dan Frumin committed
29

30
  (** [U] behaves like an applicative functor aka "lax functor with a strength" *)
Robbert Krebbers's avatar
Robbert Krebbers committed
31
  Lemma U_sep_2 P Q : U P  U Q  U (P  Q).
Dan Frumin's avatar
Dan Frumin committed
32
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
    iIntros "[HP HQ]". rewrite U_eq.
Dan Frumin's avatar
Dan Frumin committed
34 35
    iDestruct "HP" as (ls1) "[HP1 HP2]".
    iDestruct "HQ" as (ls2) "[HQ1 HQ2]".
36
    iExists (ls1  ls2). iFrame "HP1 HQ1".
Dan Frumin's avatar
Dan Frumin committed
37 38 39 40 41
    iIntros "[HP1 HQ1]". iSplitL "HP1 HP2".
    - by iApply "HP2".
    - by iApply "HQ2".
  Qed.

42 43 44
  Lemma U_stength P Q : P  U Q  U (P  Q).
  Proof. by rewrite {1}(U_intro P) U_sep_2. Qed.

45
  Lemma U_unlock l q v : l C[LLvl]{q} v  U (l C{q} v).
Dan Frumin's avatar
Dan Frumin committed
46
  Proof.
47 48
    iIntros "Hl". rewrite U_eq. iExists {[ (l,(q,v)) ]}.
    rewrite !big_sepMS_singleton /=. auto with iFrame.
Dan Frumin's avatar
Dan Frumin committed
49 50
  Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
  (* Derived properties *)
  Lemma U_mono P Q : (P  Q)  U P  U Q.
  Proof. by intros ->. Qed.

  Lemma U_applicative P Q : U (P - Q)  U P - U Q.
  Proof. apply bi.wand_intro_l. by rewrite U_sep_2 bi.wand_elim_r. Qed.

  Global Instance U_monoid_morphism : MonoidHomomorphism bi_sep bi_sep (flip ()) U.
  Proof. split; [split|]; try apply _. apply U_sep_2. apply U_intro. Qed.

  Lemma U_big_sepL {A} (l : list A) Φ :
    (([ list] ix  l, U (Φ i x))  U ([ list] ix  l, Φ i x))%I.
  Proof. apply big_opL_commute, _. Qed.

  (* Proof mode stuff *)
  Global Instance frame_U p R P Q : Frame p R P Q  Frame p R (U P) (U Q).
  Proof. rewrite /Frame=> HRQ. by rewrite U_stength HRQ. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
69 70 71 72 73
  Class IntoUnlock (P Q : iProp Σ) := into_unlock : P  U Q.
  Global Instance into_unlock_intro P : IntoUnlock (U P) P.
  Proof. rewrite /IntoUnlock. reflexivity. Qed.
  Global Instance into_unlock_id P : IntoUnlock P P | 10.
  Proof. apply U_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
74 75 76
  Global Instance into_unlock_unlock l q v x :
    IntoUnlock (l C[x]{q} v)%I (l C{q} v)%I | 0.
  Proof. destruct x. apply U_unlock. apply U_intro. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
77 78 79 80 81 82 83 84 85 86 87

  Lemma modality_U_mixin :
    modality_mixin U MIEnvId (MIEnvTransform IntoUnlock).
  Proof.
    split; simpl; eauto using bi.equiv_entails_sym, U_intro,
      U_mono, U_sep_2 with typeclass_instances.
  Qed.
  Definition modality_U := Modality _ modality_U_mixin.

  Global Instance from_modal_later P : FromModal modality_U (U P) (U P) P.
  Proof. by rewrite /FromModal. Qed.
88
End U.
Robbert Krebbers's avatar
Robbert Krebbers committed
89

Dan Frumin's avatar
Dan Frumin committed
90
Hint Extern 1 (environments.envs_entails _ (U _)) => iModIntro.