Commit 9d06e3b7 by Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

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