invariants.v 5.23 KB
Newer Older
1 2
From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat.
3
From iris.algebra Require Import gmap.
4
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
5
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
6
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
7

8
(** Derived forms and lemmas about them. *)
9
Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
10
  ( i P', i  (N:coPset)    (P'  P)  ownI i P')%I.
11 12 13
Definition inv_aux : seal (@inv_def). by eexists. Qed.
Definition inv {Σ i} := unseal inv_aux Σ i.
Definition inv_eq : @inv = @inv_def := seal_eq inv_aux.
14
Instance: Params (@inv) 3.
15
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
16 17

Section inv.
18
Context `{invG Σ}.
Ralf Jung's avatar
Ralf Jung committed
19 20
Implicit Types i : positive.
Implicit Types N : namespace.
21
Implicit Types P Q R : iProp Σ.
Ralf Jung's avatar
Ralf Jung committed
22

23
Global Instance inv_contractive N : Contractive (inv N).
24
Proof. rewrite inv_eq. solve_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
25

26 27 28
Global Instance inv_ne N : NonExpansive (inv N).
Proof. apply contractive_ne, _. Qed.

29
Global Instance inv_proper N : Proper (() ==> ()) (inv N).
30 31
Proof. apply ne_proper, _. Qed.

32
Global Instance inv_persistent N P : Persistent (inv N P).
33
Proof. rewrite inv_eq /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
34

35 36 37 38 39 40 41 42
Lemma inv_iff N P Q :   (P  Q) - inv N P - inv N Q.
Proof.
  iIntros "#HPQ". rewrite inv_eq. iDestruct 1 as (i P') "(?&#HP&?)".
  iExists i, P'. iFrame. iNext; iAlways; iSplit.
  - iIntros "HP'". iApply "HPQ". by iApply "HP".
  - iIntros "HQ". iApply "HP". by iApply "HPQ".
Qed.

43
Lemma fresh_inv_name (E : gset positive) N :  i, i  E  i  (N:coPset).
44 45 46 47 48 49 50 51
Proof.
  exists (coPpick ( N  coPset.of_gset E)).
  rewrite -coPset.elem_of_of_gset (comm and) -elem_of_difference.
  apply coPpick_elem_of=> Hfin.
  eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
  apply of_gset_finite.
Qed.

52
Lemma inv_alloc N E P :  P ={E}= inv N P.
53
Proof.
54
  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
55
  iMod (ownI_alloc ( (N : coPset)) P with "[$HP $Hw]")
56
    as (i ?) "[$ ?]"; auto using fresh_inv_name.
57
  do 2 iModIntro. iExists i, P. rewrite -(iff_refl True). auto.
58
Qed.
59

60
Lemma inv_alloc_open N E P :
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  N  E  (|={E, E∖↑N}=> inv N P  (P ={E∖↑N, E}= True))%I.
62
Proof.
63
  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros (Sub) "[Hw HE]".
64
  iMod (ownI_alloc_open ( (N : coPset)) P with "Hw")
65
    as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name.
66 67 68 69 70
  iAssert (ownE {[i]}  ownE ( N  {[i]})  ownE (E   N))%I
    with "[HE]" as "(HEi & HEN\i & HE\N)".
  { rewrite -?ownE_op; [|set_solver..].
    rewrite assoc_L -!union_difference_L //. set_solver. }
  do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
71 72 73
  iSplitL "Hi".
  { iExists i, P. rewrite -(iff_refl True). auto. }
  iIntros "HP [Hw HE\N]".
74 75 76 77 78
  iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
  do 2 iModIntro. iSplitL; [|done].
  iCombine "HEi" "HEN\i" as "HEN"; iCombine "HEN" "HE\N" as "HE".
  rewrite -?ownE_op; [|set_solver..].
  rewrite -!union_difference_L //; set_solver.
79 80
Qed.

81
Lemma inv_open E N P :
82
  N  E  inv N P ={E,E∖↑N}=  P  ( P ={E∖↑N,E}= True).
83
Proof.
84 85
  rewrite inv_eq /inv_def fupd_eq /fupd_def.
  iDestruct 1 as (i P') "(Hi & #HP' & #HiP)".
86
  iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
87 88
  rewrite {1 4}(union_difference_L ( N) E) // ownE_op; last set_solver.
  rewrite {1 5}(union_difference_L {[ i ]} ( N)) // ownE_op; last set_solver.
89
  iIntros "(Hw & [HE $] & $) !> !>".
90 91 92 93
  iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & HP & HD)".
  iDestruct ("HP'" with "HP") as "$".
  iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP".
  iApply "HP'". iFrame.
94 95
Qed.

96
Lemma inv_open_timeless E N P `{!Timeless P} :
97
  N  E  inv N P ={E,E∖↑N}= P  (P ={E∖↑N,E}= True).
98
Proof.
99 100
  iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!> {$HP} HP". iApply "Hclose"; auto.
101
Qed.
Ralf Jung's avatar
Ralf Jung committed
102
End inv.
103 104 105 106

Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
  let Htmp := iFresh in
  let patback := intro_pat.parse_one Hclose in
107
  let pat := constr:(IList [[IIdent Htmp; patback]]) in
108
  iMod (inv_open _ N with "[#]") as pat;
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
    [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
    [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
    |tac Htmp].

Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
   iInvCore N as (fun H => iDestruct H as pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
    constr(pat) constr(Hclose) :=
   iInvCore N as (fun H => iDestruct H as (x1) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
   iInvCore N as (fun H => iDestruct H as (x1 x2) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) ")"
    constr(pat) constr(Hclose) :=
   iInvCore N as (fun H => iDestruct H as (x1 x2 x3) pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
    simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
    constr(pat) constr(Hclose) :=
   iInvCore N as (fun H => iDestruct H as (x1 x2 x3 x4) pat) Hclose.