invariants.v 4.24 KB
Newer Older
1
Require Export algebra.base prelude.countable prelude.co_pset.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import program_logic.ownership.
Ralf Jung's avatar
Ralf Jung committed
3
Require Export program_logic.pviewshifts program_logic.weakestpre.
Ralf Jung's avatar
Ralf Jung committed
4 5 6 7 8 9
Import uPred.

Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
Local Hint Extern 100 (_  _) => solve_elem_of.
Local Hint Extern 99 ({[ _ ]}  _) => apply elem_of_subseteq_singleton.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11

Robbert Krebbers's avatar
Robbert Krebbers committed
12 13
Definition namespace := list positive.
Definition nnil : namespace := nil.
14 15
Definition ndot `{Countable A} (N : namespace) (x : A) : namespace :=
  encode x :: N.
Ralf Jung's avatar
Ralf Jung committed
16
Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N).
Robbert Krebbers's avatar
Robbert Krebbers committed
17

18
Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _).
19
Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21
Lemma nclose_nnil : nclose nnil = coPset_all.
Proof. by apply (sig_eq_pi _). Qed.
22
Lemma encode_nclose N : encode N  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed.
24
Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26
Proof.
  intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->].
27
  destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|].
28
  by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Qed.
30
Lemma ndot_nclose `{Countable A} N x : encode (ndot N x)  nclose N.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Proof. apply nclose_subseteq with x, encode_nclose. Qed.
32 33
Lemma nclose_disjoint `{Countable A} N (x y : A) :
  x  y  nclose (ndot N x)  nclose (ndot N y) = .
Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36
Proof.
  intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot.
  rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]].
37
  apply Hxy, (inj encode), (inj encode_nat); revert Hq.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  rewrite !(list_encode_cons (encode _)).
39
  rewrite !(assoc_L _) (inj_iff (++ _)%positive) /=.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  generalize (encode_nat (encode y)).
  induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver.
42 43
Qed.

Ralf Jung's avatar
Ralf Jung committed
44 45
Local Hint Resolve nclose_subseteq ndot_nclose.

46 47
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
48 49 50
  ( i,  (i  nclose N)  ownI i P)%I.
Instance: Params (@inv) 3.
Typeclasses Opaque inv.
Ralf Jung's avatar
Ralf Jung committed
51 52 53 54 55 56 57 58

Section inv.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types i : positive.
Implicit Types N : namespace.
Implicit Types P Q R : iProp Λ Σ.

Global Instance inv_contractive N : Contractive (@inv Λ Σ N).
59
Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed.
Ralf Jung's avatar
Ralf Jung committed
60

61 62
Global Instance inv_always_stable N P : AlwaysStable (inv N P).
Proof. rewrite /inv; apply _. Qed.
Ralf Jung's avatar
Ralf Jung committed
63 64 65 66

Lemma always_inv N P : ( inv N P)%I  inv N P.
Proof. by rewrite always_always. Qed.

67 68 69
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
      E N P (Q : A  iProp Λ Σ) :
Ralf Jung's avatar
Ralf Jung committed
70
  nclose N  E 
71
  (inv N P  (P - FSA (E  nclose N) (λ a, P  Q a)))  FSA E Q.
Ralf Jung's avatar
Ralf Jung committed
72
Proof.
73
  move=>HN.
Ralf Jung's avatar
Ralf Jung committed
74
  rewrite /inv sep_exist_r. apply exist_elim=>i.
75
  rewrite always_and_sep_l' -assoc. apply const_elim_sep_l=>HiN.
76
  rewrite -(fsa_trans3 E (E  {[encode i]})) //; last by solve_elem_of+.
Ralf Jung's avatar
Ralf Jung committed
77
  (* Add this to the local context, so that solve_elem_of finds it. *)
78
  assert ({[encode i]}  nclose N) by eauto.
Ralf Jung's avatar
Ralf Jung committed
79
  rewrite (always_sep_dup' (ownI _ _)).
Ralf Jung's avatar
Ralf Jung committed
80
  rewrite {1}pvs_openI !pvs_frame_r.
Ralf Jung's avatar
Ralf Jung committed
81
  apply pvs_mask_frame_mono ; [solve_elem_of..|].
82
  rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
83
  apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
84
  rewrite assoc -always_and_sep_l' pvs_closeI pvs_frame_r left_id.
Ralf Jung's avatar
Ralf Jung committed
85 86 87
  apply pvs_mask_frame'; solve_elem_of.
Qed.

88 89 90 91 92 93 94
(* Derive the concrete forms for pvs and wp, because they are useful. *)

Lemma pvs_open_close E N P Q :
  nclose N  E 
  (inv N P  (P - pvs (E  nclose N) (E  nclose N) (P  Q)))  pvs E E Q.
Proof. move=>HN. by rewrite (inv_fsa pvs_fsa). Qed.

95
Lemma wp_open_close E e N P (Q : val Λ  iProp Λ Σ) :
Ralf Jung's avatar
Ralf Jung committed
96
  atomic e  nclose N  E 
Ralf Jung's avatar
Ralf Jung committed
97
  (inv N P  (P - wp (E  nclose N) e (λ v, P  Q v)))  wp E e Q.
Ralf Jung's avatar
Ralf Jung committed
98
Proof.
99
  move=>He HN. by rewrite (inv_fsa (wp_fsa e _)). Qed.
Ralf Jung's avatar
Ralf Jung committed
100

101
Lemma inv_alloc N P :  P  pvs N N (inv N P).
102
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
Ralf Jung's avatar
Ralf Jung committed
103 104

End inv.