Skip to content

GitLab

Commit 36c6dc3a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Better use of canonical structures.

parent a198e45b
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 643 additions and 519 deletions
modures/agree.v
View file @ 36c6dc3a
......@@ -12,27 +12,27 @@ Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
Section agree.
Context `{Cofe A}.
Context {A : cofeT}.
Global Instance agree_validN : ValidN (agree A) := λ n x,
Instance agree_validN : ValidN (agree A) := λ n x,
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.
Global Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Global Instance agree_equiv : Equiv (agree A) := λ x y,
Instance agree_valid : Valid (agree A) := λ x, ∀ n, ✓{n} x.
Instance agree_equiv : Equiv (agree A) := λ x y,
(∀ n, agree_is_valid x n ↔ agree_is_valid y n) ∧
(∀ n, agree_is_valid x n → x n ={n}= y n).
Global Instance agree_dist : Dist (agree A) := λ n x y,
Instance agree_dist : Dist (agree A) := λ n x y,
(∀ 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').
Global Program Instance agree_compl : Compl (agree A) := λ c,
Program Instance agree_compl : Compl (agree A) := λ c,
{| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
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.
Instance agree_cofe : Cofe (agree A).
Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
split.
* intros x y; split.
......@@ -49,14 +49,15 @@ Proof.
by split; intros; apply agree_valid_0.
* by intros c n; split; intros; apply (chain_cauchy c).
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
Global Program Instance agree_op : Op (agree A) := λ x y,
Program Instance agree_op : Op (agree A) := λ x y,
{| agree_car := x;
agree_is_valid n := agree_is_valid x n ∧ agree_is_valid y n ∧ x ={n}= y |}.
Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Global Instance agree_unit : Unit (agree A) := id.
Global Instance agree_minus : Minus (agree A) := λ x y, x.
Instance agree_unit : Unit (agree A) := id.
Instance agree_minus : Minus (agree A) := λ x y, x.
Instance: Commutative (≡) (@op (agree A) _).
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x.
......@@ -70,7 +71,7 @@ Proof.
* etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) op.
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
Instance: Associative (≡) (@op (agree A) _).
......@@ -84,7 +85,7 @@ Proof.
split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
Qed.
Global Instance agree_cmra : CMRA (agree A).
Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
* intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
......@@ -103,12 +104,15 @@ Qed.
Lemma agree_op_inv (x y1 y2 : agree A) n :
✓{n} x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2.
Proof. by intros [??] Hxy; apply Hxy. Qed.
Global Instance agree_extend : CMRAExtend (agree A).
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Proof.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
* by rewrite agree_idempotent.
* by rewrite Hx (agree_op_inv x y1 y2) // agree_idempotent.
Qed.
Canonical Structure agreeRA : cmraT :=
CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.
Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
......@@ -125,12 +129,20 @@ Proof.
Qed.
End agree.
Arguments agreeC : clear implicits.
Arguments agreeRA : clear implicits.
Program Definition agree_map {A B} (f : A → B) (x : agree A) : agree B :=
{| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
Solve Obligations with auto using agree_valid_0, agree_valid_S.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. 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. done. Qed.
Section agree_map.
Context `{Cofe A, Cofe B} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
Context {A B : cofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
Global Instance agree_map_proper :
......@@ -147,13 +159,7 @@ Section agree_map.
try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Qed.
End agree_map.
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. 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. done. Qed.
Canonical Structure agreeRA (A : cofeT) : cmraT := CMRAT (agree A).
Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A → agreeRA B).
Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
......
modures/auth.v
View file @ 36c6dc3a
......@@ -10,22 +10,24 @@ Notation "◯ x" := (Auth ExclUnit x) (at level 20).
Notation "● x" := (Auth (Excl x) ∅) (at level 20).
(* COFE *)
Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
Section cofe.
Context {A : cofeT}.
Instance auth_equiv : Equiv (auth A) := λ x y,
authoritative x ≡ authoritative y ∧ own x ≡ own y.
Instance auth_dist `{Dist A} : Dist (auth A) := λ n x y,
Instance auth_dist : Dist (auth A) := λ n x y,
authoritative x ={n}= authoritative y ∧ own x ={n}= own y.
Instance Auth_ne `{Dist A} : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
Proof. by split. Qed.
Instance authoritative_ne `{Dist A} :
Proper (dist n ==> dist n) (@authoritative A).
Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
Proof. by destruct 1. Qed.
Instance own_ne `{Dist A} : Proper (dist n ==> dist n) (@own A).
Global Instance own_ne : Proper (dist n ==> dist n) (@own A).
Proof. by destruct 1. Qed.
Instance auth_compl `{Cofe A} : Compl (auth A) := λ c,
Instance auth_compl : Compl (auth A) := λ c,
Auth (compl (chain_map authoritative c)) (compl (chain_map own c)).
Local Instance auth_cofe `{Cofe A} : Cofe (auth A).
Definition auth_cofe_mixin : CofeMixin (auth A).
Proof.
split.
* intros x y; unfold dist, auth_dist, equiv, auth_equiv.
......@@ -39,53 +41,59 @@ Proof.
* intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n).
Qed.
Instance Auth_timeless `{Dist A, Equiv A} (x : excl A) (y : A) :
Canonical Structure authC := CofeT auth_cofe_mixin.
Instance Auth_timeless (x : excl A) (y : A) :
Timeless x → Timeless y → Timeless (Auth x y).
Proof. by intros ?? [??] [??]; split; apply (timeless _). Qed.
Proof. by intros ?? [??] [??]; split; simpl in *; apply (timeless _). Qed.
End cofe.
Arguments authC : clear implicits.
(* CMRA *)
Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
Instance auth_valid `{Equiv A, Valid A, Op A} : Valid (auth A) := λ x,
Section cmra.
Context {A : cmraT}.
Global Instance auth_empty `{Empty A} : Empty (auth A) := Auth ∅ ∅.
Instance auth_valid : Valid (auth A) := λ x,
match authoritative x with
| Excl a => own x ≼ a ∧ ✓ a
| ExclUnit => ✓ (own x)
| ExclBot => False
end.
Arguments auth_valid _ _ _ _ !_ /.
Instance auth_validN `{Dist A, ValidN A, Op A} : ValidN (auth A) := λ n x,
Global Arguments auth_valid !_ /.
Instance auth_validN : ValidN (auth A) := λ n x,
match authoritative x with
| Excl a => own x ≼{n} a ∧ ✓{n} a
| ExclUnit => ✓{n} (own x)
| ExclBot => n = 0
end.
Arguments auth_validN _ _ _ _ _ !_ /.
Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
Global Arguments auth_validN _ !_ /.
Instance auth_unit : Unit (auth A) := λ x,
Auth (unit (authoritative x)) (unit (own x)).
Instance auth_op `{Op A} : Op (auth A) := λ x y,
Instance auth_op : Op (auth A) := λ x y,
Auth (authoritative x ⋅ authoritative y) (own x ⋅ own y).
Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
Instance auth_minus : Minus (auth A) := λ x y,
Auth (authoritative x ⩪ authoritative y) (own x ⩪ own y).
Lemma auth_included `{Equiv A, Op A} (x y : auth A) :
Lemma auth_included (x y : auth A) :
x ≼ y ↔ authoritative x ≼ authoritative y ∧ own x ≼ own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma auth_includedN `{Dist A, Op A} n (x y : auth A) :
Lemma auth_includedN n (x y : auth A) :
x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
Lemma authoritative_validN `{CMRA A} n (x : auth A) :
✓{n} x → ✓{n} (authoritative x).
Lemma authoritative_validN n (x : auth A) : ✓{n} x → ✓{n} (authoritative x).
Proof. by destruct x as [[]]. Qed.
Lemma own_validN `{CMRA A} n (x : auth A) : ✓{n} x → ✓{n} (own x).
Lemma own_validN n (x : auth A) : ✓{n} x → ✓{n} (own x).
Proof. destruct x as [[]]; naive_solver eauto using cmra_valid_includedN. Qed.
Instance auth_cmra `{CMRA A} : CMRA (auth A).
Definition auth_cmra_mixin : CMRAMixin (auth A).
Proof.
split.
* apply _.
* by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* intros n [x a] [y b] [Hx Ha]; simpl in *;
......@@ -103,14 +111,14 @@ Proof.
* by split; simpl; rewrite ?(ra_unit_idempotent _).
* intros n ??; rewrite! auth_includedN; intros [??].
by split; simpl; apply cmra_unit_preserving.
* assert (∀ n a b1 b2, b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
* assert (∀ n (a b1 b2 : A), b1 ⋅ b2 ≼{n} a → b1 ≼{n} a).
{ intros n a b1 b2 <-; apply cmra_included_l. }
intros n [[a1| |] b1] [[a2| |] b2];
naive_solver eauto using cmra_valid_op_l, cmra_valid_includedN.
* by intros n ??; rewrite auth_includedN;
intros [??]; split; simpl; apply cmra_op_minus.
Qed.
Instance auth_cmra_extend `{CMRA A, !CMRAExtend A} : CMRAExtend (auth A).
Definition auth_cmra_extend_mixin : CMRAExtendMixin (auth A).
Proof.
intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend_op n (authoritative x) (authoritative y1)
......@@ -119,39 +127,49 @@ Proof.
as (z2&?&?&?); auto using own_validN.
by exists (Auth (z1.1) (z2.1), Auth (z1.2) (z2.2)).
Qed.
Instance auth_ra_empty `{CMRA A, Empty A, !RAIdentity A} : RAIdentity (auth A).
Canonical Structure authRA : cmraT :=
CMRAT auth_cofe_mixin auth_cmra_mixin auth_cmra_extend_mixin.
Instance auth_ra_empty `{Empty A} : RAIdentity A → RAIdentity (auth A).
Proof.
split; [apply (ra_empty_valid (A:=A))|].
split; simpl; [apply ra_empty_valid|].
by intros x; constructor; simpl; rewrite (left_id _ _).
Qed.
Instance auth_frag_valid_timeless `{CMRA A} (x : A) :
Global Instance auth_frag_valid_timeless (x : A) :
ValidTimeless x → ValidTimeless (◯ x).
Proof. by intros ??; apply (valid_timeless x). Qed.
Instance auth_valid_timeless `{CMRA A, Empty A, !RAIdentity A} (x : A) :
Global Instance auth_valid_timeless `{Empty A, !RAIdentity A} (x : A) :
ValidTimeless x → ValidTimeless (● x).
Proof.
by intros ? [??]; split; [apply ra_empty_least|apply (valid_timeless x)].
Qed.
Lemma auth_frag_op `{CMRA A} a b : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Lemma auth_frag_op (a b : A) : ◯ (a ⋅ b) ≡ ◯ a ⋅ ◯ b.
Proof. done. Qed.
Lemma auth_includedN' n (x y : authC A) :
x ≼{n} y ↔ authoritative x ≼{n} authoritative y ∧ own x ≼{n} own y.
Proof.
split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
intros [[z1 Hz1] [z2 Hz2]]; exists (Auth z1 z2); split; auto.
Qed.
End cmra.
Arguments authRA : clear implicits.
(* Functor *)
Definition authRA (A : cmraT) : cmraT := CMRAT (auth A).
Instance auth_fmap : FMap auth := λ A B f x,
Auth (f <$> authoritative x) (f (own x)).
Instance auth_fmap_cmra_ne `{Dist A, Dist B} n :
Instance auth_fmap_cmra_ne {A B : cmraT} n :
Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
Proof.
intros f g Hf [??] [??] [??]; split; [by apply excl_fmap_cmra_ne|by apply Hf].
Qed.
Instance auth_fmap_cmra_monotone `{CMRA A, CMRA B} (f : A → B) :
Instance auth_fmap_cmra_monotone {A B : cmraT} (f : A → B) :
(∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone f →
CMRAMonotone (fmap f : auth A → auth B).
Proof.
split.
* by intros n [x a] [y b]; rewrite !auth_includedN; simpl;
intros [??]; split; apply includedN_preserving.
* intros n [[a| |] b];
* by intros n [x a] [y b]; rewrite !auth_includedN /=;
intros [??]; split; simpl; apply: includedN_preserving.
* intros n [[a| |] b]; rewrite /= /cmra_validN;
naive_solver eauto using @includedN_preserving, @validN_preserving.
Qed.
Definition authRA_map {A B : cmraT} (f : A -n> B) : authRA A -n> authRA B :=
......
modures/cmra.v
View file @ 36c6dc3a
This diff is collapsed.
modures/cofe.v
View file @ 36c6dc3a
......@@ -29,14 +29,13 @@ Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
Class Compl A `{Dist A} := compl : chain A → A.
Class Cofe A `{Equiv A, Compl A} := {
equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
dist_equivalence n :> Equivalence (dist n);
dist_S n x y : x ={S n}= y → x ={n}= y;
dist_0 x y : x ={0}= y;
conv_compl (c : chain A) n : compl c ={n}= c n
Record CofeMixin A `{Equiv A, Compl A} := {
mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
mixin_dist_equivalence n : Equivalence (dist n);
mixin_dist_S n x y : x ={S n}= y → x ={n}= y;
mixin_dist_0 x y : x ={0}= y;
mixin_conv_compl (c : chain A) n : compl c ={n}= c n
}.
Hint Extern 0 (_ ={0}= _) => apply dist_0.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
contractive n : Proper (dist n ==> dist (S n)) f.
......@@ -46,20 +45,39 @@ Structure cofeT := CofeT {
cofe_equiv : Equiv cofe_car;
cofe_dist : Dist cofe_car;
cofe_compl : Compl cofe_car;
cofe_cofe : Cofe cofe_car
cofe_mixin : CofeMixin cofe_car
}.
Arguments CofeT _ {_ _ _ _}.
Arguments CofeT {_ _ _ _} _.
Add Printing Constructor cofeT.
Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
Arguments cofe_car _ : simpl never.
Arguments cofe_equiv _ _ _ : simpl never.
Arguments cofe_dist _ _ _ _ : simpl never.
Arguments cofe_compl _ _ : simpl never.
Arguments cofe_cofe _ : simpl never.
Existing Instances cofe_equiv cofe_dist cofe_compl.
Arguments cofe_car : simpl never.
Arguments cofe_equiv : simpl never.
Arguments cofe_dist : simpl never.
Arguments cofe_compl : simpl never.
Arguments cofe_mixin : simpl never.
(** Lifting properties from the mixin *)
Section cofe_mixin.
Context {A : cofeT}.
Implicit Types x y : A.
Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y.
Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
Global Instance dist_equivalence n : Equivalence (@dist A _ n).
Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
Lemma dist_S n x y : x ={S n}= y → x ={n}= y.
Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
Lemma dist_0 x y : x ={0}= y.
Proof. apply (mixin_dist_0 _ (cofe_mixin A)). Qed.
Lemma conv_compl (c : chain A) n : compl c ={n}= c n.
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
End cofe_mixin.
Hint Extern 0 (_ ={0}= _) => apply dist_0.
(** General properties *)
Section cofe.
Context `{Cofe A}.
Context {A : cofeT}.
Implicit Types x y : A.
Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
Proof.
split.
......@@ -67,24 +85,24 @@ Section cofe.
* by intros x y; rewrite !equiv_dist.
* by intros x y z; rewrite !equiv_dist; intros; transitivity y.
Qed.
Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (dist n).
Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (@dist A _ n).
Proof.
intros x1 x2 ? y1 y2 ?; split; intros.
* by transitivity x1; [|transitivity y1].
* by transitivity x2; [|transitivity y2].
Qed.
Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (dist n).
Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n).
Proof.
by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
Qed.
Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
Proof. by apply dist_proper. Qed.
Lemma dist_le x y n n' : x ={n}= y → n' ≤ n → x ={n'}= y.
Lemma dist_le (x y : A) n n' : x ={n}= y → n' ≤ n → x ={n'}= y.
Proof. induction 2; eauto using dist_S. Qed.
Instance ne_proper `{Cofe B} (f : A → B)
Instance ne_proper {B : cofeT} (f : A → B)
`{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
Instance ne_proper_2 `{Cofe B, Cofe C} (f : A → B → C)
Instance ne_proper_2 {B C : cofeT} (f : A → B → C)
`{!∀ n, Proper (dist n ==> dist n ==> dist n) f} :
Proper ((≡) ==> (≡) ==> (≡)) f | 100.
Proof.
......@@ -95,10 +113,10 @@ Section cofe.
Proof. intros. by rewrite (conv_compl c1 n) (conv_compl c2 n). Qed.
Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
Global Instance contractive_ne `{Cofe B} (f : A → B) `{!Contractive f} n :
Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
Proper (dist n ==> dist n) f | 100.
Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
Global Instance contractive_proper `{Cofe B} (f : A → B) `{!Contractive f} :
Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
Proper ((≡) ==> (≡)) f | 100 := _.
End cofe.
......@@ -106,24 +124,24 @@ End cofe.
Program Definition chain_map `{Dist A, Dist B} (f : A → B)
`{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
{| chain_car n := f (c n) |}.
Next Obligation. by intros A ? B ? f Hf c n i ?; apply Hf, chain_cauchy. Qed.
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless `{Dist A, Equiv A} (x : A) := timeless y : x ={1}= y → x ≡ y.
Arguments timeless {_ _ _} _ {_} _ _.
Class Timeless {A : cofeT} (x : A) := timeless y : x ={1}= y → x ≡ y.
Arguments timeless {_} _ {_} _ _.
(** Fixpoint *)
Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A)
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
Next Obligation.
intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
intros A ? f ? n; induction n as [|n IH]; intros i ?; first done.
destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Qed.
Program Definition fixpoint `{Cofe A, Inhabited A} (f : A → A)
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
Section fixpoint.
Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive f}.
Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
apply equiv_dist; intros n; unfold fixpoint.
......@@ -153,46 +171,51 @@ Arguments CofeMor {_ _} _ {_}.
Add Printing Constructor cofeMor.
Existing Instance cofe_mor_ne.
Instance cofe_mor_proper `(f : cofeMor A B) : Proper ((≡) ==> (≡)) f := _.
Instance cofe_mor_equiv {A B : cofeT} : Equiv (cofeMor A B) := λ f g,
∀ x, f x ≡ g x.
Instance cofe_mor_dist (A B : cofeT) : Dist (cofeMor A B) := λ n f g,
∀ x, f x ={n}= g x.
Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
{| chain_car n := c n x |}.
Next Obligation. intros A B c x n i ?. by apply (chain_cauchy c). Qed.
Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation.
intros A B c n x y Hxy.
rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy.
apply (chain_cauchy c); lia.
Qed.
Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
Proof.
split.
* intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|].
intros HXY k; apply equiv_dist; intros n; apply HXY.
* intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; transitivity (g x).
* by intros n f g ? x; apply dist_S.
* by intros f g x.
* intros c n x; simpl.
rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
Qed.
Instance cofe_mor_car_ne A B n :
Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
Instance cofe_mor_car_proper A B :
Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _.
Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
Proof. done. Qed.
Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
Section cofe_mor.
Context {A B : cofeT}.
Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f.
Proof. apply ne_proper, cofe_mor_ne. Qed.
Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, ∀ x, f x ≡ g x.
Instance cofe_mor_dist : Dist (cofeMor A B) := λ n f g, ∀ x, f x ={n}= g x.
Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
{| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation.
intros c n x y Hx.
rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n)