invariants.v 4.92 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 `````` `````` Ralf Jung committed Feb 10, 2016 11 `````` `````` Robbert Krebbers committed Jan 16, 2016 12 13 ``````Definition namespace := list positive. Definition nnil : namespace := nil. `````` Ralf Jung committed Feb 08, 2016 14 15 ``````Definition ndot `{Countable A} (N : namespace) (x : A) : namespace := encode x :: N. `````` Ralf Jung committed Feb 08, 2016 16 ``````Coercion nclose (N : namespace) : coPset := coPset_suffixes (encode N). `````` Robbert Krebbers committed Jan 16, 2016 17 18 `````` Instance ndot_injective `{Countable A} : Injective2 (=) (=) (=) (@ndot A _ _). `````` Ralf Jung committed Feb 08, 2016 19 ``````Proof. by intros N1 x1 N2 x2 ?; simplify_equality. Qed. `````` Robbert Krebbers committed Jan 16, 2016 20 21 ``````Lemma nclose_nnil : nclose nnil = coPset_all. Proof. by apply (sig_eq_pi _). Qed. `````` Ralf Jung committed Feb 08, 2016 22 ``````Lemma encode_nclose N : encode N ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 23 ``````Proof. by apply elem_coPset_suffixes; exists xH; rewrite (left_id_L _ _). Qed. `````` Ralf Jung committed Feb 08, 2016 24 ``````Lemma nclose_subseteq `{Countable A} N x : nclose (ndot N x) ⊆ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 25 26 ``````Proof. intros p; rewrite /nclose !elem_coPset_suffixes; intros [q ->]. `````` Ralf Jung committed Feb 08, 2016 27 `````` destruct (list_encode_suffix N (ndot N x)) as [q' ?]; [by exists [encode x]|]. `````` Robbert Krebbers committed Jan 16, 2016 28 29 `````` by exists (q ++ q')%positive; rewrite <-(associative_L _); f_equal. Qed. `````` Ralf Jung committed Feb 08, 2016 30 ``````Lemma ndot_nclose `{Countable A} N x : encode (ndot N x) ∈ nclose N. `````` Robbert Krebbers committed Jan 16, 2016 31 ``````Proof. apply nclose_subseteq with x, encode_nclose. Qed. `````` Ralf Jung committed Feb 08, 2016 32 33 ``````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 34 35 36 37 38 39 40 41 ``````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 42 43 ``````Qed. `````` Ralf Jung committed Feb 09, 2016 44 45 ``````Local Hint Resolve nclose_subseteq ndot_nclose. `````` Ralf Jung committed Feb 08, 2016 46 47 ``````(** Derived forms and lemmas about them. *) Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ := `````` Robbert Krebbers committed Feb 10, 2016 48 49 50 `````` (∃ i, ■ (i ∈ nclose N) ∧ ownI i P)%I. Instance: Params (@inv) 3. Typeclasses Opaque inv. `````` Ralf Jung committed Feb 09, 2016 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). `````` Robbert Krebbers committed Feb 10, 2016 59 ``````Proof. intros n ???. apply exists_ne=>i. by apply and_ne, ownI_contractive. Qed. `````` Ralf Jung committed Feb 09, 2016 60 `````` `````` Robbert Krebbers committed Feb 10, 2016 61 62 ``````Global Instance inv_always_stable N P : AlwaysStable (inv N P). Proof. rewrite /inv; apply _. Qed. `````` Ralf Jung committed Feb 09, 2016 63 64 65 66 `````` 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 11, 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 11, 2016 79 80 `````` rewrite /inv sep_exist_r. apply exist_elim=>i. rewrite always_and_sep_l' -associative. apply const_elim_sep_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 11, 2016 84 `````` rewrite (always_sep_dup' (ownI _ _)). `````` Ralf Jung committed Feb 09, 2016 85 `````` 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 11, 2016 95 `````` (inv N P ★ (▷P -★ wp (E ∖ nclose N) e (λ v, ▷P ★ Q v))) ⊑ 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 11, 2016 98 99 `````` rewrite /inv sep_exist_r. apply exist_elim=>i. rewrite always_and_sep_l' -associative. apply const_elim_sep_l=>HiN. `````` Ralf Jung committed Feb 09, 2016 100 101 102 `````` 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. `````` Ralf Jung committed Feb 11, 2016 103 `````` rewrite (always_sep_dup' (ownI _ _)). `````` Ralf Jung committed Feb 09, 2016 104 105 `````` 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 10, 2016 112 ``````Lemma inv_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.``````