dra.v 9.39 KB
 Robbert Krebbers committed Jun 16, 2016 1 ``````From iris.algebra Require Export cmra updates. `````` Ralf Jung committed Jan 05, 2017 2 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Nov 11, 2015 3 `````` `````` Robbert Krebbers committed Oct 25, 2017 4 ``````Record DraMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := { `````` Robbert Krebbers committed Nov 11, 2015 5 `````` (* setoids *) `````` Robbert Krebbers committed May 25, 2016 6 7 8 9 10 `````` mixin_dra_equivalence : Equivalence ((≡) : relation A); mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅); mixin_dra_core_proper : Proper ((≡) ==> (≡)) core; mixin_dra_valid_proper : Proper ((≡) ==> impl) valid; mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x); `````` Robbert Krebbers committed Nov 11, 2015 11 `````` (* validity *) `````` Robbert Krebbers committed May 25, 2016 12 13 `````` mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y); mixin_dra_core_valid x : ✓ x → ✓ core x; `````` Robbert Krebbers committed Nov 11, 2015 14 `````` (* monoid *) `````` Robbert Krebbers committed Oct 26, 2017 15 16 `````` mixin_dra_assoc x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z; `````` Robbert Krebbers committed May 25, 2016 17 18 19 20 21 22 23 24 `````` mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z; mixin_dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z; mixin_dra_symmetric : Symmetric (@disjoint A _); mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x; mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x; mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x; mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x; `````` Ralf Jung committed Jul 25, 2016 25 `````` mixin_dra_core_mono x y : `````` Robbert Krebbers committed Mar 11, 2016 26 `````` ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z `````` Robbert Krebbers committed Nov 11, 2015 27 ``````}. `````` Robbert Krebbers committed Oct 25, 2017 28 ``````Structure draT := DraT { `````` Robbert Krebbers committed May 25, 2016 29 30 31 32 33 34 `````` dra_car :> Type; dra_equiv : Equiv dra_car; dra_core : Core dra_car; dra_disjoint : Disjoint dra_car; dra_op : Op dra_car; dra_valid : Valid dra_car; `````` Robbert Krebbers committed Oct 25, 2017 35 `````` dra_mixin : DraMixin dra_car `````` Robbert Krebbers committed May 25, 2016 36 ``````}. `````` Robbert Krebbers committed Oct 25, 2017 37 ``````Arguments DraT _ {_ _ _ _ _} _. `````` Robbert Krebbers committed May 25, 2016 38 39 40 41 42 43 44 45 46 ``````Arguments dra_car : simpl never. Arguments dra_equiv : simpl never. Arguments dra_core : simpl never. Arguments dra_disjoint : simpl never. Arguments dra_op : simpl never. Arguments dra_valid : simpl never. Arguments dra_mixin : simpl never. Add Printing Constructor draT. Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid. `````` Robbert Krebbers committed Nov 11, 2015 47 `````` `````` Robbert Krebbers committed May 25, 2016 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 ``````(** Lifting properties from the mixin *) Section dra_mixin. Context {A : draT}. Implicit Types x y : A. Global Instance dra_equivalence : Equivalence ((≡) : relation A). Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed. Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _). Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed. Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _). Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed. Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _). Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed. Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x). Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed. Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y). Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed. Lemma dra_core_valid x : ✓ x → ✓ core x. Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed. `````` Robbert Krebbers committed Oct 26, 2017 66 67 `````` Lemma dra_assoc x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⋅ (y ⋅ z) ≡ (x ⋅ y) ⋅ z. `````` Robbert Krebbers committed May 25, 2016 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 `````` Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed. Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z. Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed. Lemma dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z. Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed. Global Instance dra_symmetric : Symmetric (@disjoint A _). Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed. Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x. Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed. Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x. Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed. Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x. Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed. Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x. Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed. `````` Ralf Jung committed Jul 25, 2016 84 `````` Lemma dra_core_mono x y : `````` Robbert Krebbers committed May 25, 2016 85 `````` ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z. `````` Ralf Jung committed Jul 25, 2016 86 `````` Proof. apply (mixin_dra_core_mono _ (dra_mixin A)). Qed. `````` Robbert Krebbers committed May 25, 2016 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 ``````End dra_mixin. Record validity (A : draT) := Validity { validity_car : A; validity_is_valid : Prop; validity_prf : validity_is_valid → valid validity_car }. Add Printing Constructor validity. Arguments Validity {_} _ _ _. Arguments validity_car {_} _. Arguments validity_is_valid {_} _. Definition to_validity {A : draT} (x : A) : validity A := Validity x (valid x) id. (* The actual construction *) `````` Robbert Krebbers committed Nov 11, 2015 103 ``````Section dra. `````` Robbert Krebbers committed May 25, 2016 104 105 106 ``````Context (A : draT). Implicit Types a b : A. Implicit Types x y z : validity A. `````` Robbert Krebbers committed Nov 11, 2015 107 ``````Arguments valid _ _ !_ /. `````` Robbert Krebbers committed Feb 16, 2016 108 `````` `````` Robbert Krebbers committed May 25, 2016 109 110 ``````Instance validity_valid : Valid (validity A) := validity_is_valid. Instance validity_equiv : Equiv (validity A) := λ x y, `````` Robbert Krebbers committed Feb 16, 2016 111 `````` (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y). `````` Robbert Krebbers committed May 25, 2016 112 ``````Instance validity_equivalence : Equivalence (@equiv (validity A) _). `````` Robbert Krebbers committed Feb 16, 2016 113 114 ``````Proof. split; unfold equiv, validity_equiv. `````` Robbert Krebbers committed Feb 17, 2016 115 116 117 `````` - by intros [x px ?]; simpl. - intros [x px ?] [y py ?]; naive_solver. - intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *. `````` Ralf Jung committed Feb 20, 2016 118 `````` split; [|intros; trans y]; tauto. `````` Robbert Krebbers committed Feb 16, 2016 119 ``````Qed. `````` Ralf Jung committed Nov 22, 2016 120 ``````Canonical Structure validityC : ofeT := discreteC (validity A). `````` Robbert Krebbers committed May 25, 2016 121 `````` `````` Robbert Krebbers committed Feb 16, 2016 122 ``````Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop). `````` Robbert Krebbers committed May 25, 2016 123 124 ``````Proof. by split; apply: dra_valid_proper. Qed. Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity. `````` Robbert Krebbers committed Feb 16, 2016 125 ``````Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed. `````` Robbert Krebbers committed May 25, 2016 126 ``````Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A). `````` Robbert Krebbers committed Nov 11, 2015 127 ``````Proof. `````` Robbert Krebbers committed Nov 20, 2015 128 `````` intros x1 x2 Hx y1 y2 Hy; split. `````` Robbert Krebbers committed Feb 17, 2016 129 130 `````` - by rewrite Hy (symmetry_iff (⊥) x1) (symmetry_iff (⊥) x2) Hx. - by rewrite -Hy (symmetry_iff (⊥) x2) (symmetry_iff (⊥) x1) -Hx. `````` Robbert Krebbers committed Nov 11, 2015 131 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 132 133 134 135 `````` Lemma dra_disjoint_rl a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b. Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed. Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c. `````` Robbert Krebbers committed Feb 11, 2016 136 ``````Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed. `````` Robbert Krebbers committed May 25, 2016 137 138 ``````Lemma dra_disjoint_move_r a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c. `````` Robbert Krebbers committed Nov 11, 2015 139 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 140 141 `````` intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl. apply dra_disjoint_move_l; auto; by rewrite dra_comm. `````` Robbert Krebbers committed Nov 11, 2015 142 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 143 ``````Hint Immediate dra_disjoint_move_l dra_disjoint_move_r. `````` Robbert Krebbers committed Nov 11, 2015 144 `````` `````` Robbert Krebbers committed May 25, 2016 145 ``````Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z. `````` Robbert Krebbers committed Nov 22, 2015 146 147 ``````Proof. apply validity_prf. Qed. Hint Resolve validity_valid_car_valid. `````` Robbert Krebbers committed May 28, 2016 148 149 ``````Program Instance validity_pcore : PCore (validity A) := λ x, Some (Validity (core (validity_car x)) (✓ x) _). `````` Robbert Krebbers committed May 25, 2016 150 151 ``````Solve Obligations with naive_solver eauto using dra_core_valid. Program Instance validity_op : Op (validity A) := λ x y, `````` Robbert Krebbers committed Nov 11, 2015 152 `````` Validity (validity_car x ⋅ validity_car y) `````` Robbert Krebbers committed Nov 23, 2015 153 `````` (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _. `````` Robbert Krebbers committed May 25, 2016 154 ``````Solve Obligations with naive_solver eauto using dra_op_valid. `````` Robbert Krebbers committed Jan 13, 2016 155 `````` `````` Robbert Krebbers committed May 25, 2016 156 ``````Definition validity_ra_mixin : RAMixin (validity A). `````` Robbert Krebbers committed Nov 11, 2015 157 ``````Proof. `````` Robbert Krebbers committed May 28, 2016 158 `````` apply ra_total_mixin; first eauto. `````` Robbert Krebbers committed Feb 17, 2016 159 `````` - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq]. `````` Robbert Krebbers committed Feb 19, 2016 160 `````` split; intros (?&?&?); split_and!; `````` Robbert Krebbers committed Jan 13, 2016 161 `````` first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto]. `````` Robbert Krebbers committed Feb 17, 2016 162 163 164 `````` - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq. - intros ?? [??]; naive_solver. - intros [x px ?] [y py ?] [z pz ?]; split; simpl; `````` Robbert Krebbers committed Nov 20, 2015 165 `````` [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl `````` Robbert Krebbers committed Oct 26, 2017 166 `````` |intuition eauto using dra_assoc, dra_disjoint_rl]. `````` Robbert Krebbers committed Feb 17, 2016 167 168 `````` - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm. - intros [x px ?]; split; `````` Ralf Jung committed Mar 08, 2016 169 170 `````` naive_solver eauto using dra_core_l, dra_core_disjoint_l. - intros [x px ?]; split; naive_solver eauto using dra_core_idemp. `````` Robbert Krebbers committed Mar 11, 2016 171 `````` - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *. `````` Ralf Jung committed Jul 25, 2016 172 `````` destruct (dra_core_mono x z) as (z'&Hz'). `````` Robbert Krebbers committed Aug 30, 2016 173 `````` unshelve eexists (Validity z' (px ∧ py ∧ pz) _). `````` Robbert Krebbers committed Mar 11, 2016 174 `````` { intros (?&?&?); apply Hz'; tauto. } `````` Robbert Krebbers committed Aug 30, 2016 175 176 `````` split; simpl; first tauto. intros. rewrite Hy //. tauto. `````` Robbert Krebbers committed Feb 17, 2016 177 `````` - by intros [x px ?] [y py ?] (?&?&?). `````` Robbert Krebbers committed Nov 11, 2015 178 ``````Qed. `````` Robbert Krebbers committed May 25, 2016 179 180 ``````Canonical Structure validityR : cmraT := discreteR (validity A) validity_ra_mixin. `````` Robbert Krebbers committed Feb 24, 2016 181 `````` `````` Robbert Krebbers committed Oct 25, 2017 182 ``````Global Instance validity_disrete_cmra : CmraDiscrete validityR. `````` Robbert Krebbers committed Feb 09, 2017 183 ``````Proof. apply discrete_cmra_discrete. Qed. `````` Robbert Krebbers committed Oct 25, 2017 184 185 ``````Global Instance validity_cmra_total : CmraTotal validityR. Proof. rewrite /CmraTotal; eauto. Qed. `````` Robbert Krebbers committed May 28, 2016 186 `````` `````` Robbert Krebbers committed May 25, 2016 187 188 ``````Lemma validity_update x y : (∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y. `````` Robbert Krebbers committed Nov 11, 2015 189 ``````Proof. `````` Robbert Krebbers committed Feb 24, 2016 190 191 `````` intros Hxy; apply cmra_discrete_update=> z [?[??]]. split_and!; try eapply Hxy; eauto. `````` Robbert Krebbers committed Nov 11, 2015 192 ``````Qed. `````` Ralf Jung committed Feb 17, 2016 193 `````` `````` Robbert Krebbers committed May 25, 2016 194 195 196 197 ``````Lemma to_validity_op a b : (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) → to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b. Proof. split; naive_solver eauto using dra_op_valid. Qed. `````` Ralf Jung committed Feb 17, 2016 198 `````` `````` Ralf Jung committed Mar 11, 2016 199 ``````(* TODO: This has to be proven again. *) `````` Robbert Krebbers committed Mar 11, 2016 200 ``````(* `````` Ralf Jung committed Feb 21, 2016 201 202 203 204 205 ``````Lemma to_validity_included x y: (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y). Proof. split. - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'. `````` Robbert Krebbers committed Mar 11, 2016 206 207 `````` destruct Hvl' as [? [? ?]]; split; first done. exists (validity_car z); eauto. `````` Ralf Jung committed Feb 21, 2016 208 `````` - intros (Hvl & z & EQ & ? & ?). `````` Robbert Krebbers committed Mar 11, 2016 209 `````` assert (✓ y) by (rewrite EQ; by apply dra_op_valid). `````` Ralf Jung committed Feb 21, 2016 210 `````` split; first done. exists (to_validity z). split; first split. `````` Robbert Krebbers committed Mar 11, 2016 211 `````` + intros _. simpl. by split_and!. `````` Ralf Jung committed Feb 21, 2016 212 213 214 `````` + intros _. setoid_subst. by apply dra_op_valid. + intros _. rewrite /= EQ //. Qed. `````` Robbert Krebbers committed Mar 11, 2016 215 ``````*) `````` Robbert Krebbers committed Nov 11, 2015 216 ``End dra.``