Commit b13debed authored by Robbert Krebbers's avatar Robbert Krebbers

Cleanup agree and prove some additional properties.

parent 69407372
...@@ -51,6 +51,11 @@ Proof. ...@@ -51,6 +51,11 @@ Proof.
Qed. Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin. Canonical Structure agreeC := CofeT agree_cofe_mixin.
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.
Program Instance agree_op : Op (agree A) := λ x y, Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x; {| agree_car := x;
agree_is_valid n := agree_is_valid x n agree_is_valid y n x ={n}= y |}. agree_is_valid n := agree_is_valid x n agree_is_valid y n x ={n}= y |}.
...@@ -62,6 +67,12 @@ Instance: Commutative (≡) (@op (agree A) _). ...@@ -62,6 +67,12 @@ Instance: Commutative (≡) (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed. Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Definition agree_idempotent (x : agree A) : x x x. Definition agree_idempotent (x : agree A) : x x x.
Proof. split; naive_solver. Qed. Proof. split; naive_solver. Qed.
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.
Instance: x : agree A, Proper (dist n ==> dist n) (op x). Instance: x : agree A, Proper (dist n ==> dist n) (op x).
Proof. Proof.
intros n x y1 y2 [Hy' Hy]; split; [|done]. intros n x y1 y2 [Hy' Hy]; split; [|done].
...@@ -88,9 +99,6 @@ Qed. ...@@ -88,9 +99,6 @@ Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A). Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof. Proof.
split; try (apply _ || done). split; try (apply _ || done).
* 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.
* by intros n x1 x2 Hx y1 y2 Hy. * by intros n x1 x2 Hx y1 y2 Hy.
* intros x; split; [apply agree_valid_0|]. * intros x; split; [apply agree_valid_0|].
by intros n'; rewrite Nat.le_0_r; intros ->. by intros n'; rewrite Nat.le_0_r; intros ->.
...@@ -101,14 +109,18 @@ Proof. ...@@ -101,14 +109,18 @@ Proof.
* by intros x y n [(?&?&?) ?]. * by intros x y n [(?&?&?) ?].
* by intros x y n; rewrite agree_includedN. * by intros x y n; rewrite agree_includedN.
Qed. Qed.
Lemma agree_op_inv (x y1 y2 : agree A) n : Lemma agree_op_inv (x1 x2 : agree A) n : {n} (x1 x2) x1 ={n}= x2.
{n} x x ={n}= y1 y2 y1 ={n}= y2. Proof. intros Hxy; apply Hxy. Qed.
Proof. by 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.
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A). Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof. Proof.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split. intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent. * by rewrite agree_idempotent.
* by rewrite Hx (agree_op_inv x y1 y2) // agree_idempotent. * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idempotent.
Qed. Qed.
Canonical Structure agreeRA : cmraT := Canonical Structure agreeRA : cmraT :=
CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin. CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
...@@ -118,15 +130,9 @@ Program Definition to_agree (x : A) : agree A := ...@@ -118,15 +130,9 @@ Program Definition to_agree (x : A) : agree A :=
Solve Obligations with done. Solve Obligations with done.
Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree. 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. Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
Lemma agree_car_ne (x y : agree A) n : {n} x x ={n}= y x n ={n}= y n. Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
Proof. by intros [??] Hxy; apply Hxy. Qed. Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
Lemma agree_cauchy (x : agree A) n i : n i {i} x x n ={n}= x i. Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
Proof. by intros ? [? Hx]; apply Hx. Qed.
Lemma agree_to_agree_inj (x y : agree A) a n :
{n} x x ={n}= to_agree a y x n ={n}= a.
Proof.
by intros; transitivity ((to_agree a y) n); first apply agree_car_ne.
Qed.
End agree. End agree.
Arguments agreeC : clear implicits. Arguments agreeC : clear implicits.
...@@ -137,8 +143,8 @@ Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B := ...@@ -137,8 +143,8 @@ Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
Solve Obligations with auto using agree_valid_0, agree_valid_S. Solve Obligations with auto using agree_valid_0, agree_valid_S.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x. Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed. Proof. by destruct x. Qed.
Lemma agree_map_compose {A B C} (f : A B) (g : B C) Lemma agree_map_compose {A B C} (f : A B) (g : B C) (x : agree A) :
(x : agree A) : agree_map (g f) x = agree_map g (agree_map f x). agree_map (g f) x = agree_map g (agree_map f x).
Proof. done. Qed. Proof. done. Qed.
Section agree_map. Section agree_map.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment