invariants.v 4.85 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, i  N  ownI i P)%I.
11
Definition inv_aux : { x | x = @inv_def }. by eexists. Qed.
12
Definition inv {Σ i} := proj1_sig inv_aux Σ i.
13
Definition inv_eq : @inv = @inv_def := proj2_sig 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 25 26
Proof.
  rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
Qed.
Ralf Jung's avatar
Ralf Jung committed
27

28
Global Instance inv_persistent N P : PersistentP (inv N P).
29
Proof. rewrite inv_eq /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
30

31
Lemma inv_alloc N E P :  P ={E}= inv N P.
32
Proof.
33
  rewrite inv_eq /inv_def fupd_eq /fupd_def. iIntros "HP [Hw $]".
34 35
  iMod (ownI_alloc (  N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
  - intros Ef. exists (coPpick ( N  coPset.of_gset Ef)).
36 37 38 39 40
    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
    apply coPpick_elem_of=> Hfin.
    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
    apply of_gset_finite.
  - by iFrame.
41
  - rewrite /uPred_except_0; eauto.
42
Qed.
43

44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
Lemma inv_alloc_open N E P :
  N  E  True ={E, E∖↑N}= inv N P  (P ={E∖↑N, E}= True).
Proof.
  rewrite inv_eq /inv_def fupd_eq /fupd_def.
  iIntros (Sub) "[Hw HE]".
  iMod (ownI_alloc_open (  N) P with "Hw") as (i) "(% & Hw & #Hi & HD)".
  - intros Ef. exists (coPpick ( N  coPset.of_gset Ef)).
    rewrite -coPset.elem_of_of_gset comm -elem_of_difference.
    apply coPpick_elem_of=> Hfin.
    eapply nclose_infinite, (difference_finite_inv _ _), Hfin.
    apply of_gset_finite.
  - iAssert (ownE {[i]}  ownE ( N  {[i]})  ownE (E   N))%I with "[HE]" as "(HEi & HEN\i & HE\N)".
    { rewrite -?ownE_op; [|set_solver|set_solver].
      rewrite assoc_L. rewrite <-!union_difference_L; try done; set_solver. }
    iModIntro. rewrite /uPred_except_0. iRight. iFrame.
    iSplitL "Hw HEi".
    + by iApply "Hw".
    + iSplitL "Hi"; [eauto|].
      iIntros "HP [Hw HE\N]".
      iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[? HEi]".
      iModIntro. iRight. iFrame. iSplitL; [|done].
      iCombine "HEi" "HEN\i" as "HEN".
      iCombine "HEN" "HE\N" as "HE".
      rewrite -?ownE_op; [|set_solver|set_solver].
      rewrite <-!union_difference_L; try done; set_solver.
Qed.

71
Lemma inv_open E N P :
72
  N  E  inv N P ={E,E∖↑N}=  P  ( P ={E∖↑N,E}= True).
73
Proof.
74
  rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
75
  iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
76 77
  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.
78 79
  iIntros "(Hw & [HE $] & $) !> !>".
  iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
80
  iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
81 82
Qed.

83
Lemma inv_open_timeless E N P `{!TimelessP P} :
84
  N  E  inv N P ={E,E∖↑N}= P  (P ={E∖↑N,E}= True).
85
Proof.
86 87
  iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!> {$HP} HP". iApply "Hclose"; auto.
88
Qed.
Ralf Jung's avatar
Ralf Jung committed
89
End inv.
90 91 92 93 94

Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
  let Htmp := iFresh in
  let patback := intro_pat.parse_one Hclose in
  let pat := constr:(IList [[IName Htmp; patback]]) in
95
  iMod (inv_open _ N with "[#]") as pat;
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115
    [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.