dra.v 6.25 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cmra. `````` Robbert Krebbers committed Nov 11, 2015 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 `````` (** 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. Instance validity_valid {A} (P : A → Prop) : Valid (validity P) := validity_is_valid. Instance validity_equiv `{Equiv A} (P : A → Prop) : Equiv (validity P) := λ x y, (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y). Instance validity_equivalence `{Equiv A,!Equivalence ((≡) : relation A)} P : Equivalence ((≡) : relation (validity P)). Proof. split; unfold equiv, validity_equiv. * by intros [x px ?]; simpl. * intros [x px ?] [y py ?]; naive_solver. * intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *. split; [|intros; transitivity y]; tauto. Qed. Instance validity_valid_proper `{Equiv A} (P : A → Prop) : `````` Robbert Krebbers committed Feb 11, 2016 29 `````` Proper ((≡) ==> iff) (valid : validity P → Prop). `````` Robbert Krebbers committed Nov 11, 2015 30 31 ``````Proof. intros ?? [??]; naive_solver. Qed. `````` Robbert Krebbers committed Nov 20, 2015 32 ``````Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y, `````` Robbert Krebbers committed Nov 23, 2015 33 `````` ∃ z, y ≡ x ⋅ z ∧ ✓ z ∧ x ⊥ z. `````` Robbert Krebbers committed Nov 20, 2015 34 35 36 37 ``````Instance: Params (@dra_included) 4. Local Infix "≼" := dra_included. Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := { `````` Robbert Krebbers committed Nov 11, 2015 38 39 40 41 42 43 44 `````` (* setoids *) dra_equivalence :> Equivalence ((≡) : relation A); dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅); dra_unit_proper :> Proper ((≡) ==> (≡)) unit; dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x); dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus; (* validity *) `````` Robbert Krebbers committed Nov 23, 2015 45 `````` dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y); `````` Robbert Krebbers committed Feb 11, 2016 46 `````` dra_unit_valid x : ✓ x → ✓ unit x; `````` Robbert Krebbers committed Nov 23, 2015 47 `````` dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x); `````` Robbert Krebbers committed Nov 11, 2015 48 49 `````` (* monoid *) dra_associative :> Associative (≡) (⋅); `````` Robbert Krebbers committed Nov 23, 2015 50 51 `````` 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 52 `````` dra_symmetric :> Symmetric (@disjoint A _); `````` Robbert Krebbers committed Nov 23, 2015 53 54 55 56 57 58 59 `````` dra_commutative x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x; dra_unit_disjoint_l x : ✓ x → unit x ⊥ x; dra_unit_l x : ✓ x → unit x ⋅ x ≡ x; dra_unit_idempotent x : ✓ x → unit (unit x) ≡ unit x; dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y; dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x; dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y `````` Robbert Krebbers committed Nov 11, 2015 60 61 62 63 64 ``````}. Section dra. Context A `{DRA A}. Arguments valid _ _ !_ /. `````` Robbert Krebbers committed Nov 20, 2015 65 ``````Hint Immediate dra_op_proper : typeclass_instances. `````` Robbert Krebbers committed Nov 11, 2015 66 `````` `````` Robbert Krebbers committed Nov 20, 2015 67 ``````Instance: Proper ((≡) ==> (≡) ==> iff) (⊥). `````` Robbert Krebbers committed Nov 11, 2015 68 ``````Proof. `````` Robbert Krebbers committed Nov 20, 2015 69 `````` intros x1 x2 Hx y1 y2 Hy; split. `````` Robbert Krebbers committed Jan 13, 2016 70 71 `````` * 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 72 ``````Qed. `````` Robbert Krebbers committed Nov 23, 2015 73 ``````Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y. `````` Robbert Krebbers committed Nov 11, 2015 74 ``````Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed. `````` Robbert Krebbers committed Nov 23, 2015 75 ``````Lemma dra_disjoint_lr x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z. `````` Robbert Krebbers committed Jan 13, 2016 76 ``````Proof. intros ????. rewrite dra_commutative //. by apply dra_disjoint_ll. Qed. `````` Robbert Krebbers committed Nov 11, 2015 77 ``````Lemma dra_disjoint_move_r x y z : `````` Robbert Krebbers committed Nov 23, 2015 78 `````` ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z. `````` Robbert Krebbers committed Nov 11, 2015 79 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 80 `````` intros; symmetry; rewrite dra_commutative; eauto using dra_disjoint_rl. `````` Robbert Krebbers committed Nov 11, 2015 81 82 `````` apply dra_disjoint_move_l; auto; by rewrite dra_commutative. Qed. `````` Robbert Krebbers committed Nov 20, 2015 83 84 ``````Hint Immediate dra_disjoint_move_l dra_disjoint_move_r. Hint Unfold dra_included. `````` Robbert Krebbers committed Nov 11, 2015 85 `````` `````` Robbert Krebbers committed Feb 11, 2016 86 87 ``````Notation T := (validity (valid : A → Prop)). Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z. `````` Robbert Krebbers committed Nov 22, 2015 88 89 ``````Proof. apply validity_prf. Qed. Hint Resolve validity_valid_car_valid. `````` Robbert Krebbers committed Nov 11, 2015 90 ``````Program Instance validity_unit : Unit T := λ x, `````` Robbert Krebbers committed Nov 23, 2015 91 `````` Validity (unit (validity_car x)) (✓ x) _. `````` Robbert Krebbers committed Nov 22, 2015 92 ``````Solve Obligations with naive_solver auto using dra_unit_valid. `````` Robbert Krebbers committed Nov 11, 2015 93 94 ``````Program Instance validity_op : Op T := λ x y, Validity (validity_car x ⋅ validity_car y) `````` Robbert Krebbers committed Nov 23, 2015 95 `````` (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _. `````` Robbert Krebbers committed Nov 22, 2015 96 ``````Solve Obligations with naive_solver auto using dra_op_valid. `````` Robbert Krebbers committed Nov 11, 2015 97 98 ``````Program Instance validity_minus : Minus T := λ x y, Validity (validity_car x ⩪ validity_car y) `````` Robbert Krebbers committed Nov 23, 2015 99 `````` (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _. `````` Robbert Krebbers committed Nov 22, 2015 100 ``````Solve Obligations with naive_solver auto using dra_minus_valid. `````` Robbert Krebbers committed Jan 13, 2016 101 `````` `````` Robbert Krebbers committed Feb 01, 2016 102 ``````Definition validity_ra : RA (discreteC T). `````` Robbert Krebbers committed Nov 11, 2015 103 104 105 106 ``````Proof. split. * intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq]. split; intros (?&?&?); split_ands'; `````` Robbert Krebbers committed Jan 13, 2016 107 `````` first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto]. `````` Robbert Krebbers committed Nov 11, 2015 108 `````` * by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq. `````` Robbert Krebbers committed Jan 13, 2016 109 `````` * by intros ?? -> ?. `````` Robbert Krebbers committed Nov 11, 2015 110 `````` * intros x1 x2 [? Hx] y1 y2 [? Hy]; `````` Robbert Krebbers committed Jan 13, 2016 111 `````` split; simpl; [|by intros (?&?&?); rewrite Hx // Hy]. `````` Robbert Krebbers committed Nov 20, 2015 112 `````` split; intros (?&?&z&?&?); split_ands'; try tauto. `````` Robbert Krebbers committed Jan 13, 2016 113 114 `````` + exists z. by rewrite -Hy // -Hx. + exists z. by rewrite Hx ?Hy; tauto. `````` Robbert Krebbers committed Nov 20, 2015 115 116 117 118 119 120 121 122 123 124 125 126 127 `````` * intros [x px ?] [y py ?] [z pz ?]; split; simpl; [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl |intros; apply (associative _)]. * intros [x px ?] [y py ?]; split; naive_solver eauto using dra_commutative. * intros [x px ?]; split; naive_solver eauto using dra_unit_l, dra_unit_disjoint_l. * intros [x px ?]; split; naive_solver eauto using dra_unit_idempotent. * intros x y Hxy; exists (unit y ⩪ unit x). destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *. assert (py → unit x ≼ unit y) by intuition eauto 10 using dra_unit_preserving. constructor; [|symmetry]; simpl in *; intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid. `````` Robbert Krebbers committed Nov 11, 2015 128 `````` * by intros [x px ?] [y py ?] (?&?&?). `````` Robbert Krebbers committed Nov 20, 2015 129 130 `````` * intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *; intuition eauto 10 using dra_disjoint_minus, dra_op_minus. `````` Robbert Krebbers committed Nov 11, 2015 131 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 132 ``````Definition validityRA : cmraT := discreteRA validity_ra. `````` Robbert Krebbers committed Nov 22, 2015 133 ``````Definition validity_update (x y : validityRA) : `````` Ralf Jung committed Feb 03, 2016 134 `````` (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y. `````` Robbert Krebbers committed Nov 11, 2015 135 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 136 `````` intros Hxy. apply discrete_update. `````` Robbert Krebbers committed Nov 22, 2015 137 `````` intros z (?&?&?); split_ands'; try eapply Hxy; eauto. `````` Robbert Krebbers committed Nov 11, 2015 138 139 ``````Qed. End dra.``````