invariants.v 3.66 KB
Newer Older
1
From iris.program_logic Require Export fancy_updates.
2
From iris.program_logic Require Export namespaces.
3
From iris.program_logic Require Import wsat.
4
From iris.algebra Require Import gmap.
5
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
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  nclose 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
  iMod (ownI_alloc ( nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
35 36 37 38 39 40
  - intros Ef. exists (coPpick (nclose 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.
  - by iFrame.
41
  - rewrite /uPred_except_0; eauto.
42
Qed.
43

44
Lemma inv_open E N P :
45
  nclose N  E  inv N P ={E,EN}=  P  ( P ={EN,E}= True).
46
Proof.
47
  rewrite inv_eq /inv_def fupd_eq /fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
48 49 50
  iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
  rewrite {1 4}(union_difference_L (nclose N) E) // ownE_op; last set_solver.
  rewrite {1 5}(union_difference_L {[ i ]} (nclose N)) // ownE_op; last set_solver.
51 52
  iIntros "(Hw & [HE $] & $) !> !>".
  iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
53
  iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
54 55
Qed.

56
Lemma inv_open_timeless E N P `{!TimelessP P} :
57
  nclose N  E  inv N P ={E,EN}= P  (P ={EN,E}= True).
58
Proof.
59 60
  iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!> {$HP} HP". iApply "Hclose"; auto.
61
Qed.
Ralf Jung's avatar
Ralf Jung committed
62
End inv.
63 64 65 66 67

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
68
  iMod (inv_open _ N with "[#]") as pat;
69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
    [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.