agree.v 7.7 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export algebra.cmra. `````` Ralf Jung committed Feb 05, 2016 2 ``````Require Import algebra.functor. `````` Robbert Krebbers committed Nov 11, 2015 3 4 ``````Local Hint Extern 10 (_ ≤ _) => omega. `````` Robbert Krebbers committed Dec 21, 2015 5 ``````Record agree (A : Type) : Type := Agree { `````` Robbert Krebbers committed Nov 11, 2015 6 7 8 `````` agree_car :> nat → A; agree_is_valid : nat → Prop; agree_valid_0 : agree_is_valid 0; `````` Robbert Krebbers committed Nov 16, 2015 9 `````` agree_valid_S n : agree_is_valid (S n) → agree_is_valid n `````` Robbert Krebbers committed Nov 11, 2015 10 ``````}. `````` Robbert Krebbers committed Dec 21, 2015 11 12 13 ``````Arguments Agree {_} _ _ _ _. Arguments agree_car {_} _ _. Arguments agree_is_valid {_} _ _. `````` Robbert Krebbers committed Nov 11, 2015 14 15 `````` Section agree. `````` Robbert Krebbers committed Jan 14, 2016 16 ``````Context {A : cofeT}. `````` Robbert Krebbers committed Nov 11, 2015 17 `````` `````` Robbert Krebbers committed Jan 14, 2016 18 ``````Instance agree_validN : ValidN (agree A) := λ n x, `````` Robbert Krebbers committed Nov 16, 2015 19 20 21 22 `````` agree_is_valid x n ∧ ∀ n', n' ≤ n → x n' ={n'}= x n. Lemma agree_valid_le (x : agree A) n n' : agree_is_valid x n → n' ≤ n → agree_is_valid x n'. Proof. induction 2; eauto using agree_valid_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 23 ``````Instance agree_equiv : Equiv (agree A) := λ x y, `````` Robbert Krebbers committed Nov 16, 2015 24 25 `````` (∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧ (∀ n, agree_is_valid x n → x n ={n}= y n). `````` Robbert Krebbers committed Jan 14, 2016 26 ``````Instance agree_dist : Dist (agree A) := λ n x y, `````` Robbert Krebbers committed Nov 16, 2015 27 28 `````` (∀ n', n' ≤ n → agree_is_valid x n' ↔ agree_is_valid y n') ∧ (∀ n', n' ≤ n → agree_is_valid x n' → x n' ={n'}= y n'). `````` Robbert Krebbers committed Jan 14, 2016 29 ``````Program Instance agree_compl : Compl (agree A) := λ c, `````` Robbert Krebbers committed Nov 16, 2015 30 `````` {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}. `````` Robbert Krebbers committed Nov 11, 2015 31 32 33 34 ``````Next Obligation. intros; apply agree_valid_0. Qed. Next Obligation. intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto. Qed. `````` Robbert Krebbers committed Jan 14, 2016 35 ``````Definition agree_cofe_mixin : CofeMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 36 37 38 39 40 41 42 43 44 ``````Proof. split. * intros x y; split. + by intros Hxy n; split; intros; apply Hxy. + by intros Hxy; split; intros; apply Hxy with n. * split. + by split. + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy. + intros x y z Hxy Hyz; split; intros n'; intros. `````` Robbert Krebbers committed Nov 16, 2015 45 `````` - transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz. `````` Robbert Krebbers committed Nov 11, 2015 46 47 48 49 50 51 `````` - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy. * intros n x y Hxy; split; intros; apply Hxy; auto. * intros x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done]. by split; intros; apply agree_valid_0. * by intros c n; split; intros; apply (chain_cauchy c). Qed. `````` Robbert Krebbers committed Jan 14, 2016 52 ``````Canonical Structure agreeC := CofeT agree_cofe_mixin. `````` Robbert Krebbers committed Nov 11, 2015 53 `````` `````` Robbert Krebbers committed Jan 16, 2016 54 55 56 57 58 ``````Lemma agree_car_ne (x y : agree A) n : ✓{n} x → x ={n}= y → x n ={n}= y n. Proof. by intros [??] Hxy; apply Hxy. Qed. Lemma agree_cauchy (x : agree A) n i : ✓{n} x → i ≤ n → x i ={i}= x n. Proof. by intros [? Hx]; apply Hx. Qed. `````` Robbert Krebbers committed Jan 14, 2016 59 ``````Program Instance agree_op : Op (agree A) := λ x y, `````` Robbert Krebbers committed Nov 16, 2015 60 61 `````` {| agree_car := x; agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ={n}= y |}. `````` Robbert Krebbers committed Nov 11, 2015 62 ``````Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed. `````` Robbert Krebbers committed Nov 16, 2015 63 ``````Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed. `````` Robbert Krebbers committed Jan 14, 2016 64 65 ``````Instance agree_unit : Unit (agree A) := id. Instance agree_minus : Minus (agree A) := λ x y, x. `````` Robbert Krebbers committed Nov 11, 2015 66 ``````Instance: Commutative (≡) (@op (agree A) _). `````` Robbert Krebbers committed Nov 17, 2015 67 ``````Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed. `````` Robbert Krebbers committed Nov 11, 2015 68 ``````Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x. `````` Robbert Krebbers committed Nov 17, 2015 69 ``````Proof. split; naive_solver. Qed. `````` Robbert Krebbers committed Jan 16, 2016 70 71 72 73 74 75 ``````Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n). Proof. intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?]. rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le. by apply dist_le with n; try apply Hxy. Qed. `````` Robbert Krebbers committed Nov 11, 2015 76 77 78 79 80 81 82 83 84 ``````Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x). Proof. intros n x y1 y2 [Hy' Hy]; split; [|done]. split; intros (?&?&Hxy); repeat (intro || split); try apply Hy'; eauto using agree_valid_le. * etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le. * etransitivity; [apply Hxy|symmetry; apply Hy, Hy']; eauto using agree_valid_le. Qed. `````` Robbert Krebbers committed Jan 14, 2016 85 ``````Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _). `````` Robbert Krebbers committed Jan 13, 2016 86 ``````Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed. `````` Robbert Krebbers committed Nov 12, 2015 87 ``````Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _. `````` Robbert Krebbers committed Nov 17, 2015 88 89 90 91 92 93 ``````Instance: Associative (≡) (@op (agree A) _). Proof. intros x y z; split; simpl; intuition; repeat match goal with H : agree_is_valid _ _ |- _ => clear H end; by cofe_subst; rewrite !agree_idempotent. Qed. `````` Robbert Krebbers committed Nov 20, 2015 94 95 96 ``````Lemma agree_includedN (x y : agree A) n : x ≼{n} y ↔ y ={n}= x ⋅ y. Proof. split; [|by intros ?; exists y]. `````` Robbert Krebbers committed Jan 13, 2016 97 `````` by intros [z Hz]; rewrite Hz (associative _) agree_idempotent. `````` Robbert Krebbers committed Nov 20, 2015 98 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 99 ``````Definition agree_cmra_mixin : CMRAMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 100 101 102 ``````Proof. split; try (apply _ || done). * by intros n x1 x2 Hx y1 y2 Hy. `````` Robbert Krebbers committed Nov 16, 2015 103 104 105 `````` * intros x; split; [apply agree_valid_0|]. by intros n'; rewrite Nat.le_0_r; intros ->. * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?]. `````` Robbert Krebbers committed Jan 13, 2016 106 107 `````` rewrite (Hx n'); last auto. symmetry; apply dist_le with n; try apply Hx; auto. `````` Robbert Krebbers committed Nov 11, 2015 108 `````` * intros x; apply agree_idempotent. `````` Robbert Krebbers committed Nov 16, 2015 109 `````` * by intros x y n [(?&?&?) ?]. `````` Robbert Krebbers committed Nov 20, 2015 110 `````` * by intros x y n; rewrite agree_includedN. `````` Robbert Krebbers committed Nov 11, 2015 111 ``````Qed. `````` Robbert Krebbers committed Jan 16, 2016 112 113 114 115 116 117 118 ``````Lemma agree_op_inv (x1 x2 : agree A) n : ✓{n} (x1 ⋅ x2) → x1 ={n}= x2. Proof. intros Hxy; apply Hxy. Qed. Lemma agree_valid_includedN (x y : agree A) n : ✓{n} y → x ≼{n} y → x ={n}= y. Proof. move=> Hval [z Hy]; move: Hval; rewrite Hy. by move=> /agree_op_inv->; rewrite agree_idempotent. Qed. `````` Robbert Krebbers committed Jan 14, 2016 119 ``````Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A). `````` Robbert Krebbers committed Nov 11, 2015 120 ``````Proof. `````` Robbert Krebbers committed Jan 16, 2016 121 `````` intros n x y1 y2 Hval Hx; exists (x,x); simpl; split. `````` Robbert Krebbers committed Nov 11, 2015 122 `````` * by rewrite agree_idempotent. `````` Robbert Krebbers committed Jan 16, 2016 123 `````` * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent. `````` Robbert Krebbers committed Nov 11, 2015 124 ``````Qed. `````` Robbert Krebbers committed Jan 14, 2016 125 126 127 ``````Canonical Structure agreeRA : cmraT := CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin. `````` Robbert Krebbers committed Nov 16, 2015 128 129 130 131 132 ``````Program Definition to_agree (x : A) : agree A := {| agree_car n := x; agree_is_valid n := True |}. Solve Obligations with done. Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree. Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed. `````` Robbert Krebbers committed Jan 16, 2016 133 134 135 ``````Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _. Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree). Proof. by intros x y [_ Hxy]; apply Hxy. Qed. `````` Robbert Krebbers committed Jan 18, 2016 136 137 ``````Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ={n}= x. Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed. `````` Robbert Krebbers committed Nov 11, 2015 138 139 ``````End agree. `````` Robbert Krebbers committed Jan 14, 2016 140 141 142 ``````Arguments agreeC : clear implicits. Arguments agreeRA : clear implicits. `````` Robbert Krebbers committed Dec 21, 2015 143 ``````Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B := `````` Robbert Krebbers committed Dec 15, 2015 144 145 `````` {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}. Solve Obligations with auto using agree_valid_0, agree_valid_S. `````` Robbert Krebbers committed Jan 14, 2016 146 147 ``````Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. Proof. by destruct x. Qed. `````` Robbert Krebbers committed Jan 16, 2016 148 149 ``````Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) : agree_map (g ∘ f) x = agree_map g (agree_map f x). `````` Robbert Krebbers committed Jan 14, 2016 150 ``````Proof. done. Qed. `````` Robbert Krebbers committed Dec 15, 2015 151 `````` `````` Robbert Krebbers committed Nov 11, 2015 152 ``````Section agree_map. `````` Robbert Krebbers committed Jan 14, 2016 153 `````` Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}. `````` Robbert Krebbers committed Dec 15, 2015 154 `````` Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f). `````` Robbert Krebbers committed Nov 11, 2015 155 `````` Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed. `````` Robbert Krebbers committed Dec 15, 2015 156 157 158 159 160 161 `````` Global Instance agree_map_proper : Proper ((≡) ==> (≡)) (agree_map f) := ne_proper _. Lemma agree_map_ext (g : A → B) x : (∀ x, f x ≡ g x) → agree_map f x ≡ agree_map g x. Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed. Global Instance agree_map_monotone : CMRAMonotone (agree_map f). `````` Robbert Krebbers committed Nov 11, 2015 162 `````` Proof. `````` Robbert Krebbers committed Nov 16, 2015 163 `````` split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]]. `````` Robbert Krebbers committed Nov 20, 2015 164 `````` intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy. `````` Robbert Krebbers committed Jan 13, 2016 165 `````` split; last done; split; simpl; last tauto. `````` Robbert Krebbers committed Nov 20, 2015 166 167 `````` by intros (?&?&Hxy); repeat split; intros; try apply Hxy; try apply Hf; eauto using @agree_valid_le. `````` Robbert Krebbers committed Nov 11, 2015 168 169 `````` Qed. End agree_map. `````` Robbert Krebbers committed Nov 16, 2015 170 `````` `````` Robbert Krebbers committed Feb 04, 2016 171 172 173 ``````Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B := CofeMor (agree_map f : agreeC A → agreeC B). Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B). `````` Robbert Krebbers committed Nov 16, 2015 174 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 175 `````` intros f g Hfg x; split; simpl; intros; first done. `````` Robbert Krebbers committed Nov 16, 2015 176 177 `````` by apply dist_le with n; try apply Hfg. Qed. `````` Ralf Jung committed Feb 05, 2016 178 179 180 181 182 `````` Program Definition agreeF : iFunctor := {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}. Solve Obligations with done. ``````