Skip to content
Snippets Groups Projects
Commit 62e8a98b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Shorten the agreement proofs and bring the construction closer to the one in the paper.

parent b73112e3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/algebra/agree.v
+ 120
− 318
View file @ 62e8a98b
......@@ -9,7 +9,6 @@ Local Arguments pcore _ _ !_ /.
(** Define an agreement construction such that Agree A is discrete when A is discrete.
Notice that this construction is NOT complete. The fullowing is due to Aleš:
Proposition: Ag(T) is not necessarily complete.
Proof.
Let T be the set of binary streams (infinite sequences) with the usual
......@@ -28,314 +27,117 @@ Proof.
*)
Record agree (A : Type) : Type := Agree {
agree_car : A;
agree_with : list A;
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Arguments Agree {_} _ _.
Arguments agree_car {_} _.
Arguments agree_with {_} _.
(* Some theory about set-inclusion on lists and lists of which all elements are equal.
TODO: Move this elsewhere. *)
Definition list_setincl `(R : relation A) (al bl : list A) :=
∀ a, a ∈ al → ∃ b, b ∈ bl ∧ R a b.
Definition list_setequiv `(R : relation A) (al bl : list A) :=
list_setincl R al bl ∧ list_setincl R bl al.
(* list_agrees is carefully written such that, when applied to a
singleton, it is convertible to True. This makes working with
agreement much more pleasant. *)
Definition list_agrees `(R : relation A) (al : list A) :=
match al with
| [] => True
| [a] => True
| a :: al => ∀ b, b ∈ al → R a b
end.
Arguments agree_not_nil {_} _.
Local Coercion agree_car : agree >-> list.
Lemma list_agrees_alt `(R : relation A) `{Equivalence _ R} al :
list_agrees R al ↔ (∀ a b, a ∈ al → b ∈ al → R a b).
Lemma elem_of_agree {A} (x : agree A) : ∃ a, a ∈ agree_car x.
Proof. destruct x as [[|a ?] ?]; set_solver+. Qed.
Lemma agree_eq {A} (x y : agree A) : agree_car x = agree_car y → x = y.
Proof.
destruct al as [|a [|b al]].
- split; last done. intros _ ? ? []%elem_of_nil.
- split; last done. intros _ ? ? ->%elem_of_list_singleton ->%elem_of_list_singleton. done.
- simpl. split.
+ intros Hl a' b' [->|Ha']%elem_of_cons.
* intros [->|Hb']%elem_of_cons; first done. auto.
* intros [->|Hb']%elem_of_cons; first by (symmetry; auto).
trans a; last by auto. symmetry. auto.
+ intros Hl b' Hb'. apply Hl; set_solver.
destruct x as [a ?], y as [b ?]; simpl.
intros ->; f_equal. apply (proof_irrel _).
Qed.
Section list_theory.
Context `(R: relation A) `{Equivalence A R}.
Collection Hyps := Type H.
Local Set Default Proof Using "Hyps".
Global Instance: PreOrder (list_setincl R).
Proof.
split.
- intros al a Ha. set_solver.
- intros al bl cl Hab Hbc a Ha. destruct (Hab _ Ha) as (b & Hb & Rab).
destruct (Hbc _ Hb) as (c & Hc & Rbc). exists c. split; first done.
by trans b.
Qed.
Global Instance: Equivalence (list_setequiv R).
Proof.
split.
- by split.
- intros ?? [??]. split; auto.
- intros ??? [??] [??]. split; etrans; done.
Qed.
Global Instance list_setincl_subrel `(R' : relation A) :
subrelation R R' → subrelation (list_setincl R) (list_setincl R').
Proof using.
intros HRR' al bl Hab. intros a Ha. destruct (Hab _ Ha) as (b & Hb & HR).
exists b. split; first done. exact: HRR'.
Qed.
Global Instance list_setequiv_subrel `(R' : relation A) :
subrelation R R' → subrelation (list_setequiv R) (list_setequiv R').
Proof using. intros HRR' ?? [??]. split; exact: list_setincl_subrel. Qed.
Global Instance list_setincl_perm : subrelation (≡ₚ) (list_setincl R).
Proof.
intros al bl Hab a Ha. exists a. split; last done.
by rewrite -Hab.
Qed.
Global Instance list_setincl_app l :
Proper (list_setincl R ==> list_setincl R) (app l).
Proof.
intros al bl Hab a [Ha|Ha]%elem_of_app.
- exists a. split; last done. apply elem_of_app. by left.
- destruct (Hab _ Ha) as (b & Hb & HR). exists b. split; last done.
apply elem_of_app. by right.
Qed.
Global Instance list_setequiv_app l :
Proper (list_setequiv R ==> list_setequiv R) (app l).
Proof. intros al bl [??]. split; apply list_setincl_app; done. Qed.
Global Instance: subrelation (≡ₚ) (flip (list_setincl R)).
Proof. intros ???. apply list_setincl_perm. done. Qed.
Global Instance list_agrees_setincl :
Proper (flip (list_setincl R) ==> impl) (list_agrees R).
Proof.
move=> al bl /= Hab /list_agrees_alt Hal. apply (list_agrees_alt _) => a b Ha Hb.
destruct (Hab _ Ha) as (a' & Ha' & HRa).
destruct (Hab _ Hb) as (b' & Hb' & HRb).
trans a'; first done. etrans; last done.
eapply Hal; done.
Qed.
Global Instance list_agrees_setequiv :
Proper (list_setequiv R ==> iff) (list_agrees R).
Proof.
intros ?? [??]. split; by apply: list_agrees_setincl.
Qed.
Lemma list_setincl_contains al bl :
(∀ x, x ∈ al → x ∈ bl) → list_setincl R al bl.
Proof. intros Hin a Ha. exists a. split; last done. naive_solver. Qed.
Lemma list_setequiv_equiv al bl :
(∀ x, x ∈ al ↔ x ∈ bl) → list_setequiv R al bl.
Proof.
intros Hin. split; apply list_setincl_contains; naive_solver.
Qed.
Lemma list_agrees_contains al bl :
(∀ x, x ∈ bl → x ∈ al) →
list_agrees R al → list_agrees R bl.
Proof. intros ?. by eapply (list_agrees_setincl _),list_setincl_contains. Qed.
Lemma list_agrees_equiv al bl :
(∀ x, x ∈ bl ↔ x ∈ al) →
list_agrees R al ↔ list_agrees R bl.
Proof. intros ?. by eapply (list_agrees_setequiv _), list_setequiv_equiv. Qed.
Lemma list_setincl_singleton a b :
R a b → list_setincl R [a] [b].
Proof.
intros HR c ->%elem_of_list_singleton. exists b. split; last done.
apply elem_of_list_singleton. done.
Qed.
Lemma list_setincl_singleton_rev a b :
list_setincl R [a] [b] → R a b.
Proof using.
intros Hl. destruct (Hl a) as (? & ->%elem_of_list_singleton & HR); last done.
by apply elem_of_list_singleton.
Qed.
Lemma list_setequiv_singleton a b :
R a b → list_setequiv R [a] [b].
Proof. intros ?. split; by apply list_setincl_singleton. Qed.
Lemma list_agrees_iff_setincl al a :
a ∈ al → list_agrees R al ↔ list_setincl R al [a].
Proof.
intros Hin. split.
- move=>/list_agrees_alt Hl b Hb. exists a. split; first set_solver+. exact: Hl.
- intros Hl. apply (list_agrees_alt _)=> b c Hb Hc.
destruct (Hl _ Hb) as (? & ->%elem_of_list_singleton & ?).
destruct (Hl _ Hc) as (? & ->%elem_of_list_singleton & ?).
by trans a.
Qed.
Lemma list_setincl_singleton_in al a :
a ∈ al → list_setincl R [a] al.
Proof.
intros Hin b ->%elem_of_list_singleton. exists a. split; done.
Qed.
Global Instance list_setincl_ext : subrelation (Forall2 R) (list_setincl R).
Proof.
move=>al bl. induction 1.
- intros ? []%elem_of_nil.
- intros a [->|Ha]%elem_of_cons.
+ eexists. split; first constructor. done.
+ destruct (IHForall2 _ Ha) as (b & ? & ?).
exists b. split; first by constructor. done.
Qed.
Global Instance list_setequiv_ext : subrelation (Forall2 R) (list_setequiv R).
Proof.
move=>al bl ?. split; apply list_setincl_ext; done.
Qed.
Lemma list_agrees_subrel `(R' : relation A) `{Equivalence _ R'} :
subrelation R R' → ∀ l, list_agrees R l → list_agrees R' l.
Proof. move=> HR l /list_agrees_alt Hl. apply (list_agrees_alt _)=> a b Ha Hb. by apply HR, Hl. Qed.
Section fmap.
Context `(R' : relation B) (f : A → B) {Hf: Proper (R ==> R') f}.
Collection Hyps := Type Hf.
Local Set Default Proof Using "Hyps".
Global Instance list_setincl_fmap :
Proper (list_setincl R ==> list_setincl R') (fmap f).
Proof using Hf.
intros al bl Hab a' (a & -> & Ha)%elem_of_list_fmap.
destruct (Hab _ Ha) as (b & Hb & HR). exists (f b).
split; first eapply elem_of_list_fmap; eauto.
Qed.
Global Instance list_setequiv_fmap :
Proper (list_setequiv R ==> list_setequiv R') (fmap f).
Proof using Hf. intros ?? [??]. split; apply list_setincl_fmap; done. Qed.
Lemma list_agrees_fmap `{Equivalence _ R'} al :
list_agrees R al → list_agrees R' (f <$> al).
Proof using Type*.
move=> /list_agrees_alt Hl. apply (list_agrees_alt R') => a' b'.
intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
apply Hf. exact: Hl.
Qed.
End fmap.
End list_theory.
Section agree.
Local Set Default Proof Using "Type".
Context {A : ofeT}.
Implicit Types a b : A.
Implicit Types x y : agree A.
Definition agree_list (x : agree A) := agree_car x :: agree_with x.
Instance agree_validN : ValidN (agree A) := λ n x,
list_agrees (dist n) (agree_list x).
Instance agree_valid : Valid (agree A) := λ x,
list_agrees (equiv) (agree_list x).
(* OFE *)
Instance agree_dist : Dist (agree A) := λ n x y,
list_setequiv (dist n) (agree_list x) (agree_list y).
Instance agree_equiv : Equiv (agree A) := λ x y,
∀ n, list_setequiv (dist n) (agree_list x) (agree_list y).
Definition agree_dist_incl n (x y : agree A) :=
list_setincl (dist n) (agree_list x) (agree_list y).
(∀ a, a ∈ agree_car x → ∃ b, b ∈ agree_car y ∧ a ≡{n}≡ b) ∧
(∀ b, b ∈ agree_car y → ∃ a, a ∈ agree_car x ∧ a ≡{n}≡ b).
Instance agree_equiv : Equiv (agree A) := λ x y, ∀ n, x ≡{n}≡ y.
Definition agree_ofe_mixin : OfeMixin (agree A).
Proof.
split.
- intros x y; split; intros Hxy; done.
- split; rewrite /dist /agree_dist; intros ? *.
+ reflexivity.
+ by symmetry.
+ intros. etrans; eassumption.
- intros ???. apply list_setequiv_subrel=>??. apply dist_S.
- done.
- intros n; split; rewrite /dist /agree_dist.
+ intros x; split; eauto.
+ intros x y [??]. naive_solver eauto.
+ intros x y z [H1 H1'] [H2 H2']; split.
* intros a ?. destruct (H1 a) as (b&?&?); auto.
destruct (H2 b) as (c&?&?); eauto. by exists c; split; last etrans.
* intros a ?. destruct (H2' a) as (b&?&?); auto.
destruct (H1' b) as (c&?&?); eauto. by exists c; split; last etrans.
- intros n x y [??]; split; naive_solver eauto using dist_S.
Qed.
Canonical Structure agreeC := OfeT (agree A) agree_ofe_mixin.
(* CMRA *)
(* agree_validN is carefully written such that, when applied to a singleton, it
is convertible to True. This makes working with agreement much more pleasant. *)
Instance agree_validN : ValidN (agree A) := λ n x,
match agree_car x with
| [a] => True
| _ => ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b
end.
Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := agree_car x;
agree_with := agree_with x ++ agree_car y :: agree_with y |}.
Agree (agree_car x ++ agree_car y) _.
Next Obligation. by intros [[|??]] y. Qed.
Instance agree_pcore : PCore (agree A) := Some.
Instance: Comm (≡) (@op (agree A) _).
Proof. intros x y n. apply: list_setequiv_equiv. set_solver. Qed.
Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
Proof. intros n. apply: list_setequiv_equiv. set_solver. Qed.
Lemma agree_validN_def n x :
✓{n} x ↔ ∀ a b, a ∈ agree_car x → b ∈ agree_car x → a ≡{n}≡ b.
Proof.
rewrite /validN /agree_validN. destruct (agree_car _) as [|? [|??]]; auto.
setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Instance: ∀ n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
Instance agree_comm : Comm (≡) (@op (agree A) _).
Proof. intros x y n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
Instance agree_assoc : Assoc (≡) (@op (agree A) _).
Proof.
intros n x y. rewrite /dist /validN /agree_dist /agree_validN.
by intros ->.
intros x y z n; split=> a /=; repeat setoid_rewrite elem_of_app; naive_solver.
Qed.
Instance: ∀ n : nat, Proper (equiv ==> iff) (@validN (agree A) _ n).
Lemma agree_idemp (x : agree A) : x ⋅ x ≡ x.
Proof. intros n; split=> a /=; setoid_rewrite elem_of_app; naive_solver. Qed.
Instance agree_validN_ne n : Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
intros n ???. assert (x ≡{n}≡ y) as Hxy by by apply equiv_dist.
split; rewrite Hxy; done.
intros x y [H H']; rewrite /impl !agree_validN_def; intros Hv a b Ha Hb.
destruct (H' a) as (a'&?&<-); auto. destruct (H' b) as (b'&?&<-); auto.
Qed.
Instance agree_validN_proper n : Proper (equiv ==> iff) (@validN (agree A) _ n).
Proof. move=> x y /equiv_dist H. by split; rewrite (H n). Qed.
Instance: ∀ x : agree A, NonExpansive (op x).
Instance agree_op_ne' x : NonExpansive (op x).
Proof.
intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=.
rewrite !app_comm_cons. apply: list_setequiv_app.
intros n y1 y2 [H H']; split=> a /=; setoid_rewrite elem_of_app; naive_solver.
Qed.
Instance: NonExpansive2 (@op (agree A) _).
Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Instance: Assoc (≡) (@op (agree A) _).
Proof. intros x y z n. apply: list_setequiv_equiv. set_solver. Qed.
Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Lemma agree_included (x y : agree A) : x ≼ y ↔ y ≡ x ⋅ y.
Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz assoc agree_idemp.
Qed.
Lemma agree_op_inv_inclN n x1 x2 : ✓{n} (x1 ⋅ x2) → agree_dist_incl n x1 x2.
Proof.
rewrite /validN /= => /list_agrees_alt Hv a /elem_of_cons Ha. exists (agree_car x2).
split; first by constructor. eapply Hv.
- simpl. destruct Ha as [->|Ha]; set_solver.
- simpl. set_solver+.
Qed.
Lemma agree_op_invN n (x1 x2 : agree A) : ✓{n} (x1 ⋅ x2) → x1 ≡{n}≡ x2.
Proof.
intros Hxy. split; apply agree_op_inv_inclN; first done. by rewrite comm.
Qed.
Lemma agree_valid_includedN n (x y : agree A) : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
Proof.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_invN->; rewrite agree_idemp.
rewrite agree_validN_def /=. setoid_rewrite elem_of_app=> Hv; split=> a Ha.
- destruct (elem_of_agree x2); naive_solver.
- destruct (elem_of_agree x1); naive_solver.
Qed.
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
apply cmra_total_mixin; try apply _ || by eauto.
- move=>x. split.
+ move=>/list_agrees_alt Hx n. apply (list_agrees_alt _)=> a b Ha Hb.
apply equiv_dist, Hx; done.
+ intros Hx. apply (list_agrees_alt _)=> a b Ha Hb.
apply equiv_dist=>n. eapply (list_agrees_alt _); first (by apply Hx); done.
- intros n x. apply (list_agrees_subrel _ _)=>??. apply dist_S.
- intros n x; rewrite !agree_validN_def; eauto using dist_S.
- intros x. apply agree_idemp.
- intros ??? Hl. apply: list_agrees_contains Hl. set_solver.
- intros n x y; rewrite !agree_validN_def /=.
setoid_rewrite elem_of_app; naive_solver.
- intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_invN->; rewrite agree_idemp.
......@@ -350,55 +152,56 @@ Proof. by constructor. Qed.
Global Instance agree_discrete : Discrete A → CMRADiscrete agreeR.
Proof.
intros HD. split.
- intros x y Hxy n. eapply list_setequiv_subrel; last exact Hxy. clear -HD.
intros x y ?. apply equiv_dist, HD. done.
- rewrite /valid /cmra_valid /agree_valid /validN /cmra_validN /agree_validN /=.
move=> x. apply (list_agrees_subrel _ _). clear -HD.
intros x y. apply HD.
- intros x y [H H'] n; split=> a; setoid_rewrite <-(timeless_iff_0 _ _); auto.
- intros x; rewrite agree_validN_def=> Hv n. apply agree_validN_def=> a b ??.
apply timeless_iff_0; auto.
Qed.
Definition to_agree (x : A) : agree A :=
{| agree_car := x; agree_with := [] |}.
Program Definition to_agree (a : A) : agree A :=
{| agree_car := [a]; agree_not_nil := eq_refl |}.
Global Instance to_agree_ne : NonExpansive to_agree.
Proof.
intros x1 x2 Hx; rewrite /= /dist /agree_dist /=.
exact: list_setequiv_singleton.
intros n a1 a2 Hx; split=> b /=;
setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
Global Instance to_agree_injN n : Inj (dist n) (dist n) (to_agree).
Proof. intros a b [Hxy%list_setincl_singleton_rev _]. done. Qed.
Proof.
move=> a b [_] /=. setoid_rewrite elem_of_list_singleton. naive_solver.
Qed.
Global Instance to_agree_inj : Inj (≡) (≡) (to_agree).
Proof. intros a b ?. apply equiv_dist=>n. by apply to_agree_injN, equiv_dist. Qed.
Lemma to_agree_uninjN n (x : agree A) : ✓{n} x → ∃ y : A, to_agree y ≡{n}≡ x.
Lemma to_agree_uninjN n (x : agree A) : ✓{n} x → ∃ a : A, to_agree a ≡{n}≡ x.
Proof.
intros Hl. exists (agree_car x). rewrite /dist /agree_dist /=. split.
- apply: list_setincl_singleton_in. set_solver+.
- apply (list_agrees_iff_setincl _); first set_solver+. done.
rewrite agree_validN_def=> Hv.
destruct (elem_of_agree x) as [a ?].
exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Lemma to_agree_uninj (x : agree A) : ✓ x → ∃ y : A, to_agree y ≡ x.
Proof.
intros Hl. exists (agree_car x). rewrite /dist /agree_dist /=. split.
- apply: list_setincl_singleton_in. set_solver+.
- apply (list_agrees_iff_setincl _); first set_solver+.
eapply list_agrees_subrel; last exact: Hl; [apply _..|].
intros ???. by apply equiv_dist.
rewrite /valid /agree_valid; setoid_rewrite agree_validN_def.
destruct (elem_of_agree x) as [a ?].
exists a; split=> b /=; setoid_rewrite elem_of_list_singleton; naive_solver.
Qed.
Lemma to_agree_included (a b : A) : to_agree a ≼ to_agree b ↔ a ≡ b.
Lemma agree_valid_includedN n x y : ✓{n} y → x ≼{n} y → x ≡{n}≡ y.
Proof.
split.
- intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl].
(* TODO: This could become a generic lemma about list_setincl. *)
destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
done.
- by intros ->.
move=> Hval [z Hy]; move: Hval; rewrite Hy.
by move=> /agree_op_invN->; rewrite agree_idemp.
Qed.
Lemma to_agree_included a b : to_agree a ≼ to_agree b ↔ a ≡ b.
Proof.
split; last by intros ->.
intros (x & Heq). apply equiv_dist=>n. destruct (Heq n) as [_ Hincl].
by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
Qed.
Global Instance agree_cancelable (x : agree A) : Cancelable x.
Global Instance agree_cancelable x : Cancelable x.
Proof.
intros n y z Hv Heq.
destruct (to_agree_uninjN n x) as [x' EQx]; first by eapply cmra_validN_op_l.
......@@ -412,14 +215,13 @@ Proof.
by rewrite -EQy -EQz -Hx'y' -Hx'z'.
Qed.
Lemma agree_op_inv (x1 x2 : agree A) : ✓ (x1 ⋅ x2) → x1 ≡ x2.
Lemma agree_op_inv x y : ✓ (x ⋅ y) → x ≡ y.
Proof.
intros ?. apply equiv_dist=>n. by apply agree_op_invN, cmra_valid_validN.
Qed.
Lemma agree_op_inv' (a1 a2 : A) : ✓ (to_agree a1 ⋅ to_agree a2) → a1 ≡ a2.
Lemma agree_op_inv' a b : ✓ (to_agree a ⋅ to_agree b) → a ≡ b.
Proof. by intros ?%agree_op_inv%(inj _). Qed.
Lemma agree_op_invL' `{!LeibnizEquiv A} (a1 a2 : A) :
✓ (to_agree a1 ⋅ to_agree a2) → a1 = a2.
Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b) → a = b.
Proof. by intros ?%agree_op_inv'%leibniz_equiv. Qed.
(** Internalized properties *)
......@@ -438,41 +240,42 @@ Arguments agreeC : clear implicits.
Arguments agreeR : clear implicits.
Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
{| agree_car := f (agree_car x); agree_with := f <$> (agree_with x) |}.
{| agree_car := f <$> agree_car x |}.
Next Obligation. by intros A B f [[|??] ?]. Qed.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. rewrite /agree_map /= list_fmap_id. by destruct x. Qed.
Proof. apply agree_eq. by rewrite /= list_fmap_id. Qed.
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).
Proof. rewrite /agree_map /= list_fmap_compose. done. Qed.
Proof. apply agree_eq. by rewrite /= list_fmap_compose. Qed.
Section agree_map.
Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
Collection Hyps := Type Hf.
Instance agree_map_ne : NonExpansive (agree_map f).
Proof using Hyps.
intros n x y Hxy.
change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
eapply list_setequiv_fmap; last exact Hxy. apply _.
Proof.
intros n x y [H H']; split=> b /=; setoid_rewrite elem_of_list_fmap.
- intros (a&->&?). destruct (H a) as (a'&?&?); auto. naive_solver.
- intros (a&->&?). destruct (H' a) as (a'&?&?); auto. naive_solver.
Qed.
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.
intros Hfg n. apply: list_setequiv_ext.
change (f <$> (agree_list x) ≡{n}≡ g <$> (agree_list x)).
apply list_fmap_ext_ne=>y. by apply equiv_dist.
(∀ a, f a ≡ g a) → agree_map f x ≡ agree_map g x.
Proof using Hf.
intros Hfg n; split=> b /=; setoid_rewrite elem_of_list_fmap.
- intros (a&->&?). exists (g a). rewrite Hfg; eauto.
- intros (a&->&?). exists (f a). rewrite -Hfg; eauto.
Qed.
Global Instance agree_map_morphism : CMRAMorphism (agree_map f).
Proof using Hyps.
Proof using Hf.
split; first apply _.
- intros n x. rewrite /cmra_validN /validN /= /agree_validN /= => ?.
change (list_agrees (dist n) (f <$> agree_list x)).
eapply (list_agrees_fmap _ _ _); done.
- intros n x. rewrite !agree_validN_def=> Hv b b' /=.
intros (a&->&?)%elem_of_list_fmap (a'&->&?)%elem_of_list_fmap.
apply Hf; eauto.
- done.
- intros x y n. apply: list_setequiv_equiv=>b.
rewrite /agree_list /= !fmap_app. set_solver+.
- intros x y n; split=> b /=;
rewrite !fmap_app; setoid_rewrite elem_of_app; eauto.
Qed.
End agree_map.
......@@ -480,9 +283,8 @@ 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 : NonExpansive (@agreeC_map A B).
Proof.
intros n f g Hfg x. apply: list_setequiv_ext.
change (f <$> (agree_list x) ≡{n}≡ g <$> (agree_list x)).
apply list_fmap_ext_ne. done.
intros n f g Hfg x; split=> b /=;
setoid_rewrite elem_of_list_fmap; naive_solver.
Qed.
Program Definition agreeRF (F : cFunctor) : rFunctor := {|
......@@ -494,11 +296,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A B x; simpl. rewrite -{2}(agree_map_id x).
apply agree_map_ext=>y. by rewrite cFunctor_id.
apply (agree_map_ext _)=>y. by rewrite cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -agree_map_compose.
apply agree_map_ext=>y; apply cFunctor_compose.
apply (agree_map_ext _)=>y; apply cFunctor_compose.
Qed.
Instance agreeRF_contractive F :
......
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