invariants.v 2.8 KB
 Robbert Krebbers committed Feb 13, 2016 1 2 ``````From algebra Require Export base. From program_logic Require Import ownership. `````` Robbert Krebbers committed Feb 17, 2016 3 ``````From program_logic Require Export namespaces pviewshifts weakestpre. `````` Ralf Jung committed Feb 09, 2016 4 ``````Import uPred. `````` Robbert Krebbers committed Feb 17, 2016 5 6 7 ``````Local Hint Extern 100 (@eq coPset _ _) => set_solver. Local Hint Extern 100 (@subseteq coPset _ _) => set_solver. Local Hint Extern 100 (_ ∉ _) => set_solver. `````` Ralf Jung committed Feb 09, 2016 8 ``````Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton. `````` Robbert Krebbers committed Jan 16, 2016 9 `````` `````` Ralf Jung committed Feb 08, 2016 10 11 ``````(** Derived forms and lemmas about them. *) Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Feb 10, 2016 12 13 14 `````` (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I. Instance: Params (@inv) 3. Typeclasses Opaque inv. `````` Ralf Jung committed Feb 09, 2016 15 16 17 18 19 20 21 22 `````` 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 23 ``````Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed. `````` Ralf Jung committed Feb 09, 2016 24 `````` `````` Robbert Krebbers committed Feb 10, 2016 25 26 ``````Global Instance inv_always_stable N P : AlwaysStable (inv N P). Proof. rewrite /inv; apply _. Qed. `````` Ralf Jung committed Feb 09, 2016 27 28 29 30 `````` Lemma always_inv N P : (□ inv N P)%I ≡ inv N P. Proof. by rewrite always_always. Qed. `````` Ralf Jung committed Feb 11, 2016 31 ``````(** Invariants can be opened around any frame-shifting assertion. *) `````` Robbert Krebbers committed Feb 13, 2016 32 33 34 ``````Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P (Q : A → iProp Λ Σ) R : fsaV → `````` Ralf Jung committed Feb 09, 2016 35 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 36 `````` R ⊑ inv N P → `````` Robbert Krebbers committed Feb 13, 2016 37 38 `````` R ⊑ (▷ P -★ fsa (E ∖ nclose N) (λ a, ▷ P ★ Q a)) → R ⊑ fsa E Q. `````` Ralf Jung committed Feb 09, 2016 39 ``````Proof. `````` Robbert Krebbers committed Feb 13, 2016 40 41 `````` intros ? HN Hinv Hinner. rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}. `````` Ralf Jung committed Feb 13, 2016 42 `````` rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i. `````` Ralf Jung committed Feb 12, 2016 43 `````` rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN. `````` Robbert Krebbers committed Feb 17, 2016 44 45 `````` rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by set_solver+. (* Add this to the local context, so that set_solver finds it. *) `````` Ralf Jung committed Feb 09, 2016 46 `````` assert ({[encode i]} ⊆ nclose N) by eauto. `````` Ralf Jung committed Feb 12, 2016 47 `````` rewrite (always_sep_dup (ownI _ _)). `````` Ralf Jung committed Feb 09, 2016 48 `````` rewrite {1}pvs_openI !pvs_frame_r. `````` Robbert Krebbers committed Feb 17, 2016 49 `````` apply pvs_mask_frame_mono; [set_solver..|]. `````` Robbert Krebbers committed Feb 11, 2016 50 `````` rewrite (comm _ (▷_)%I) -assoc wand_elim_r fsa_frame_l. `````` Robbert Krebbers committed Feb 17, 2016 51 `````` apply fsa_mask_frame_mono; [set_solver..|]. intros a. `````` Ralf Jung committed Feb 12, 2016 52 `````` rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id. `````` Robbert Krebbers committed Feb 17, 2016 53 `````` apply pvs_mask_frame'; set_solver. `````` Ralf Jung committed Feb 09, 2016 54 55 ``````Qed. `````` Ralf Jung committed Feb 11, 2016 56 57 ``````(* Derive the concrete forms for pvs and wp, because they are useful. *) `````` Ralf Jung committed Feb 13, 2016 58 ``````Lemma pvs_open_close E N P Q R : `````` Ralf Jung committed Feb 11, 2016 59 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 60 61 62 `````` 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 63 ``````Proof. intros. by apply: (inv_fsa pvs_fsa). Qed. `````` Ralf Jung committed Feb 11, 2016 64 `````` `````` Ralf Jung committed Feb 13, 2016 65 ``````Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) R : `````` Ralf Jung committed Feb 09, 2016 66 `````` atomic e → nclose N ⊆ E → `````` Ralf Jung committed Feb 13, 2016 67 `````` R ⊑ inv N P → `````` Robbert Krebbers committed Feb 17, 2016 68 `````` R ⊑ (▷ P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)) → `````` Ralf Jung committed Feb 13, 2016 69 `````` R ⊑ wp E e Q. `````` Ralf Jung committed Feb 14, 2016 70 ``````Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed. `````` Ralf Jung committed Feb 09, 2016 71 `````` `````` Ralf Jung committed Feb 10, 2016 72 ``````Lemma inv_alloc N P : ▷ P ⊑ pvs N N (inv N P). `````` Robbert Krebbers committed Feb 10, 2016 73 ``````Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed. `````` Ralf Jung committed Feb 09, 2016 74 75 `````` End inv.``````