Commit 4064c62e by Robbert Krebbers

### Disjointness of sets.

parent 71667413
 ... ... @@ -26,17 +26,16 @@ Context {sts : stsT}. (** ** Step relations *) Inductive step : relation (state sts * tokens sts) := | Step s1 s2 T1 T2 : (* TODO: This asks for ⊥ on sets: T1 ⊥ T2 := T1 ∩ T2 ⊆ ∅. *) prim_step s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ → prim_step s1 s2 → tok s1 ⊥ T1 → tok s2 ⊥ T2 → tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2). Notation steps := (rtc step). Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop := | Frame_step T1 T2 : T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2. T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2. (** ** Closure under frame steps *) Record closed (S : states sts) (T : tokens sts) : Prop := Closed { closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅; closed_disjoint s : s ∈ S → tok s ⊥ T; closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S }. Definition up (s : state sts) (T : tokens sts) : states sts := ... ... @@ -50,6 +49,7 @@ Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 50 (_ ∈ _) => set_solver : sts. Hint Extern 50 (_ ⊆ _) => set_solver : sts. Hint Extern 50 (_ ⊥ _) => set_solver : sts. (** ** Setoids *) Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step. ... ... @@ -60,10 +60,7 @@ Qed. Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step. Proof. by intros ?? [??] ??????; split; apply framestep_mono. Qed. Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed. Proof. intros ?? HT ?? HS; destruct 1; constructor; intros until 0; rewrite -?HS -?HT; eauto. Qed. Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed. Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed. Proof. by split; apply closed_proper'. Qed. Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up. ... ... @@ -95,16 +92,16 @@ Proof. - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts. Qed. Lemma step_closed s1 s2 T1 T2 S Tf : step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ → s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ⊥ Tf → s2 ∈ S ∧ T2 ⊥ Tf ∧ tok s2 ⊥ T2. Proof. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto. - eapply Hstep with s1, Frame_step with T1 T2; auto with sts. - set_solver -Hstep Hs1 Hs2. Qed. Lemma steps_closed s1 s2 T1 T2 S Tf : steps (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ → tok s1 ∩ T1 ≡ ∅ → s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. steps (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ⊥ Tf → tok s1 ⊥ T1 → s2 ∈ S ∧ T2 ⊥ Tf ∧ tok s2 ⊥ T2. Proof. remember (s1,T1) as sT1 eqn:HsT1; remember (s2,T2) as sT2 eqn:HsT2. intros Hsteps; revert s1 T1 HsT1 s2 T2 HsT2. ... ... @@ -120,8 +117,7 @@ Lemma subseteq_up_set S T : S ⊆ up_set S T. Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T. Proof. by rewrite /up_set collection_bind_singleton. Qed. Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → closed (up_set S T) T. Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ⊥ T) → closed (up_set S T) T. Proof. intros HS; unfold up_set; split. - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). ... ... @@ -131,7 +127,7 @@ Proof. - intros s1 s2; rewrite /up; set_unfold; intros (s&?&?) ?; exists s. split; [eapply rtc_r|]; eauto. Qed. Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T. Lemma closed_up s T : tok s ⊥ T → closed (up s T) T. Proof. intros; rewrite -(collection_bind_singleton (λ s, up s T) s). apply closed_up_set; set_solver. ... ... @@ -188,7 +184,7 @@ Inductive sts_equiv : Equiv (car sts) := Global Existing Instance sts_equiv. Global Instance sts_valid : Valid (car sts) := λ x, match x with | auth s T => tok s ∩ T ≡ ∅ | auth s T => tok s ⊥ T | frag S' T => closed S' T ∧ S' ≢ ∅ end. Global Instance sts_core : Core (car sts) := λ x, ... ... @@ -198,11 +194,9 @@ Global Instance sts_core : Core (car sts) := λ x, end. Inductive sts_disjoint : Disjoint (car sts) := | frag_frag_disjoint S1 S2 T1 T2 : S1 ∩ S2 ≢ ∅ → T1 ∩ T2 ≡ ∅ → frag S1 T1 ⊥ frag S2 T2 | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → auth s T1 ⊥ frag S T2 | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → frag S T1 ⊥ auth s T2. S1 ∩ S2 ≢ ∅ → T1 ⊥ T2 → frag S1 T1 ⊥ frag S2 T2 | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → auth s T1 ⊥ frag S T2 | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ⊥ T2 → frag S T1 ⊥ auth s T2. Global Existing Instance sts_disjoint. Global Instance sts_op : Op (car sts) := λ x1 x2, match x1, x2 with ... ... @@ -216,6 +210,8 @@ Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts. Hint Extern 50 (_ ∈ _) => set_solver : sts. Hint Extern 50 (_ ⊆ _) => set_solver : sts. Hint Extern 50 (_ ⊥ _) => set_solver : sts. Global Instance sts_equivalence: Equivalence ((≡) : relation (car sts)). Proof. split. ... ... @@ -303,11 +299,11 @@ Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s). Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed. (** Validity *) Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ∩ T ≡ ∅. Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ⊥ T. Proof. done. Qed. Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅. Proof. done. Qed. Lemma sts_frag_up_valid s T : tok s ∩ T ≡ ∅ → ✓ sts_frag_up s T. Lemma sts_frag_up_valid s T : tok s ⊥ T → ✓ sts_frag_up s T. Proof. intros. by apply sts_frag_valid; auto using closed_up, up_non_empty. Qed. Lemma sts_auth_frag_valid_inv s S T1 T2 : ... ... @@ -335,7 +331,7 @@ Proof. Qed. Lemma sts_op_frag S1 S2 T1 T2 : T1 ∩ T2 ≡ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 → sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2. Proof. intros HT HS1 HS2. rewrite /sts_frag. ... ... @@ -390,7 +386,7 @@ Qed. Lemma sts_frag_included S1 S2 T1 T2 : closed S2 T2 → S2 ≢ ∅ → (sts_frag S1 T1 ≼ sts_frag S2 T2) ↔ (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ (closed S1 T1 ∧ S1 ≢ ∅ ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ⊥ Tf ∧ S2 ≡ S1 ∩ up_set S2 Tf). Proof. intros ??; split. ... ...
 ... ... @@ -5,9 +5,11 @@ importantly, it implements some tactics to automatically solve goals involving collections. *) From iris.prelude Require Export base tactics orders. Instance collection_disjoint `{ElemOf A C} : Disjoint C := λ X Y, ∀ x, x ∈ X → x ∈ Y → False. Instance collection_subseteq `{ElemOf A C} : SubsetEq C := λ X Y, ∀ x, x ∈ X → x ∈ Y. Typeclasses Opaque collection_subseteq. Typeclasses Opaque collection_disjoint collection_subseteq. (** * Basic theorems *) Section simple_collection. ... ... @@ -36,6 +38,9 @@ Section simple_collection. Proof. firstorder. Qed. Lemma elem_of_equiv_empty X : X ≡ ∅ ↔ ∀ x, x ∉ X. Proof. firstorder. Qed. Lemma elem_of_disjoint X Y : X ⊥ Y ↔ ∀ x, x ∈ X → x ∈ Y → False. Proof. done. Qed. Lemma collection_positive_l X Y : X ∪ Y ≡ ∅ → X ≡ ∅. Proof. rewrite !elem_of_equiv_empty. setoid_rewrite elem_of_union. naive_solver. ... ... @@ -52,11 +57,14 @@ Section simple_collection. - intros ??. rewrite elem_of_singleton. by intros ->. - intros Ex. by apply (Ex x), elem_of_singleton. Qed. Global Instance singleton_proper : Proper ((=) ==> (≡)) (singleton (B:=C)). Proof. by repeat intro; subst. Qed. Global Instance elem_of_proper : Proper ((=) ==> (≡) ==> iff) ((∈) : A → C → Prop) | 5. Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5. Proof. intros ???; subst. firstorder. Qed. Global Instance disjoint_prope : Proper ((≡) ==> (≡) ==> iff) (@disjoint C _). Proof. intros ??????. by rewrite !elem_of_disjoint; setoid_subst. Qed. Lemma elem_of_union_list Xs x : x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X. Proof. split. ... ... @@ -196,6 +204,10 @@ Section set_unfold_simple. constructor. rewrite subset_spec, elem_of_subseteq, elem_of_equiv. repeat f_equiv; naive_solver. Qed. Global Instance set_unfold_disjoint (P Q : A → Prop) : (∀ x, SetUnfold (x ∈ X) (P x)) → (∀ x, SetUnfold (x ∈ Y) (Q x)) → SetUnfold (X ⊥ Y) (∀ x, P x → Q x → False). Proof. constructor. rewrite elem_of_disjoint. naive_solver. Qed. Context `{!LeibnizEquiv C}. Global Instance set_unfold_equiv_same_L X : SetUnfold (X = X) True | 1. ... ... @@ -387,7 +399,7 @@ Section collection. Proof. set_solver. Qed. Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z. Proof. set_solver. Qed. Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y. Lemma disjoint_union_difference X Y : X ⊥ Y → (X ∪ Y) ∖ X ≡ Y. Proof. set_solver. Qed. Section leibniz. ... ... @@ -407,7 +419,7 @@ Section collection. Lemma difference_intersection_distr_l_L X Y Z : (X ∩ Y) ∖ Z = X ∖ Z ∩ Y ∖ Z. Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed. Lemma disjoint_union_difference_L X Y : X ∩ Y = ∅ → (X ∪ Y) ∖ X = Y. Lemma disjoint_union_difference_L X Y : X ⊥ Y → (X ∪ Y) ∖ X = Y. Proof. unfold_leibniz. apply disjoint_union_difference. Qed. End leibniz. ... ...
 ... ... @@ -92,9 +92,9 @@ Proof. - rewrite elem_of_singleton. eauto using size_singleton_inv. - set_solver. Qed. Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y. Lemma size_union X Y : X ⊥ Y → size (X ∪ Y) = size X + size Y. Proof. intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length. intros. unfold size, collection_size. simpl. rewrite <-app_length. apply Permutation_length, NoDup_Permutation. - apply NoDup_elements. - apply NoDup_app; repeat split; try apply NoDup_elements. ... ...
 ... ... @@ -74,15 +74,14 @@ Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed. Lemma delete_insert_dom {A} (m : M A) i x : i ∉ dom D m → delete i (<[i:=x]>m) = m. Proof. rewrite not_elem_of_dom. apply delete_insert. Qed. Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ∩ dom D m2 ≡ ∅. Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ⊥ dom D m2. Proof. rewrite map_disjoint_spec, elem_of_equiv_empty. setoid_rewrite elem_of_intersection. rewrite map_disjoint_spec, elem_of_disjoint. setoid_rewrite elem_of_dom. unfold is_Some. naive_solver. Qed. Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → dom D m1 ∩ dom D m2 ≡ ∅. Lemma map_disjoint_dom_1 {A} (m1 m2 : M A) : m1 ⊥ₘ m2 → dom D m1 ⊥ dom D m2. Proof. apply map_disjoint_dom. Qed. Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ∩ dom D m2 ≡ ∅ → m1 ⊥ₘ m2. Lemma map_disjoint_dom_2 {A} (m1 m2 : M A) : dom D m1 ⊥ dom D m2 → m1 ⊥ₘ m2. Proof. apply map_disjoint_dom. Qed. Lemma dom_union {A} (m1 m2 : M A) : dom D (m1 ∪ m2) ≡ dom D m1 ∪ dom D m2. Proof. ... ... @@ -90,8 +89,7 @@ Proof. unfold is_Some. setoid_rewrite lookup_union_Some_raw. destruct (m1 !! i); naive_solver. Qed. Lemma dom_intersection {A} (m1 m2 : M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2. Lemma dom_intersection {A} (m1 m2: M A) : dom D (m1 ∩ m2) ≡ dom D m1 ∩ dom D m2. Proof. apply elem_of_equiv. intros i. rewrite elem_of_intersection, !elem_of_dom. unfold is_Some. setoid_rewrite lookup_intersection_Some. naive_solver. ... ...
 From iris.program_logic Require Export hoare. From iris.program_logic Require Import wsat ownership. Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver. Local Hint Extern 100 (_ ⊥ _) => set_solver. Local Hint Extern 10 (✓{_} _) => repeat match goal with | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega ... ... @@ -151,5 +151,4 @@ Proof. intros ? Hht. eapply wp_adequacy_safe with (E:=E) (Φ:=Φ); first done. move:Hht. by rewrite /ht uPred.always_elim=>/uPred.impl_entails. Qed. End adequacy.
 From iris.program_logic Require Export weakestpre. From iris.program_logic Require Import wsat ownership. Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => set_solver. Local Hint Extern 100 (_ ⊥ _) => set_solver. Local Hint Extern 10 (✓{_} _) => repeat match goal with | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega ... ...
 ... ... @@ -49,13 +49,11 @@ Section ndisjoint. Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ N2 .@ x . Proof. rewrite ![N1 ⊥ _]comm. apply ndot_preserve_disjoint_l. Qed. Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ∩ nclose N2 = ∅. Lemma ndisj_disjoint N1 N2 : N1 ⊥ N2 → nclose N1 ⊥ nclose N2. Proof. intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne). apply elem_of_equiv_empty_L=> p; unfold nclose. rewrite elem_of_intersection !elem_coPset_suffixes; intros [[q ->] [q' Hq]]. rewrite !list_encode_app !assoc in Hq. by eapply Hne, list_encode_suffix_eq. intros (N1' & N2' & [N1'' ->] & [N2'' ->] & Hl & Hne) p; unfold nclose. rewrite !elem_coPset_suffixes; intros [q ->] [q' Hq]; destruct Hne. by rewrite !list_encode_app !assoc in Hq; apply list_encode_suffix_eq in Hq. Qed. End ndisjoint. ... ... @@ -63,20 +61,19 @@ End ndisjoint. of masks (i.e., coPsets) with set_solver, taking disjointness of namespaces into account. *) (* TODO: This tactic is by far now yet as powerful as it should be. For example, given N1 ⊥ N2, it should be able to solve nclose (ndot N1 x) ∩ N2 ≡ ∅. It should also solve (ndot N x) ∩ (ndot N y) ≡ ∅ if x ≠ y is in the context or For example, given [N1 ⊥ N2], it should be able to solve [nclose (ndot N1 x) ⊥ N2]. It should also solve [ndot N x ⊥ ndot N y] if x ≠ y is in the context or follows from [discriminate]. *) Ltac set_solver_ndisj := repeat match goal with (* TODO: Restrict these to have type namespace *) | [ H : (?N1 ⊥ ?N2) |-_ ] => apply ndisj_disjoint in H end; set_solver. (* TODO: Restrict these to have type namespace *) | [ H : ?N1 ⊥ ?N2 |-_ ] => apply ndisj_disjoint in H end; set_solver. (* TODO: restrict this to match only if this is ⊆ of coPset *) Hint Extern 500 (_ ⊆ _) => set_solver_ndisj : ndisj. (* The hope is that registering these will suffice to solve most goals of the form N1 ⊥ N2. of the form [N1 ⊥ N2]. TODO: Can this prove x ≠ y if discriminate can? *) Hint Resolve ndot_ne_disjoint : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj. ... ...
 ... ... @@ -2,7 +2,7 @@ From iris.prelude Require Export co_pset. From iris.program_logic Require Export model. From iris.program_logic Require Import ownership wsat. Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => set_solver. Local Hint Extern 100 (_ ⊥ _) => set_solver. Local Hint Extern 100 (_ ∉ _) => set_solver. Local Hint Extern 10 (✓{_} _) => repeat match goal with ... ... @@ -11,7 +11,7 @@ Local Hint Extern 10 (✓{_} _) => Program Definition pvs_def {Λ Σ} (E1 E2 : coPset) (P : iProp Λ Σ) : iProp Λ Σ := {| uPred_holds n r1 := ∀ rf k Ef σ, 0 < k ≤ n → (E1 ∪ E2) ∩ Ef = ∅ → 0 < k ≤ n → E1 ∪ E2 ⊥ Ef → wsat k (E1 ∪ Ef) σ (r1 ⋅ rf) → ∃ r2, P k r2 ∧ wsat k (E2 ∪ Ef) σ (r2 ⋅ rf) |}. Next Obligation. ... ... @@ -84,7 +84,7 @@ Proof. destruct (HP1 rf k Ef σ) as (r2&HP2&?); auto. Qed. Lemma pvs_mask_frame E1 E2 Ef P : Ef ∩ (E1 ∪ E2) = ∅ → (|={E1,E2}=> P) ⊢ (|={E1 ∪ Ef,E2 ∪ Ef}=> P). Ef ⊥ E1 ∪ E2 → (|={E1,E2}=> P) ⊢ (|={E1 ∪ Ef,E2 ∪ Ef}=> P). Proof. rewrite pvs_eq. intros ?; split=> n r ? HP rf k Ef' σ ???. destruct (HP rf k (Ef∪Ef') σ) as (r'&?&?); rewrite ?(assoc_L _); eauto. ... ... @@ -244,6 +244,5 @@ Proof. Qed. Lemma pvs_mk_fsa {Λ Σ} E (P Q : iProp Λ Σ) : P ⊢ pvs_fsa E (λ _, Q) → P ⊢ |={E}=> Q. P ⊢ pvs_fsa E (λ _, Q) → P ⊢ |={E}=> Q. Proof. by intros ?. Qed.
 ... ... @@ -72,7 +72,7 @@ Section sts. Proof. intros ???. by apply own_update, sts_update_frag_up. Qed. Lemma sts_ownS_op γ S1 S2 T1 T2 : T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → T1 ⊥ T2 → sts.closed S1 T1 → sts.closed S2 T2 → sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2). Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed. ... ...
 ... ... @@ -78,18 +78,17 @@ Lemma vs_frame_r E1 E2 P Q R : (P ={E1,E2}=> Q) ⊢ (P ★ R ={E1,E2}=> Q ★ R) Proof. rewrite !(comm _ _ R); apply vs_frame_l. Qed. Lemma vs_mask_frame E1 E2 Ef P Q : Ef ∩ (E1 ∪ E2) = ∅ → (P ={E1,E2}=> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q). Ef ⊥ E1 ∪ E2 → (P ={E1,E2}=> Q) ⊢ (P ={E1 ∪ Ef,E2 ∪ Ef}=> Q). Proof. intros ?; apply always_intro', impl_intro_l; rewrite (pvs_mask_frame _ _ Ef)//. by rewrite always_elim impl_elim_r. Qed. Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q). Lemma vs_mask_frame' E Ef P Q : Ef ⊥ E → (P ={E}=> Q) ⊢ (P ={E ∪ Ef}=> Q). Proof. intros; apply vs_mask_frame; set_solver. Qed. Lemma vs_inv N E P Q R : nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q). nclose N ⊆ E → (inv N R ★ (▷ R ★ P ={E ∖ nclose N}=> ▷ R ★ Q)) ⊢ (P ={E}=> Q). Proof. intros; apply: always_intro. apply impl_intro_l. rewrite always_and_sep_r assoc [(P ★ _)%I]comm -assoc. ... ...
 From iris.program_logic Require Export pviewshifts. From iris.program_logic Require Import wsat. Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver. Local Hint Extern 100 (_ ∉ _) => set_solver. Local Hint Extern 100 (_ ⊥ _) => set_solver. Local Hint Extern 100 (_ ∉_) => set_solver. Local Hint Extern 100 (@subseteq coPset _ _ _) => set_solver. Local Hint Extern 10 (✓{_} _) => repeat match goal with ... ... @@ -25,7 +25,7 @@ CoInductive wp_pre {Λ Σ} (E : coPset) | wp_pre_step n r1 e1 : to_val e1 = None → (∀ rf k Ef σ1, 0 < k < n → E ∩ Ef = ∅ → 0 < k < n → E ⊥ Ef → wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) → wp_go (E ∪ Ef) (wp_pre E Φ) (wp_pre ⊤ (λ _, True%I)) k rf e1 σ1) → ... ... @@ -122,7 +122,7 @@ Proof. by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq. Qed. Lemma wp_step_inv E Ef Φ e k n σ r rf : to_val e = None → 0 < k < n → E ∩ Ef = ∅ → to_val e = None → 0 < k < n → E ⊥ Ef → wp_def E e Φ n r → wsat (S k) (E ∪ Ef) σ (r ⋅ rf) → wp_go (E ∪ Ef) (λ e, wp_def E e Φ) (λ e, wp_def ⊤ e (λ _, True%I)) k rf e σ. Proof. ... ...
 From Coq Require Import Wf_nat. From iris.program_logic Require Import weakestpre wsat. Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 10 (@eq coPset _ _) => set_solver. Local Hint Extern 10 (_ ⊥ _) => set_solver. Local Hint Extern 10 (✓{_} _) => repeat match goal with | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega ... ... @@ -19,7 +19,7 @@ Program Definition wp_pre (wp : coPsetC -n> exprC Λ -n> (valC Λ -n> iProp) -n> iProp) (E : coPset) (e1 : expr Λ) (Φ : valC Λ -n> iProp) : iProp := {| uPred_holds n r1 := ∀ rf k Ef σ1, 0 ≤ k < n → E ∩ Ef = ∅ → 0 ≤ k < n → E ⊥ Ef → wsat (S k) (E ∪ Ef) σ1 (r1 ⋅ rf) → (∀ v, to_val e1 = Some v → ∃ r2, Φ v (S k) r2 ∧ wsat (S k) (E ∪ Ef) σ1 (r2 ⋅ rf)) ∧ ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment