dra.v 7.1 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export cmra. `````` Robbert Krebbers committed Nov 11, 2015 2 3 4 5 6 7 8 9 10 11 12 13 14 15 `````` (** From disjoint pcm *) Record validity {A} (P : A → Prop) : Type := Validity { validity_car : A; validity_is_valid : Prop; validity_prf : validity_is_valid → P validity_car }. Arguments Validity {_ _} _ _ _. Arguments validity_car {_ _} _. Arguments validity_is_valid {_ _} _. Definition to_validity {A} {P : A → Prop} (x : A) : validity P := Validity x (P x) id. `````` Robbert Krebbers committed Nov 20, 2015 16 ``````Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y, `````` Robbert Krebbers committed Nov 23, 2015 17 `````` ∃ z, y ≡ x ⋅ z ∧ ✓ z ∧ x ⊥ z. `````` Robbert Krebbers committed Nov 20, 2015 18 19 20 ``````Instance: Params (@dra_included) 4. Local Infix "≼" := dra_included. `````` Ralf Jung committed Mar 08, 2016 21 ``````Class DRA A `{Equiv A, Valid A, Core A, Disjoint A, Op A, Div A} := { `````` Robbert Krebbers committed Nov 11, 2015 22 23 24 `````` (* setoids *) dra_equivalence :> Equivalence ((≡) : relation A); dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅); `````` Ralf Jung committed Mar 08, 2016 25 `````` dra_core_proper :> Proper ((≡) ==> (≡)) core; `````` Robbert Krebbers committed Feb 16, 2016 26 `````` dra_valid_proper :> Proper ((≡) ==> impl) valid; `````` Robbert Krebbers committed Nov 11, 2015 27 `````` dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x); `````` Ralf Jung committed Feb 29, 2016 28 `````` dra_div_proper :> Proper ((≡) ==> (≡) ==> (≡)) div; `````` Robbert Krebbers committed Nov 11, 2015 29 `````` (* validity *) `````` Robbert Krebbers committed Nov 23, 2015 30 `````` dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y); `````` Ralf Jung committed Mar 08, 2016 31 `````` dra_core_valid x : ✓ x → ✓ core x; `````` Ralf Jung committed Feb 29, 2016 32 `````` dra_div_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ÷ x); `````` Robbert Krebbers committed Nov 11, 2015 33 `````` (* monoid *) `````` Robbert Krebbers committed Feb 11, 2016 34 `````` dra_assoc :> Assoc (≡) (⋅); `````` Robbert Krebbers committed Nov 23, 2015 35 36 `````` dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z; dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z; `````` Robbert Krebbers committed Nov 11, 2015 37 `````` dra_symmetric :> Symmetric (@disjoint A _); `````` Robbert Krebbers committed Feb 11, 2016 38 `````` dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x; `````` Ralf Jung committed Mar 08, 2016 39 40 41 42 `````` dra_core_disjoint_l x : ✓ x → core x ⊥ x; dra_core_l x : ✓ x → core x ⋅ x ≡ x; dra_core_idemp x : ✓ x → core (core x) ≡ core x; dra_core_preserving x y : ✓ x → ✓ y → x ≼ y → core x ≼ core y; `````` Ralf Jung committed Feb 29, 2016 43 44 `````` dra_disjoint_div x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ÷ x; dra_op_div x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ÷ x ≡ y `````` Robbert Krebbers committed Nov 11, 2015 45 46 47 48 49 ``````}. Section dra. Context A `{DRA A}. Arguments valid _ _ !_ /. `````` Robbert Krebbers committed Nov 20, 2015 50 ``````Hint Immediate dra_op_proper : typeclass_instances. `````` Robbert Krebbers committed Nov 11, 2015 51 `````` `````` Robbert Krebbers committed Feb 16, 2016 52 53 54 55 56 57 58 59 ``````Notation T := (validity (valid : A → Prop)). Instance validity_valid : Valid T := validity_is_valid. Instance validity_equiv : Equiv T := λ x y, (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y). Instance validity_equivalence : Equivalence ((≡) : relation T). Proof. split; unfold equiv, validity_equiv. `````` Robbert Krebbers committed Feb 17, 2016 60 61 62 `````` - 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 63 `````` split; [|intros; trans y]; tauto. `````` Robbert Krebbers committed Feb 16, 2016 64 ``````Qed. `````` Robbert Krebbers committed Feb 16, 2016 65 66 67 68 ``````Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop). Proof. by split; apply dra_valid_proper. Qed. Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity. Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed. `````` Robbert Krebbers committed Nov 20, 2015 69 ``````Instance: Proper ((≡) ==> (≡) ==> iff) (⊥). `````` Robbert Krebbers committed Nov 11, 2015 70 ``````Proof. `````` Robbert Krebbers committed Nov 20, 2015 71 `````` intros x1 x2 Hx y1 y2 Hy; split. `````` Robbert Krebbers committed Feb 17, 2016 72 73 `````` - 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 74 ``````Qed. `````` Robbert Krebbers committed Nov 23, 2015 75 ``````Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y. `````` Robbert Krebbers committed Nov 11, 2015 76 ``````Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed. `````` Robbert Krebbers committed Nov 23, 2015 77 ``````Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z. `````` Robbert Krebbers committed Feb 11, 2016 78 ``````Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed. `````` Robbert Krebbers committed Nov 11, 2015 79 ``````Lemma dra_disjoint_move_r x y z : `````` Robbert Krebbers committed Nov 23, 2015 80 `````` ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z. `````` Robbert Krebbers committed Nov 11, 2015 81 ``````Proof. `````` Robbert Krebbers committed Feb 11, 2016 82 83 `````` 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 84 ``````Qed. `````` Robbert Krebbers committed Nov 20, 2015 85 86 ``````Hint Immediate dra_disjoint_move_l dra_disjoint_move_r. Hint Unfold dra_included. `````` Robbert Krebbers committed Nov 11, 2015 87 `````` `````` Robbert Krebbers committed Feb 11, 2016 88 ``````Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z. `````` Robbert Krebbers committed Nov 22, 2015 89 90 ``````Proof. apply validity_prf. Qed. Hint Resolve validity_valid_car_valid. `````` Ralf Jung committed Mar 08, 2016 91 92 93 ``````Program Instance validity_core : Core T := λ x, Validity (core (validity_car x)) (✓ x) _. Solve Obligations with naive_solver auto using dra_core_valid. `````` Robbert Krebbers committed Nov 11, 2015 94 95 ``````Program Instance validity_op : Op T := λ x y, Validity (validity_car x ⋅ validity_car y) `````` Robbert Krebbers committed Nov 23, 2015 96 `````` (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _. `````` Robbert Krebbers committed Nov 22, 2015 97 ``````Solve Obligations with naive_solver auto using dra_op_valid. `````` Ralf Jung committed Feb 29, 2016 98 99 ``````Program Instance validity_div : Div T := λ x y, Validity (validity_car x ÷ validity_car y) `````` Robbert Krebbers committed Nov 23, 2015 100 `````` (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _. `````` Ralf Jung committed Feb 29, 2016 101 ``````Solve Obligations with naive_solver auto using dra_div_valid. `````` Robbert Krebbers committed Jan 13, 2016 102 `````` `````` Robbert Krebbers committed Feb 01, 2016 103 ``````Definition validity_ra : RA (discreteC T). `````` Robbert Krebbers committed Nov 11, 2015 104 105 ``````Proof. split. `````` Robbert Krebbers committed Feb 17, 2016 106 `````` - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq]. `````` Robbert Krebbers committed Feb 19, 2016 107 `````` split; intros (?&?&?); split_and!; `````` Robbert Krebbers committed Jan 13, 2016 108 `````` first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto]. `````` Robbert Krebbers committed Feb 17, 2016 109 110 111 `````` - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq. - intros ?? [??]; naive_solver. - intros x1 x2 [? Hx] y1 y2 [? Hy]; `````` Robbert Krebbers committed Jan 13, 2016 112 `````` split; simpl; [|by intros (?&?&?); rewrite Hx // Hy]. `````` Robbert Krebbers committed Feb 19, 2016 113 `````` split; intros (?&?&z&?&?); split_and!; try tauto. `````` Robbert Krebbers committed Jan 13, 2016 114 115 `````` + exists z. by rewrite -Hy // -Hx. + exists z. by rewrite Hx ?Hy; tauto. `````` Robbert Krebbers committed Feb 17, 2016 116 `````` - intros [x px ?] [y py ?] [z pz ?]; split; simpl; `````` Robbert Krebbers committed Nov 20, 2015 117 `````` [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl `````` Robbert Krebbers committed Feb 11, 2016 118 `````` |by intros; rewrite assoc]. `````` Robbert Krebbers committed Feb 17, 2016 119 120 `````` - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm. - intros [x px ?]; split; `````` Ralf Jung committed Mar 08, 2016 121 122 123 `````` naive_solver eauto using dra_core_l, dra_core_disjoint_l. - intros [x px ?]; split; naive_solver eauto using dra_core_idemp. - intros x y Hxy; exists (core y ÷ core x). `````` Robbert Krebbers committed Nov 20, 2015 124 `````` destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *. `````` Ralf Jung committed Mar 08, 2016 125 126 `````` assert (py → core x ≼ core y) by intuition eauto 10 using dra_core_preserving. `````` Robbert Krebbers committed Nov 20, 2015 127 `````` constructor; [|symmetry]; simpl in *; `````` Ralf Jung committed Mar 08, 2016 128 `````` intuition eauto using dra_op_div, dra_disjoint_div, dra_core_valid. `````` Robbert Krebbers committed Feb 17, 2016 129 130 `````` - by intros [x px ?] [y py ?] (?&?&?). - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *; `````` Ralf Jung committed Feb 29, 2016 131 `````` intuition eauto 10 using dra_disjoint_div, dra_op_div. `````` Robbert Krebbers committed Nov 11, 2015 132 ``````Qed. `````` Robbert Krebbers committed Mar 01, 2016 133 ``````Definition validityR : cmraT := discreteR validity_ra. `````` Robbert Krebbers committed Feb 24, 2016 134 ``````Instance validity_cmra_discrete : `````` Robbert Krebbers committed Mar 01, 2016 135 `````` CMRADiscrete validityR := discrete_cmra_discrete _. `````` Robbert Krebbers committed Feb 24, 2016 136 `````` `````` Robbert Krebbers committed Mar 01, 2016 137 ``````Lemma validity_update (x y : validityR) : `````` Ralf Jung committed Feb 03, 2016 138 `````` (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y. `````` Robbert Krebbers committed Nov 11, 2015 139 ``````Proof. `````` Robbert Krebbers committed Feb 24, 2016 140 141 `````` intros Hxy; apply cmra_discrete_update=> z [?[??]]. split_and!; try eapply Hxy; eauto. `````` Robbert Krebbers committed Nov 11, 2015 142 ``````Qed. `````` Ralf Jung committed Feb 17, 2016 143 144 `````` Lemma to_validity_op (x y : A) : `````` 145 `````` (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) → `````` Ralf Jung committed Feb 17, 2016 146 `````` to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y. `````` Robbert Krebbers committed Feb 24, 2016 147 ``````Proof. split; naive_solver auto using dra_op_valid. Qed. `````` Ralf Jung committed Feb 17, 2016 148 `````` `````` Ralf Jung committed Feb 21, 2016 149 150 151 152 153 154 ``````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'. destruct Hvl' as [? [? ?]]. `````` Robbert Krebbers committed Feb 24, 2016 155 `````` split; first done. `````` Ralf Jung committed Feb 21, 2016 156 157 158 159 160 161 162 163 164 165 `````` exists (validity_car z). split_and!; last done. + apply EQ. assumption. + by apply validity_valid_car_valid. - intros (Hvl & z & EQ & ? & ?). assert (✓ y) by (rewrite EQ; apply dra_op_valid; done). split; first done. exists (to_validity z). split; first split. + intros _. simpl. split_and!; done. + intros _. setoid_subst. by apply dra_op_valid. + intros _. rewrite /= EQ //. Qed. `````` Robbert Krebbers committed Nov 11, 2015 166 ``End dra.``