invariants.v 3.76 KB
Newer Older
1
From iris.program_logic Require Export pviewshifts.
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 `{irisG Λ Σ} (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) 4.
15
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
16
17

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

24
Global Instance inv_contractive N : Contractive (inv N).
25
26
27
Proof.
  rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
Qed.
Ralf Jung's avatar
Ralf Jung committed
28

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

32
Lemma inv_alloc N E P :  P ={E}=> inv N P.
33
Proof.
34
35
36
37
38
39
40
41
  rewrite inv_eq /inv_def pvs_eq /pvs_def. iIntros "HP [Hw $]".
  iVs (ownI_alloc ( nclose N) P with "[HP Hw]") as (i) "(% & $ & ?)"; auto.
  - 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.
42
  - rewrite /uPred_except_last; eauto.
43
Qed.
44

45
Lemma inv_open E N P :
46
  nclose N  E  inv N P ={E,EN}=>  P  ( P ={EN,E}= True).
47
Proof.
48
49
50
51
  rewrite inv_eq /inv_def pvs_eq /pvs_def; iDestruct 1 as (i) "[Hi #HiP]".
  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.
52
  iIntros "(Hw & [HE $] & $)"; iVsIntro; iApply except_last_intro.
53
  iDestruct (ownI_open i P with "[Hw HE]") as "($ & $ & HD)"; first by iFrame.
54
  iIntros "HP [Hw $] !==>"; iApply except_last_intro. iApply ownI_close; by iFrame.
55
56
Qed.

57
58
Lemma inv_open_timeless E N P `{!TimelessP P} :
  nclose N  E  inv N P ={E,EN}=> P  (P ={EN,E}= True).
59
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
61
  iIntros (?) "Hinv". iVs (inv_open with "Hinv") as "[>HP Hclose]"; auto.
  iIntros "!==> {$HP} HP". iApply "Hclose"; auto.
62
Qed.
Ralf Jung's avatar
Ralf Jung committed
63
End inv.
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89

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
  iVs (inv_open _ N with "[#]") as pat;
    [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.