Commit 07d525a0 by Robbert Krebbers

COFE distance is no longer trivial at index 0.

```This way we avoid many one-off indexes and no longer need special cases for
index 0 in many definitions. For example, the definition of the distance
relation on option and excl has become much easier. Also, uPreds no longer need
to hold at index 0.

In order to make this change possible, we had to change the notions of
"contractive functions" and "chains" slightly.

Thanks to Aleš Bizjak and Amin Timany for suggesting this change and to help
with the proofs.```
parent 7f8d960d
 ... ... @@ -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). Qed. Definition tower_cofe_mixin : CofeMixin tower. Proof. ... ... @@ -79,24 +90,23 @@ Proof. + by intros X Y Z ?? n; transitivity (Y n). * intros k X Y HXY n; apply dist_S. by rewrite -(g_tower X) (HXY (S n)) g_tower. * intros X Y k; apply dist_0. * intros c n k; rewrite /= (conv_compl (tower_chain c k) n). apply (chain_cauchy c); lia. Qed. Definition T : cofeT := CofeT tower_cofe_mixin. Fixpoint ff {k} (i : nat) : A k -n> A (i + k) := match i with 0 => cid | S i => f ◎ ff i end. match i with 0 => cid | S i => f (i + k) ◎ ff i end. Fixpoint gg {k} (i : nat) : A (i + k) -n> A k := match i with 0 => cid | S i => gg i ◎ g end. match i with 0 => cid | S i => gg i ◎ g (i + k) end. Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x. Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ≡{n}≡ X (S k). Proof. intros. by rewrite -(fg (X (S k))) // -(g_tower X). Qed. Lemma ff_tower {n} k i (X : tower) : n ≤ k → ff i (X k) ≡{n}≡ X (i + k). Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)). Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed. Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k). Proof. intros; induction i as [|i IH]; simpl; [done|]. by rewrite IH (f_tower X); last lia. by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega. Qed. Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k. Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed. ... ... @@ -113,10 +123,10 @@ Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) : x = y → coerce H1 x = coerce H2 y. Proof. by destruct H1; rewrite !coerce_id. Qed. Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) : g (coerce H x) = coerce (Nat.succ_inj _ _ H) (g x). g j (coerce H x) = coerce (Nat.succ_inj _ _ H) (g k x). Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. Lemma coerce_f {k j} (H : S k = S j) (x : A k) : coerce H (f x) = f (coerce (Nat.succ_inj _ _ H) x). coerce H (f k x) = f j (coerce (Nat.succ_inj _ _ H) x). Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed. Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) : gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)). ... ... @@ -133,14 +143,15 @@ Proof. [by rewrite coerce_id|by rewrite coerce_f IH]. Qed. Definition embed' {k} (i : nat) : A k -n> A i := Definition embed_coerce {k} (i : nat) : A k -n> A i :=