Commit 9c8eb238 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 6af9f587 d90c495b
......@@ -5,10 +5,9 @@ Local Hint Extern 10 (_ ≤ _) => omega.
Record agree (A : Type) : Type := Agree {
agree_car :> nat A;
agree_is_valid : nat Prop;
agree_valid_0 : agree_is_valid 0;
agree_valid_S n : agree_is_valid (S n) agree_is_valid n
}.
Arguments Agree {_} _ _ _ _.
Arguments Agree {_} _ _ _.
Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
......@@ -27,10 +26,9 @@ 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').
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.
{| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}.
Next Obligation.
intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto.
Qed.
Definition agree_cofe_mixin : CofeMixin (agree A).
Proof.
......@@ -45,9 +43,8 @@ Proof.
- transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
- 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).
* intros c n; apply and_wlog_r; intros;
symmetry; apply (chain_cauchy c); naive_solver.
Qed.
Canonical Structure agreeC := CofeT agree_cofe_mixin.
......@@ -59,7 +56,6 @@ Proof. by intros [? Hx]; apply Hx. Qed.
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.
Instance agree_unit : Unit (agree A) := id.
Instance agree_minus : Minus (agree A) := λ x y, x.
......@@ -100,8 +96,6 @@ Definition agree_cmra_mixin : CMRAMixin (agree A).
Proof.
split; try (apply _ || done).
* by intros n x1 x2 Hx y1 y2 Hy.
* 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' ?].
rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
......@@ -142,7 +136,7 @@ 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.
Solve Obligations with auto using 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) :
......@@ -179,4 +173,3 @@ Qed.
Program Definition agreeF : iFunctor :=
{| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
Solve Obligations with done.
......@@ -46,7 +46,6 @@ Proof.
+ by intros ?? [??]; split; symmetry.
+ intros ??? [??] [??]; split; etransitivity; eauto.
* by intros ? [??] [??] [??]; split; apply dist_S.
* by split.
* intros c n; split. apply (conv_compl (chain_map authoritative c) n).
apply (conv_compl (chain_map own c) n).
Qed.
......@@ -71,7 +70,7 @@ 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
| ExclBot => False
end.
Global Arguments auth_validN _ !_ /.
Instance auth_unit : Unit (auth A) := λ x,
......@@ -103,10 +102,9 @@ Proof.
* 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 *;
destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
destruct Hx; intros ?; cofe_subst; auto.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
* by intros [[] ?]; simpl.
* intros n [[] ?] ?; naive_solver eauto using cmra_includedN_S, cmra_validN_S.
* by split; simpl; rewrite associative.
* by split; simpl; rewrite commutative.
......@@ -150,7 +148,7 @@ Lemma auth_both_op a b : Auth (Excl a) b ≡ ● a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
Lemma auth_update a a' b b' :
( n af, {S n} a a {S n} a' af b {S n} b' af {S n} b)
( n af, {n} a a {n} a' af b {n} b' af {n} b)
a a' ~~> b b'.
Proof.
move=> Hab [[?| |] bf1] n // =>-[[bf2 Ha] ?]; do 2 red; simpl in *.
......@@ -216,4 +214,3 @@ Next Obligation.
intros Σ A B C f g x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply ifunctor_map_compose.
Qed.
......@@ -40,7 +40,6 @@ Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
mixin_cmra_validN_ne n : Proper (dist n ==> impl) ({n});
mixin_cmra_minus_ne n : Proper (dist n ==> dist n ==> dist n) minus;
(* valid *)
mixin_cmra_validN_0 x : {0} x;
mixin_cmra_validN_S n x : {S n} x {n} x;
(* monoid *)
mixin_cmra_associative : Associative () ();
......@@ -99,8 +98,6 @@ Section cmra_mixin.
Global Instance cmra_minus_ne n :
Proper (dist n ==> dist n ==> dist n) (@minus A _).
Proof. apply (mixin_cmra_minus_ne _ (cmra_mixin A)). Qed.
Lemma cmra_validN_0 x : {0} x.
Proof. apply (mixin_cmra_validN_0 _ (cmra_mixin A)). Qed.
Lemma cmra_validN_S n x : {S n} x {n} x.
Proof. apply (mixin_cmra_validN_S _ (cmra_mixin A)). Qed.
Global Instance cmra_associative : Associative () (@op A _).
......@@ -123,8 +120,6 @@ Section cmra_mixin.
Proof. apply (cmra_extend_mixin A). Qed.
End cmra_mixin.
Hint Extern 0 ({0} _) => apply cmra_validN_0.
(** * CMRAs with a global identity element *)
(** We use the notation ∅ because for most instances (maps, sets, etc) the
`empty' element is the global identity. *)
......@@ -142,11 +137,11 @@ Class CMRAMonotone {A B : cmraT} (f : A → B) := {
(** * Frame preserving updates *)
Definition cmra_updateP {A : cmraT} (x : A) (P : A Prop) := z n,
{S n} (x z) y, P y {S n} (y z).
{n} (x z) y, P y {n} (y z).
Instance: Params (@cmra_updateP) 1.
Infix "~~>:" := cmra_updateP (at level 70).
Definition cmra_update {A : cmraT} (x y : A) := z n,
{S n} (x z) {S n} (y z).
{n} (x z) {n} (y z).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
......@@ -251,8 +246,6 @@ Proof. intros Hyv [z ?]; cofe_subst y; eauto using cmra_validN_op_l. Qed.
Lemma cmra_validN_included x y n : {n} y x y {n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_validN_includedN. Qed.
Lemma cmra_includedN_0 x y : x {0} y.
Proof. by exists (unit x). Qed.
Lemma cmra_includedN_S x y n : x {S n} y x {n} y.
Proof. by intros [z Hz]; exists z; apply dist_S. Qed.
Lemma cmra_includedN_le x y n n' : x {n} y n' n x {n'} y.
......@@ -290,19 +283,19 @@ Proof.
Qed.
(** ** Timeless *)
Lemma cmra_timeless_included_l x y : Timeless x {1} y x {1} y x y.
Lemma cmra_timeless_included_l x y : Timeless x {0} y x {0} y x y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
destruct (cmra_extend_op 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (timeless x z).
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y x {1} y x {n} y.
Lemma cmra_timeless_included_r n x y : Timeless y x {0} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
Lemma cmra_op_timeless x1 x2 :
(x1 x2) Timeless x1 Timeless x2 Timeless (x1 x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
destruct (cmra_extend_op 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
{ by rewrite -?Hz. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
......@@ -370,8 +363,6 @@ Section identity_updates.
End identity_updates.
End cmra.
Hint Extern 0 (_ {0} _) => apply cmra_includedN_0.
(** * Properties about monotone functions *)
Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
Proof. by split. Qed.
......@@ -444,22 +435,16 @@ Section discrete.
Context {A : cofeT} `{ x : A, Timeless x}.
Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A).
Instance discrete_validN : ValidN A := λ n x,
match n with 0 => True | S n => x end.
Instance discrete_validN : ValidN A := λ n x, x.
Definition discrete_cmra_mixin : CMRAMixin A.
Proof.
destruct ra; split; unfold Proper, respectful, includedN;
repeat match goal with
| |- n : nat, _ => intros [|?]
end; try setoid_rewrite <-(timeless_S _ _ _ _); try done.
by intros x y ?; exists x.
by destruct ra; split; unfold Proper, respectful, includedN;
try setoid_rewrite <-(timeless_iff _ _ _ _).
Qed.
Definition discrete_extend_mixin : CMRAExtendMixin A.
Proof.
intros [|n] x y1 y2 ??.
* by exists (unit x, x); rewrite /= ra_unit_l.
* exists (y1,y2); split_ands; auto.
apply (timeless _), dist_le with (S n); auto with lia.
intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
apply (timeless _), dist_le with n; auto with lia.
Qed.
Definition discreteRA : cmraT :=
CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
......@@ -512,7 +497,6 @@ Section prod.
* by intros n y1 y2 [Hy1 Hy2] [??]; split; rewrite /= -?Hy1 -?Hy2.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; rewrite /= ?Hx1 ?Hx2 ?Hy1 ?Hy2.
* by split.
* by intros n x [??]; split; apply cmra_validN_S.
* split; simpl; apply (associative _).
* split; simpl; apply (commutative _).
......
......@@ -23,7 +23,7 @@ Tactic Notation "cofe_subst" :=
Record chain (A : Type) `{Dist A} := {
chain_car :> nat A;
chain_cauchy n i : n i chain_car n {n} chain_car i
chain_cauchy n i : n < i chain_car i {n} chain_car (S n)
}.
Arguments chain_car {_ _} _ _.
Arguments chain_cauchy {_ _} _ _ _ _.
......@@ -33,11 +33,10 @@ 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
mixin_conv_compl (c : chain A) n : compl c {n} c (S n)
}.
Class Contractive `{Dist A, Dist B} (f : A -> B) :=
contractive n : Proper (dist n ==> dist (S n)) f.
contractive n x y : ( i, i < n x {i} y) f x {n} f y.
(** Bundeled version *)
Structure cofeT := CofeT {
......@@ -66,14 +65,10 @@ Section cofe_mixin.
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.
Lemma conv_compl (c : chain A) n : compl c {n} c (S 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 {A : cofeT}.
......@@ -109,13 +104,12 @@ Section cofe.
unfold Proper, respectful; setoid_rewrite equiv_dist.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed.
Lemma compl_ne (c1 c2: chain A) n : c1 n {n} c2 n compl c1 {n} compl c2.
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.
Lemma contractive_S {B : cofeT} {f : A B} `{!Contractive f} n x y :
x {n} y f x {S n} f y.
Proof. eauto using contractive, dist_le with omega. Qed.
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.
Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
Global Instance contractive_proper {B : cofeT} (f : A B) `{!Contractive f} :
Proper (() ==> ()) f | 100 := _.
End cofe.
......@@ -127,20 +121,21 @@ Program Definition chain_map `{Dist A, Dist B} (f : A → B)
Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
(** Timeless elements *)
Class Timeless {A : cofeT} (x : A) := timeless y : x {1} y x y.
Class Timeless {A : cofeT} (x : A) := timeless y : x {0} y x y.
Arguments timeless {_} _ {_} _ _.
Lemma timeless_S {A : cofeT} (x y : A) n : Timeless x x y x {S n} y.
Lemma timeless_iff {A : cofeT} (x y : A) n : Timeless x x y x {n} y.
Proof.
split; intros; [by apply equiv_dist|].
apply (timeless _), dist_le with (S n); auto with lia.
apply (timeless _), dist_le with n; auto with lia.
Qed.
(** Fixpoint *)
Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A A)
`{!Contractive f} : chain A := {| chain_car i := Nat.iter i f inhabitant |}.
`{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
Next Obligation.
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.
intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
* apply contractive; auto with omega.
* apply contractive_S, IH; auto with omega.
Qed.
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f).
......@@ -149,17 +144,16 @@ Section fixpoint.
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.
rewrite (conv_compl (fixpoint_chain f) n).
by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
apply equiv_dist=>n; rewrite /fixpoint (conv_compl (fixpoint_chain f) n) //.
induction n as [|n IH]; simpl; eauto using contractive, dist_le with omega.
Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z {n} g z) fixpoint f {n} fixpoint g.
Proof.
intros Hfg; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
induction n as [|n IH]; simpl in *; first done.
rewrite Hfg; apply contractive, IH; auto using dist_S.
intros Hfg. rewrite /fixpoint
(conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n) /=.
induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
rewrite Hfg; apply contractive_S, IH; auto using dist_S.
Qed.
Lemma fixpoint_proper (g : A A) `{!Contractive g} :
( x, f x g x) fixpoint f fixpoint g.
......@@ -188,9 +182,8 @@ Section cofe_mor.
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) /= Hx.
apply (chain_cauchy c); lia.
intros c n x y Hx. by rewrite (conv_compl (fun_chain c x) n)
(conv_compl (fun_chain c y) n) /= Hx.
Qed.
Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
Proof.
......@@ -202,9 +195,8 @@ Section cofe_mor.
+ 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.
by rewrite (conv_compl (fun_chain c x) n) /=.
Qed.
Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
......@@ -262,7 +254,6 @@ Section product.
rewrite !equiv_dist; naive_solver.
* apply _.
* by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
* by split.
* intros c n; split. apply (conv_compl (chain_map fst c) n).
apply (conv_compl (chain_map snd c) n).
Qed.
......@@ -288,17 +279,16 @@ Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
(** Discrete cofe *)
Section discrete_cofe.
Context `{Equiv A, @Equivalence A ()}.
Instance discrete_dist : Dist A := λ n x y,
match n with 0 => True | S n => x y end.
Instance discrete_dist : Dist A := λ n x y, x y.
Instance discrete_compl : Compl A := λ c, c 1.
Definition discrete_cofe_mixin : CofeMixin A.
Proof.
split.
* intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
* intros [|n]; [done|apply _].
* by intros [|n].
* intros x y; split; [done|intros Hn; apply (Hn 0)].
* done.
* done.
* intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
* intros c n. rewrite /compl /discrete_compl /=.
symmetry; apply (chain_cauchy c 0 (S n)); omega.
Qed.
Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
......@@ -314,11 +304,11 @@ Canonical Structure natC := leibnizC nat.
Canonical Structure boolC := leibnizC bool.
(** Later *)
Inductive later (A : Type) : Type := Later { later_car : A }.
Inductive later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Later {_} _.
Arguments Next {_} _.
Arguments later_car {_} _.
Lemma later_eta {A} (x : later A) : Later (later_car x) = x.
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Proof. by destruct x. Qed.
Section later.
......@@ -329,7 +319,7 @@ Section later.
Program Definition later_chain (c : chain (later A)) : chain A :=
{| chain_car n := later_car (c (S n)) |}.
Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
Instance later_compl : Compl (later A) := λ c, Later (compl (later_chain c)).
Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
Definition later_cofe_mixin : CofeMixin (later A).
Proof.
split.
......@@ -340,20 +330,19 @@ Section later.
+ by intros [x] [y].
+ by intros [x] [y] [z] ??; transitivity y.
* intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
* done.
* intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
Qed.
Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
Global Instance Later_contractive : Contractive (@Later A).
Proof. by intros n ??. Qed.
Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Later A).
Global Instance Next_contractive : Contractive (@Next A).
Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
Global Instance Later_inj n : Injective (dist n) (dist (S n)) (@Next A).
Proof. by intros x y. Qed.
End later.
Arguments laterC : clear implicits.
Definition later_map {A B} (f : A B) (x : later A) : later B :=
Later (f (later_car x)).
Next (f (later_car x)).
Instance later_map_ne {A B : cofeT} (f : A B) n :
Proper (dist (pred n) ==> dist (pred n)) f
Proper (dist n ==> dist n) (later_map f) | 0.
......@@ -366,4 +355,4 @@ Proof. by destruct x. Qed.
Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
CofeMor (later_map f).
Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
Proof. intros n f g Hf n'; apply Hf. Qed.
Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.
......@@ -28,33 +28,44 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
( x, f x f' x) ( y, g y g' y) x x'
map (f,g) x map (f',g') x'.
Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
Lemma map_ne {A1 A2 B1 B2 : cofeT}
(f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) n x :
( x, f x {n} f' x) ( y, g y {n} g' y)
map (f,g) x {n} map (f',g') x.
Proof.
intros. by apply map_contractive=> i ?; apply dist_le with n; last lia.
Qed.
Fixpoint A (k : nat) : cofeT :=
match k with 0 => unitC | S k => F (A k) (A k) end.
Fixpoint f {k} : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g,f) end
with g {k} : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, ()) | S k => map (f,g) end.
Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
Lemma gf {k} (x : A k) : g (f x) x.
Fixpoint f (k : nat) : A k -n> A (S k) :=
match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end
with g (k : nat) : A (S k) -n> A k :=
match k with 0 => CofeMor (λ _, ()) | S k => map (f k,g k) end.
Definition f_S k (x : A (S k)) : f (S k) x = map (g k,f k) x := eq_refl.
Definition g_S k (x : A (S (S k))) : g (S k) x = map (f k,g k) x := eq_refl.
Arguments A : simpl never.
Arguments f : simpl never.
Arguments g : simpl never.
Lemma gf {k} (x : A k) : g k (f k x) x.
Proof.
induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Qed.
Lemma fg {n k} (x : A (S k)) : n k f (g x) {n} x.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) {k} x.
Proof.
intros Hnk; apply dist_le with k; auto; clear Hnk.
induction k as [|k IH]; simpl; [apply dist_0|].
rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
induction k as [|k IH]; simpl.
* rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
apply map_contractive=> i ?; omega.
* rewrite f_S g_S -{2}(map_id _ _ x) -map_comp.
apply map_contractive=> i ?; apply dist_le with k; [|omega].
split=> x' /=; apply IH.
Qed.
Arguments A _ : simpl never.
Arguments f {_} : simpl never.
Arguments g {_} : simpl never.
Record tower := {
tower_car k :> A k;
g_tower k : g (tower_car (S k)) tower_car k
g_tower k : g k (tower_car (S k)) tower_car k
}.
Instance tower_equiv : Equiv tower := λ X Y, k, X k Y k.
Instance tower_dist : Dist tower := λ n X Y, k, X k {n} Y k.
......@@ -64,9 +75,9 @@ Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
Program Instance tower_compl : Compl tower := λ c,
{| tower_car n := compl (tower_chain c n) |}.
Next Obligation.
intros c k; apply equiv_dist; intros n.
rewrite (conv_compl (tower_chain c k) n).
by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
intros c k; apply equiv_dist=> n.
by rewrite (conv_compl (tower_chain c k) n)
(conv_compl (tower_chain c (S k)) n) /= (g_tower (c (S n)) k).