Commit 9df894ee authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use ssreflect for modures.

parent 3967e715
Require Import mathcomp.ssreflect.ssreflect.
Require Import Autosubst.Autosubst. Require Import Autosubst.Autosubst.
Require Import prelude.option prelude.gmap iris.language. Require Import prelude.option prelude.gmap iris.language.
......
...@@ -71,7 +71,7 @@ Proof. ...@@ -71,7 +71,7 @@ Proof.
eauto using agree_valid_le. eauto using agree_valid_le.
Qed. Qed.
Instance: Proper (dist n ==> dist n ==> dist n) op. Instance: Proper (dist n ==> dist n ==> dist n) op.
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy,!(commutative _ _ y2), Hx. Qed. Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(commutative _ _ y2) Hx. Qed.
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _. Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
Instance: Associative () (@op (agree A) _). Instance: Associative () (@op (agree A) _).
Proof. Proof.
...@@ -82,19 +82,20 @@ Qed. ...@@ -82,19 +82,20 @@ Qed.
Lemma agree_includedN (x y : agree A) n : x {n} y y ={n}= x y. Lemma agree_includedN (x y : agree A) n : x {n} y y ={n}= x y.
Proof. Proof.
split; [|by intros ?; exists y]. split; [|by intros ?; exists y].
by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent. by intros [z Hz]; rewrite Hz (associative _) agree_idempotent.
Qed. Qed.
Global Instance agree_cmra : CMRA (agree A). Global Instance agree_cmra : CMRA (agree A).
Proof. Proof.
split; try (apply _ || done). split; try (apply _ || done).
* intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?]. * intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le. rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le.
by apply dist_le with n; try apply Hxy. 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 ->.
* intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?]. * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto. rewrite (Hx n'); last auto.
symmetry; apply dist_le with n; try apply Hx; auto.
* intros x; apply agree_idempotent. * intros x; apply agree_idempotent.
* 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.
...@@ -106,7 +107,7 @@ Global Instance agree_extend : CMRAExtend (agree A). ...@@ -106,7 +107,7 @@ Global Instance agree_extend : CMRAExtend (agree A).
Proof. Proof.
intros n x y1 y2 ? Hx; exists (x,x); simpl; split. intros n x y1 y2 ? 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 done. * by rewrite Hx (agree_op_inv x y1 y2) // agree_idempotent.
Qed. Qed.
Program Definition to_agree (x : A) : agree A := Program Definition to_agree (x : A) : agree A :=
{| agree_car n := x; agree_is_valid n := True |}. {| agree_car n := x; agree_is_valid n := True |}.
...@@ -120,7 +121,7 @@ Proof. by intros ? [? Hx]; apply Hx. Qed. ...@@ -120,7 +121,7 @@ Proof. by intros ? [? Hx]; apply Hx. Qed.
Lemma agree_to_agree_inj (x y : agree A) a n : Lemma agree_to_agree_inj (x y : agree A) a n :
{n} x x ={n}= to_agree a y x n ={n}= a. {n} x x ={n}= to_agree a y x n ={n}= a.
Proof. Proof.
by intros; transitivity ((to_agree a y) n); [by apply agree_car_ne|]. by intros; transitivity ((to_agree a y) n); first apply agree_car_ne.
Qed. Qed.
End agree. End agree.
...@@ -141,7 +142,7 @@ Section agree_map. ...@@ -141,7 +142,7 @@ Section agree_map.
Proof. Proof.
split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]]. split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy. intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
split; [split; simpl; try tauto|done]. split; last done; split; simpl; last tauto.
by intros (?&?&Hxy); repeat split; intros; by intros (?&?&Hxy); repeat split; intros;
try apply Hxy; try apply Hf; eauto using @agree_valid_le. try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Qed. Qed.
...@@ -157,6 +158,6 @@ Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B := ...@@ -157,6 +158,6 @@ Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
CofeMor (agree_map f : agreeRA A 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). Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
Proof. Proof.
intros f g Hfg x; split; simpl; intros; [done|]. intros f g Hfg x; split; simpl; intros; first done.
by apply dist_le with n; try apply Hfg. by apply dist_le with n; try apply Hfg.
Qed. Qed.
...@@ -86,15 +86,15 @@ Instance auth_cmra `{CMRA A} : CMRA (auth A). ...@@ -86,15 +86,15 @@ Instance auth_cmra `{CMRA A} : CMRA (auth A).
Proof. Proof.
split. split.
* apply _. * apply _.
* by intros n x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'. * 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'. * by intros n y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy ?Hy'.
* intros n [x a] [y b] [Hx Ha]; simpl in *; * intros n [x a] [y b] [Hx Ha]; simpl in *;
destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto. destruct Hx as [[][]| | |]; intros ?; cofe_subst; auto.
* by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy']; * by intros n x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'. split; simpl; rewrite ?Hy ?Hy' ?Hx ?Hx'.
* by intros [[] ?]; simpl. * by intros [[] ?]; simpl.
* intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S. * intros n [[] ?] ?; naive_solver eauto using cmra_included_S, cmra_valid_S.
* destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN, * destruct x as [[a| |] b]; simpl; rewrite ?cmra_included_includedN
?cmra_valid_validN; [naive_solver|naive_solver|]. ?cmra_valid_validN; [naive_solver|naive_solver|].
split; [done|intros Hn; discriminate (Hn 1)]. split; [done|intros Hn; discriminate (Hn 1)].
* by split; simpl; rewrite (associative _). * by split; simpl; rewrite (associative _).
......
Require Export mathcomp.ssreflect.ssreflect.
Require Export prelude.prelude.
Global Set Bullet Behavior "Strict Subproofs".
...@@ -110,7 +110,7 @@ Global Instance cmra_ra : RA A. ...@@ -110,7 +110,7 @@ Global Instance cmra_ra : RA A.
Proof. Proof.
split; try by (destruct cmra; split; try by (destruct cmra;
eauto using ne_proper, ne_proper_2 with typeclass_instances). eauto using ne_proper, ne_proper_2 with typeclass_instances).
* by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx. * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite -Hx.
* intros x y; rewrite !cmra_included_includedN. * intros x y; rewrite !cmra_included_includedN.
eauto using cmra_unit_preserving. eauto using cmra_unit_preserving.
* intros x y; rewrite !cmra_valid_validN; intros ? n. * intros x y; rewrite !cmra_valid_validN; intros ? n.
...@@ -125,10 +125,10 @@ Proof. induction 2; eauto using cmra_valid_S. Qed. ...@@ -125,10 +125,10 @@ Proof. induction 2; eauto using cmra_valid_S. Qed.
Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (). Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) ().
Proof. Proof.
intros x1 x2 Hx y1 y2 Hy. intros x1 x2 Hx y1 y2 Hy.
by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2). by rewrite Hy (commutative _ x1) Hx (commutative _ y2).
Qed. Qed.
Lemma cmra_unit_valid x n : {n} x {n} (unit x). Lemma cmra_unit_valid x n : {n} x {n} (unit x).
Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed. Proof. rewrite -{1}(cmra_unit_l x); apply cmra_valid_op_l. Qed.
(** * Timeless *) (** * Timeless *)
Lemma cmra_timeless_included_l `{!CMRAExtend A} x y : Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
...@@ -136,7 +136,7 @@ Lemma cmra_timeless_included_l `{!CMRAExtend A} x y : ...@@ -136,7 +136,7 @@ Lemma cmra_timeless_included_l `{!CMRAExtend A} x y :
Proof. Proof.
intros ?? [x' ?]. intros ?? [x' ?].
destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *. destruct (cmra_extend_op 1 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy, (timeless x z) by done. by exists z'; rewrite Hy (timeless x z).
Qed. 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 {1} y x {n} y.
Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed. Proof. intros ? [x' ?]. exists x'. by apply equiv_dist, (timeless y). Qed.
...@@ -145,8 +145,8 @@ Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 : ...@@ -145,8 +145,8 @@ Lemma cmra_op_timeless `{!CMRAExtend A} x1 x2 :
Proof. Proof.
intros ??? z Hz. intros ??? z Hz.
destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *. destruct (cmra_extend_op 1 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
{ by rewrite <-?Hz; apply cmra_valid_validN. } { by rewrite -?Hz; apply cmra_valid_validN. }
by rewrite Hz', (timeless x1 y1), (timeless x2 y2). by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed. Qed.
(** * Included *) (** * Included *)
...@@ -176,17 +176,17 @@ Proof. ...@@ -176,17 +176,17 @@ Proof.
split. split.
* by intros x; exists (unit x); rewrite ra_unit_r. * by intros x; exists (unit x); rewrite ra_unit_r.
* intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2). * intros x y z [z1 Hy] [z2 Hz]; exists (z1 z2).
by rewrite (associative _), <-Hy, <-Hz. by rewrite (associative _) -Hy -Hz.
Qed. Qed.
Lemma cmra_valid_includedN x y n : {n} y x {n} y {n} x. Lemma cmra_valid_includedN x y n : {n} y x {n} y {n} x.
Proof. intros Hyv [z Hy]; rewrite Hy in Hyv; eauto using cmra_valid_op_l. Qed. Proof. intros Hyv [z Hy]; revert Hyv; rewrite Hy; apply cmra_valid_op_l. Qed.
Lemma cmra_valid_included x y n : {n} y x y {n} x. Lemma cmra_valid_included x y n : {n} y x y {n} x.
Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed. Proof. rewrite cmra_included_includedN; eauto using cmra_valid_includedN. Qed.
Lemma cmra_included_dist_l x1 x2 x1' n : Lemma cmra_included_dist_l x1 x2 x1' n :
x1 x2 x1' ={n}= x1 x2', x1' x2' x2' ={n}= x2. x1 x2 x1' ={n}= x1 x2', x1' x2' x2' ={n}= x2.
Proof. Proof.
intros [z Hx2] Hx1; exists (x1' z); split; auto using ra_included_l. intros [z Hx2] Hx1; exists (x1' z); split; auto using ra_included_l.
by rewrite Hx1, Hx2. by rewrite Hx1 Hx2.
Qed. Qed.
(** * Properties of [(⇝)] relation *) (** * Properties of [(⇝)] relation *)
...@@ -281,11 +281,11 @@ Qed. ...@@ -281,11 +281,11 @@ Qed.
Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B). Instance prod_cmra `{CMRA A, CMRA B} : CMRA (A * B).
Proof. Proof.
split; try apply _. split; try apply _.
* by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2. * by intros n x y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
* by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1, ?Hy2. * by intros n y1 y2 [Hy1 Hy2]; split; simpl in *; rewrite ?Hy1 ?Hy2.
* by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite <-?Hy1, <-?Hy2. * by intros n y1 y2 [Hy1 Hy2] [??]; split; simpl in *; rewrite -?Hy1 -?Hy2.
* by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2]; * by intros n x1 x2 [Hx1 Hx2] y1 y2 [Hy1 Hy2];
split; simpl in *; rewrite ?Hx1, ?Hx2, ?Hy1, ?Hy2. split; simpl in *; rewrite ?Hx1 ?Hx2 ?Hy1 ?Hy2.
* split; apply cmra_valid_0. * split; apply cmra_valid_0.
* by intros n x [??]; split; apply cmra_valid_S. * by intros n x [??]; split; apply cmra_valid_S.
* intros x; split; [by intros [??] n; split; apply cmra_valid_validN|]. * intros x; split; [by intros [??] n; split; apply cmra_valid_validN|].
......
Require Export prelude.prelude. Require Export modures.base.
(** Unbundeled version *) (** Unbundeled version *)
Class Dist A := dist : nat relation A. Class Dist A := dist : nat relation A.
...@@ -75,8 +75,7 @@ Section cofe. ...@@ -75,8 +75,7 @@ Section cofe.
Qed. Qed.
Global Instance dist_proper n : Proper (() ==> () ==> iff) (dist n). Global Instance dist_proper n : Proper (() ==> () ==> iff) (dist n).
Proof. Proof.
intros x1 x2 Hx y1 y2 Hy. by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist Hy; rewrite (Hx n) (Hy n).
by rewrite equiv_dist in Hx, Hy; rewrite (Hx n), (Hy n).
Qed. Qed.
Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x). Global Instance dist_proper_2 n x : Proper (() ==> iff) (dist n x).
Proof. by apply dist_proper. Qed. Proof. by apply dist_proper. Qed.
...@@ -90,10 +89,10 @@ Section cofe. ...@@ -90,10 +89,10 @@ Section cofe.
Proper (() ==> () ==> ()) f | 100. Proper (() ==> () ==> ()) f | 100.
Proof. Proof.
unfold Proper, respectful; setoid_rewrite equiv_dist. unfold Proper, respectful; setoid_rewrite equiv_dist.
by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n), (Hy n). by intros x1 x2 Hx y1 y2 Hy n; rewrite (Hx n) (Hy n).
Qed. Qed.
Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n compl c1 ={n}= compl c2. 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. 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. 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. 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 `{Cofe B} (f : A B) `{!Contractive f} n :
...@@ -118,7 +117,7 @@ Program Definition fixpoint_chain `{Cofe A, Inhabited A} (f : A → A) ...@@ -118,7 +117,7 @@ Program Definition fixpoint_chain `{Cofe A, 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 i f inhabitant |}.
Next Obligation. Next Obligation.
intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|]. intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia. destruct i as [|i]; simpl; first lia; apply contractive, IH; auto with lia.
Qed. Qed.
Program Definition fixpoint `{Cofe A, Inhabited A} (f : A A) Program Definition fixpoint `{Cofe A, Inhabited A} (f : A A)
`{!Contractive f} : A := compl (fixpoint_chain f). `{!Contractive f} : A := compl (fixpoint_chain f).
...@@ -129,14 +128,14 @@ Section fixpoint. ...@@ -129,14 +128,14 @@ Section fixpoint.
Proof. Proof.
apply equiv_dist; intros n; unfold fixpoint. apply equiv_dist; intros n; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f) n). rewrite (conv_compl (fixpoint_chain f) n).
by rewrite (chain_cauchy (fixpoint_chain f) n (S n)) at 1 by lia. by rewrite {1}(chain_cauchy (fixpoint_chain f) n (S n)); last lia.
Qed. Qed.
Lemma fixpoint_ne (g : A A) `{!Contractive g} n : Lemma fixpoint_ne (g : A A) `{!Contractive g} n :
( z, f z ={n}= g z) fixpoint f ={n}= fixpoint g. ( z, f z ={n}= g z) fixpoint f ={n}= fixpoint g.
Proof. Proof.
intros Hfg; unfold fixpoint. intros Hfg; unfold fixpoint.
rewrite (conv_compl (fixpoint_chain f) n),(conv_compl (fixpoint_chain g) n). rewrite (conv_compl (fixpoint_chain f) n) (conv_compl (fixpoint_chain g) n).
induction n as [|n IH]; simpl in *; [done|]. induction n as [|n IH]; simpl in *; first done.
rewrite Hfg; apply contractive, IH; auto using dist_S. rewrite Hfg; apply contractive, IH; auto using dist_S.
Qed. Qed.
Lemma fixpoint_proper (g : A A) `{!Contractive g} : Lemma fixpoint_proper (g : A A) `{!Contractive g} :
...@@ -166,8 +165,8 @@ Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c, ...@@ -166,8 +165,8 @@ Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
{| cofe_mor_car x := compl (fun_chain c x) |}. {| cofe_mor_car x := compl (fun_chain c x) |}.
Next Obligation. Next Obligation.
intros A B c n x y Hxy. intros A B c n x y Hxy.
rewrite (conv_compl (fun_chain c x) n), (conv_compl (fun_chain c y) n). rewrite (conv_compl (fun_chain c x) n) (conv_compl (fun_chain c y) n) /= Hxy.
simpl; rewrite Hxy; apply (chain_cauchy c); lia. apply (chain_cauchy c); lia.
Qed. Qed.
Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B). Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
Proof. Proof.
...@@ -204,7 +203,7 @@ Instance: Params (@ccompose) 3. ...@@ -204,7 +203,7 @@ Instance: Params (@ccompose) 3.
Infix "◎" := ccompose (at level 40, left associativity). Infix "◎" := ccompose (at level 40, left associativity).
Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n : Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
f1 ={n}= f2 g1 ={n}= g2 f1 g1 ={n}= f2 g2. f1 ={n}= f2 g1 ={n}= g2 f1 g1 ={n}= f2 g2.
Proof. by intros Hf Hg x; simpl; rewrite (Hg x), (Hf (g2 x)). Qed. Proof. by intros Hf Hg x; rewrite /= (Hg x) (Hf (g2 x)). Qed.
(** Pre-composition as a functor *) (** Pre-composition as a functor *)
Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n : Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n :
......
...@@ -17,7 +17,7 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT} ...@@ -17,7 +17,7 @@ Lemma map_ext {A1 A2 B1 B2 : cofeT}
(f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' : (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' :
( x, f x f' x) ( y, g y g' y) x x' ( x, f x f' x) ( y, g y g' y) x x'
map (f,g) x map (f',g') x'. map (f,g) x map (f',g') x'.
Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed. Proof. by rewrite -!cofe_mor_ext; intros -> -> ->. Qed.
Fixpoint A (k : nat) : cofeT := Fixpoint A (k : nat) : cofeT :=
match k with 0 => CofeT unit | S k => F (A k) (A k) end. match k with 0 => CofeT unit | S k => F (A k) (A k) end.
...@@ -30,13 +30,13 @@ Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl. ...@@ -30,13 +30,13 @@ 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. Lemma gf {k} (x : A k) : g (f x) x.
Proof. Proof.
induction k as [|k IH]; simpl in *; [by destruct x|]. induction k as [|k IH]; simpl in *; [by destruct x|].
rewrite <-map_comp; rewrite <-(map_id _ _ x) at 2; by apply map_ext. rewrite -map_comp -{2}(map_id _ _ x); by apply map_ext.
Qed. Qed.
Lemma fg {n k} (x : A (S k)) : n k f (g x) ={n}= x. Lemma fg {n k} (x : A (S k)) : n k f (g x) ={n}= x.
Proof. Proof.
intros Hnk; apply dist_le with k; auto; clear Hnk. intros Hnk; apply dist_le with k; auto; clear Hnk.
induction k as [|k IH]; simpl; [apply dist_0|]. induction k as [|k IH]; simpl; [apply dist_0|].
rewrite <-(map_id _ _ x) at 2; rewrite <-map_comp; by apply map_contractive. rewrite -{2}(map_id _ _ x) -map_comp; by apply map_contractive.
Qed. Qed.
Arguments A _ : simpl never. Arguments A _ : simpl never.
Arguments f {_} : simpl never. Arguments f {_} : simpl never.
...@@ -56,8 +56,7 @@ Program Instance tower_compl : Compl tower := λ c, ...@@ -56,8 +56,7 @@ Program Instance tower_compl : Compl tower := λ c,
Next Obligation. Next Obligation.
intros c k; apply equiv_dist; intros n. intros c k; apply equiv_dist; intros n.
rewrite (conv_compl (tower_chain c k) n). rewrite (conv_compl (tower_chain c k) n).
rewrite (conv_compl (tower_chain c (S k)) n); simpl. by rewrite (conv_compl (tower_chain c (S k)) n) /= (g_tower (c n) k).
by rewrite (g_tower (c n) k).
Qed. Qed.
Instance tower_cofe : Cofe tower. Instance tower_cofe : Cofe tower.
Proof. Proof.
...@@ -69,9 +68,9 @@ Proof. ...@@ -69,9 +68,9 @@ Proof.
+ by intros X Y ? n. + by intros X Y ? n.
+ by intros X Y Z ?? n; transitivity (Y n). + by intros X Y Z ?? n; transitivity (Y n).
* intros k X Y HXY n; apply dist_S. * intros k X Y HXY n; apply dist_S.
by rewrite <-(g_tower X), (HXY (S n)), g_tower. by rewrite -(g_tower X) (HXY (S n)) g_tower.
* intros X Y k; apply dist_0. * intros X Y k; apply dist_0.
* intros c n k; simpl; rewrite (conv_compl (tower_chain c k) n). * intros c n k; rewrite /= (conv_compl (tower_chain c k) n).
apply (chain_cauchy c); lia. apply (chain_cauchy c); lia.
Qed. Qed.
Definition T : cofeT := CofeT tower. Definition T : cofeT := CofeT tower.
...@@ -81,16 +80,16 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) := ...@@ -81,16 +80,16 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
Fixpoint gg {k} (i : nat) : A (i + k) -n> A k := 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 end.
Lemma ggff {k i} (x : A k) : gg i (ff i x) x. 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. 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). 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. 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 ff_tower {n} k i (X : tower) : n k ff i (X k) ={n}= X (i + k).
Proof. Proof.
intros; induction i as [|i IH]; simpl; [done|]. intros; induction i as [|i IH]; simpl; [done|].
by rewrite IH, (f_tower X) by lia. by rewrite IH (f_tower X); last lia.
Qed. Qed.
Lemma gg_tower k i (X : tower) : gg i (X (i + k)) X k. 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. Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k). Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
Proof. by intros X Y HX. Qed. Proof. by intros X Y HX. Qed.
...@@ -114,14 +113,14 @@ Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) : ...@@ -114,14 +113,14 @@ Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
Proof. Proof.
assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1. assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1.
induction i2 as [|i2 IH]; intros j X H1; simplify_equality'; induction i2 as [|i2 IH]; intros j X H1; simplify_equality';
[by rewrite coerce_id|by rewrite g_coerce, IH]. [by rewrite coerce_id|by rewrite g_coerce IH].
Qed. Qed.
Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) : Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)). coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
Proof. Proof.
assert (i = i1 + i2) by lia; simplify_equality'. assert (i = i1 + i2) by lia; simplify_equality'.
induction i1 as [|i1 IH]; simplify_equality'; induction i1 as [|i1 IH]; simplify_equality';
[by rewrite coerce_id|by rewrite coerce_f, IH]. [by rewrite coerce_id|by rewrite coerce_f IH].
Qed. Qed.
Definition embed' {k} (i : nat) : A k -n> A i := Definition embed' {k} (i : nat) : A k -n> A i :=
...@@ -135,10 +134,10 @@ Proof. ...@@ -135,10 +134,10 @@ Proof.
* symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl. * symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
* exfalso; lia. * exfalso; lia.
* assert (i = k) by lia; subst. * assert (i = k) by lia; subst.
rewrite (ff_ff _ (eq_refl (1 + (0 + k)))); simpl; rewrite gf. rewrite (ff_ff _ (eq_refl (1 + (0 + k)))) /= gf.
by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))). by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
* assert (H : 1 + ((i - k) + k) = S i) by lia; rewrite (ff_ff _ H); simpl. * assert (H : 1 + ((i - k) + k) = S i) by lia.
rewrite <-(gf (ff (i - k) x)) at 2; rewrite g_coerce.