invariants.v 4.87 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.base prelude.countable prelude.co_pset. `````` Ralf Jung committed Feb 08, 2016 2 ``````Require Import program_logic.ownership. `````` Ralf Jung committed Feb 09, 2016 3 ``````Require Export program_logic.pviewshifts program_logic.weakestpre. `````` Ralf Jung committed Feb 09, 2016 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 committed Jan 16, 2016 10 11 12 `````` Definition namespace := list positive. Definition nnil : namespace := nil. `````` Ralf Jung committed Feb 08, 2016 13 14 ``````Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. `````` Ralf Jung committed Feb 08, 2016 15 ``````Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). `````` Robbert Krebbers committed Jan 16, 2016 16 17 `````` Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _). `````` Ralf Jung committed Feb 08, 2016 18 ``````Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed. `````` Robbert Krebbers committed Jan 16, 2016 19 20 ``````Lemma nclose_nnil : nclose nnil = coPset_all. Proof. by apply (sig_eq_pi _). Qed. `````` Ralf Jung committed Feb 08, 2016 21 ``````Lemma encode_nclose N : encode N ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 22 ``````Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. `````` Ralf Jung committed Feb 08, 2016 23 ``````Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 24 25 ``````Proof. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. `````` Ralf Jung committed Feb 08, 2016 26 `````` destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|]. `````` Robbert Krebbers committed Jan 16, 2016 27 28 `````` by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal. Qed. `````` Ralf Jung committed Feb 08, 2016 29 ``````Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 30 ``````Proof. apply nclose_subseteq with x, encode_nclose. Qed. `````` Ralf Jung committed Feb 08, 2016 31 32 ``````Lemma nclose_disjoint `{Countable A} N (x y : A) : x ≠ y → nclose (ndot N x) ∩ nclose (ndot N y) = ∅. `````` Robbert Krebbers committed Jan 16, 2016 33 34 35 36 37 38 39 40 ``````Proof. intros Hxy; apply elem_of_equiv_empty_L=> p; unfold nclose, ndot. rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]]. apply Hxy, (injective encode), (injective encode_nat); revert Hq. rewrite !(list_encode_cons (encode _)). rewrite !(associative_L _) (injective_iff (++ _)%positive) /=. generalize (encode_nat (encode y)). induction (encode_nat (encode x)); intros [|?] ?; f_equal'; naive_solver. `````` Ralf Jung committed Feb 08, 2016 41 42 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 43 44 ``````Local Hint Resolve nclose_subseteq ndot_nclose. `````` Ralf Jung committed Feb 08, 2016 45 46 ``````(** Derived forms and lemmas about them. *) Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ := `````` Ralf Jung committed Feb 09, 2016 47 `````` (∃ i : positive, ■(i ∈ nclose N) ∧ ownI i P)%I. `````` Ralf Jung committed Feb 09, 2016 48 49 50 51 52 53 54 55 56 57 `````` 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). Proof. intros n ? ? EQ. apply exists_ne=>i. `````` Ralf Jung committed Feb 09, 2016 58 `````` apply and_ne; first done. `````` Ralf Jung committed Feb 09, 2016 59 60 61 62 63 64 65 66 67 68 69 70 71 `````` by apply ownI_contractive. Qed. Global Instance inv_always_stable N P : AlwaysStable (inv N P) := _. Lemma always_inv N P : (□ inv N P)%I ≡ inv N P. Proof. by rewrite always_always. Qed. (* We actually pretty much lose the abolity to deal with mask-changing view shifts when using `inv`. This is because we cannot exactly name the invariants any more. But that's okay; all this means is that sugar like the atomic triples will have to prove its own version of the open_close rule by unfolding `inv`. *) `````` Ralf Jung committed Feb 09, 2016 72 ``````(* TODO Can we prove something that helps for both open_close lemmas? *) `````` Ralf Jung committed Feb 09, 2016 73 ``````Lemma pvs_open_close E N P Q : `````` Ralf Jung committed Feb 09, 2016 74 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 09, 2016 75 `````` (inv N P ∧ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q. `````` Ralf Jung committed Feb 09, 2016 76 ``````Proof. `````` Ralf Jung committed Feb 09, 2016 77 `````` move=>HN. `````` Ralf Jung committed Feb 09, 2016 78 `````` rewrite /inv and_exist_r. apply exist_elim=>i. `````` Ralf Jung committed Feb 09, 2016 79 `````` rewrite -associative. apply const_elim_l=>HiN. `````` Ralf Jung committed Feb 09, 2016 80 `````` rewrite -(pvs_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+. `````` Ralf Jung committed Feb 09, 2016 81 `````` (* Add this to the local context, so that solve_elem_of finds it. *) `````` Ralf Jung committed Feb 09, 2016 82 `````` assert ({[encode i]} ⊆ nclose N) by eauto. `````` Ralf Jung committed Feb 09, 2016 83 84 `````` rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)). rewrite {1}pvs_openI !pvs_frame_r. `````` Ralf Jung committed Feb 09, 2016 85 `````` apply pvs_mask_frame_mono ; [solve_elem_of..|]. `````` Ralf Jung committed Feb 09, 2016 86 `````` rewrite (commutative _ (▷_)%I) -associative wand_elim_r pvs_frame_l. `````` Ralf Jung committed Feb 09, 2016 87 88 89 90 91 `````` apply pvs_mask_frame_mono; [solve_elem_of..|]. rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id. apply pvs_mask_frame'; solve_elem_of. Qed. `````` Ralf Jung committed Feb 09, 2016 92 ``````Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) : `````` Ralf Jung committed Feb 09, 2016 93 `````` atomic e → nclose N ⊆ E → `````` Ralf Jung committed Feb 09, 2016 94 `````` (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)))%I ⊑ wp E e Q. `````` Ralf Jung committed Feb 09, 2016 95 ``````Proof. `````` Ralf Jung committed Feb 09, 2016 96 `````` move=>He HN. `````` Ralf Jung committed Feb 09, 2016 97 98 99 100 101 102 103 104 `````` rewrite /inv and_exist_r. apply exist_elim=>i. rewrite -associative. apply const_elim_l=>HiN. rewrite -(wp_atomic E (E ∖ {[encode i]})) //; last by solve_elem_of+. (* Add this to the local context, so that solve_elem_of finds it. *) assert ({[encode i]} ⊆ nclose N) by eauto. rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)). rewrite {1}pvs_openI !pvs_frame_r. apply pvs_mask_frame_mono; [solve_elem_of..|]. `````` Ralf Jung committed Feb 09, 2016 105 `````` rewrite (commutative _ (▷_)%I) -associative wand_elim_r wp_frame_l. `````` Ralf Jung committed Feb 09, 2016 106 107 108 109 110 `````` apply wp_mask_frame_mono; [solve_elem_of..|]=>v. rewrite associative -always_and_sep_l' pvs_closeI pvs_frame_r left_id. apply pvs_mask_frame'; solve_elem_of. Qed. `````` Ralf Jung committed Feb 09, 2016 111 112 ``````Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P). Proof. `````` Ralf Jung committed Feb 09, 2016 113 `````` rewrite /inv (pvs_allocI N); first done. `````` Ralf Jung committed Feb 09, 2016 114 115 `````` apply coPset_suffixes_infinite. Qed. `````` Ralf Jung committed Feb 09, 2016 116 117 `````` End inv.``````