invariants.v 5.09 KB
 Robbert Krebbers committed Feb 13, 2016 1 2 3 4 ``````From algebra Require Export base. From prelude Require Export countable co_pset. From program_logic Require Import ownership. From program_logic Require Export pviewshifts weakestpre. `````` Ralf Jung committed Feb 09, 2016 5 6 7 8 9 10 ``````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 committed Jan 16, 2016 11 `````` `````` Ralf Jung committed Feb 10, 2016 12 `````` `````` Robbert Krebbers committed Jan 16, 2016 13 14 ``````Definition namespace := list positive. Definition nnil : namespace := nil. `````` Ralf Jung committed Feb 08, 2016 15 16 ``````Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. `````` Ralf Jung committed Feb 08, 2016 17 ``````Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). `````` Robbert Krebbers committed Jan 16, 2016 18 `````` `````` Robbert Krebbers committed Feb 11, 2016 19 ``````Instance ndot_inj `{Countable A} : Inj2 (=) (=) (=) (@ndot A _ _). `````` Ralf Jung committed Feb 08, 2016 20 ``````Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed. `````` Robbert Krebbers committed Jan 16, 2016 21 22 ``````Lemma nclose_nnil : nclose nnil = coPset_all. Proof. by apply (sig_eq_pi _). Qed. `````` Ralf Jung committed Feb 08, 2016 23 ``````Lemma encode_nclose N : encode N ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 24 ``````Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. `````` Ralf Jung committed Feb 08, 2016 25 ``````Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 26 27 ``````Proof. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. `````` Ralf Jung committed Feb 08, 2016 28 `````` destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|]. `````` Robbert Krebbers committed Feb 11, 2016 29 `````` by exists (q ++ q')%positive; rewrite <-(assoc_L _); f_equal. `````` Robbert Krebbers committed Jan 16, 2016 30 ``````Qed. `````` Ralf Jung committed Feb 08, 2016 31 ``````Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 32 ``````Proof. apply nclose_subseteq with x, encode_nclose. Qed. `````` Ralf Jung committed Feb 16, 2016 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 `````` Definition ndisj (N1 N2 : namespace) := ∃ N1' N2', N1' `suffix_of` N1 ∧ N2' `suffix_of` N2 ∧ length N1' = length N2' ∧ N1' ≠ N2'. Global Instance ndisj_comm : Comm iff ndisj. Proof. intros N1 N2. rewrite /ndisj; naive_solver. Qed. Lemma ndot_ne_disj `{Countable A} N (x y : A) : x ≠ y → ndisj (ndot N x) (ndot N y). Proof. intros Hxy. exists (ndot N x), (ndot N y). split_ands; try done; []. by apply not_inj2_2. Qed. Lemma ndot_preserve_disj_l `{Countable A} N1 N2 (x : A) : ndisj N1 N2 → ndisj (ndot N1 x) N2. Proof. intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'. split_ands; try done; []. by apply suffix_of_cons_r. Qed. Lemma ndot_preserve_disj_r `{Countable A} N1 N2 (x : A) : ndisj N1 N2 → ndisj N1 (ndot N2 x). Proof. rewrite ![ndisj N1 _]comm. apply ndot_preserve_disj_l. Qed. Lemma ndisj_disjoint N1 N2 : ndisj N1 N2 → nclose N1 ∩ nclose N2 = ∅. `````` Robbert Krebbers committed Jan 16, 2016 63 ``````Proof. `````` Ralf Jung committed Feb 16, 2016 64 65 `````` intros (N1' & N2' & [N1'' Hpr1] & [N2'' Hpr2] & Hl & Hne). subst N1 N2. apply elem_of_equiv_empty_L=> p; unfold nclose. `````` Robbert Krebbers committed Jan 16, 2016 66 `````` rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]]. `````` Ralf Jung committed Feb 16, 2016 67 68 `````` rewrite !list_encode_app !assoc in Hq. apply Hne. eapply list_encode_suffix_eq; done. `````` Ralf Jung committed Feb 08, 2016 69 70 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 71 72 ``````Local Hint Resolve nclose_subseteq ndot_nclose. `````` Ralf Jung committed Feb 08, 2016 73 74 ``````(** Derived forms and lemmas about them. *) Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Feb 10, 2016 75 76 77 `````` (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I. Instance: Params (@inv) 3. Typeclasses Opaque inv. `````` Ralf Jung committed Feb 09, 2016 78 79 80 81 82 83 84 85 `````` 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). `````` Robbert Krebbers committed Feb 10, 2016 86 ``````Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed. `````` Ralf Jung committed Feb 09, 2016 87 `````` `````` Robbert Krebbers committed Feb 10, 2016 88 89 ``````Global Instance inv_always_stable N P : AlwaysStable (inv N P). Proof. rewrite /inv; apply _. Qed. `````` Ralf Jung committed Feb 09, 2016 90 91 92 93 `````` Lemma always_inv N P : (□ inv N P)%I ≡ inv N P. Proof. by rewrite always_always. Qed. `````` Ralf Jung committed Feb 11, 2016 94 ``````(** Invariants can be opened around any frame-shifting assertion. *) `````` Robbert Krebbers committed Feb 13, 2016 95 96 97 ``````Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P (Q : A → iProp Λ Σ) R : fsaV → `````` Ralf Jung committed Feb 09, 2016 98 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 99 `````` R ⊑ inv N P → `````` Robbert Krebbers committed Feb 13, 2016 100 101 `````` R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Q a)) → R ⊑ fsa E Q. `````` Ralf Jung committed Feb 09, 2016 102 ``````Proof. `````` Robbert Krebbers committed Feb 13, 2016 103 104 `````` intros ? HN Hinv Hinner. rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}. `````` Ralf Jung committed Feb 13, 2016 105 `````` rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i. `````` Ralf Jung committed Feb 12, 2016 106 `````` rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN. `````` Robbert Krebbers committed Feb 13, 2016 107 `````` rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by solve_elem_of+. `````` Ralf Jung committed Feb 09, 2016 108 `````` (* Add this to the local context, so that solve_elem_of finds it. *) `````` Ralf Jung committed Feb 09, 2016 109 `````` assert ({[encode i]} ⊆ nclose N) by eauto. `````` Ralf Jung committed Feb 12, 2016 110 `````` rewrite (always_sep_dup (ownI _ _)). `````` Ralf Jung committed Feb 09, 2016 111 `````` rewrite {1}pvs_openI !pvs_frame_r. `````` Robbert Krebbers committed Feb 13, 2016 112 `````` apply pvs_mask_frame_mono; [solve_elem_of..|]. `````` Robbert Krebbers committed Feb 11, 2016 113 `````` rewrite (comm _ (▷_)%I) -assoc wand_elim_r fsa_frame_l. `````` Ralf Jung committed Feb 11, 2016 114 `````` apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a. `````` Ralf Jung committed Feb 12, 2016 115 `````` rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id. `````` Ralf Jung committed Feb 09, 2016 116 117 118 `````` apply pvs_mask_frame'; solve_elem_of. Qed. `````` Ralf Jung committed Feb 11, 2016 119 120 ``````(* Derive the concrete forms for pvs and wp, because they are useful. *) `````` Ralf Jung committed Feb 13, 2016 121 ``````Lemma pvs_open_close E N P Q R : `````` Ralf Jung committed Feb 11, 2016 122 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 123 124 125 `````` R ⊑ inv N P → R ⊑ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q)) → R ⊑ pvs E E Q. `````` Ralf Jung committed Feb 14, 2016 126 ``````Proof. intros. by apply: (inv_fsa pvs_fsa). Qed. `````` Ralf Jung committed Feb 11, 2016 127 `````` `````` Ralf Jung committed Feb 13, 2016 128 ``````Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R : `````` Ralf Jung committed Feb 09, 2016 129 `````` atomic e → nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 130 131 132 `````` R ⊑ inv N P → R ⊑ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)) → R ⊑ wp E e Q. `````` Ralf Jung committed Feb 14, 2016 133 ``````Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed. `````` Ralf Jung committed Feb 09, 2016 134 `````` `````` Ralf Jung committed Feb 10, 2016 135 ``````Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P). `````` Robbert Krebbers committed Feb 10, 2016 136 ``````Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed. `````` Ralf Jung committed Feb 09, 2016 137 138 `````` End inv.``````