invariants.v 4.87 KB
Newer Older
 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 `````` 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. `````` Ralf Jung committed Feb 09, 2016 67 68 69 70 71 72 73 ``````(* There is not really a way to provide versions of pvs_openI and pvs_closeI that work with inv. The issue is that these rules track the exact current mask too precisely. However, we *can* provide abstract rules by performing both the opening and the closing of the invariant in the rule, and then implicitly framing all the unused invariants around the "inner" view shift provided by the client. *) `````` Ralf Jung committed Feb 09, 2016 74 ``````Lemma pvs_open_close E N P Q : `````` Ralf Jung committed Feb 09, 2016 75 `````` nclose N ⊆ E → `````` Ralf Jung committed Feb 09, 2016 76 `````` (inv N P ∧ (▷P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷P ★ Q))) ⊑ pvs E E Q. `````` Ralf Jung committed Feb 09, 2016 77 ``````Proof. `````` Ralf Jung committed Feb 09, 2016 78 `````` move=>HN. `````` Ralf Jung committed Feb 09, 2016 79 `````` rewrite /inv and_exist_r. apply exist_elim=>i. `````` Ralf Jung committed Feb 09, 2016 80 `````` rewrite -associative. apply const_elim_l=>HiN. `````` Ralf Jung committed Feb 09, 2016 81 `````` rewrite -(pvs_trans3 E (E ∖ {[encode i]})) //; last by solve_elem_of+. `````` Ralf Jung committed Feb 09, 2016 82 `````` (* Add this to the local context, so that solve_elem_of finds it. *) `````` Ralf Jung committed Feb 09, 2016 83 `````` assert ({[encode i]} ⊆ nclose N) by eauto. `````` Ralf Jung committed Feb 09, 2016 84 85 `````` rewrite always_and_sep_l' (always_sep_dup' (ownI _ _)). rewrite {1}pvs_openI !pvs_frame_r. `````` Ralf Jung committed Feb 09, 2016 86 `````` apply pvs_mask_frame_mono ; [solve_elem_of..|]. `````` Ralf Jung committed Feb 09, 2016 87 `````` rewrite (commutative _ (▷_)%I) -associative wand_elim_r pvs_frame_l. `````` Ralf Jung committed Feb 09, 2016 88 89 90 91 92 `````` 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 93 ``````Lemma wp_open_close E e N P (Q : val Λ → iProp Λ Σ) : `````` Ralf Jung committed Feb 09, 2016 94 `````` atomic e → nclose N ⊆ E → `````` Ralf Jung committed Feb 09, 2016 95 `````` (inv N P ∧ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v)))%I ⊑ wp E e Q. `````` Ralf Jung committed Feb 09, 2016 96 ``````Proof. `````` Ralf Jung committed Feb 09, 2016 97 `````` move=>He HN. `````` Ralf Jung committed Feb 09, 2016 98 99 100 101 102 103 104 105 `````` 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 106 `````` rewrite (commutative _ (▷_)%I) -associative wand_elim_r wp_frame_l. `````` Ralf Jung committed Feb 09, 2016 107 108 109 110 111 `````` 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 112 ``````Lemma pvs_alloc N P : ▷ P ⊑ pvs N N (inv N P). `````` Robbert Krebbers committed Feb 10, 2016 113 ``````Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed. `````` Ralf Jung committed Feb 09, 2016 114 115 `````` End inv.``````