From 6950fa1d167a390fcb2e11a8e7d788346dbbbfa3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Feb 2016 03:13:32 +0100
Subject: [PATCH] Factor out boring properties of contractive.
---
algebra/cofe.v | 11 +++++++----
algebra/cofe_solver.v | 33 +++++++++------------------------
2 files changed, 16 insertions(+), 28 deletions(-)
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 550c2fc5a..1b77fde09 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -106,9 +106,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 contractive_S {B : cofeT} {f : A → B} `{!Contractive f} n x y :
+ 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.
+ Lemma contractive_0 {B : cofeT} (f : A → B) `{!Contractive f} x y :
+ f x ≡{0}≡ f y.
+ Proof. eauto using contractive 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 x y ?; apply dist_S, contractive_S. Qed.
@@ -136,8 +139,8 @@ Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
`{!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] ?; simpl; try omega.
- * apply contractive; auto with omega.
- * apply contractive_S, IH; auto with omega.
+ * apply (contractive_0 f).
+ * apply (contractive_S f), IH; auto with omega.
Qed.
Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
`{!Contractive f} : A := compl (fixpoint_chain f).
@@ -147,7 +150,7 @@ Section fixpoint.
Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
Proof.
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.
+ induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
Qed.
Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
(∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
diff --git a/algebra/cofe_solver.v b/algebra/cofe_solver.v
index 1a56cc65e..b9f8dbf5b 100644
--- a/algebra/cofe_solver.v
+++ b/algebra/cofe_solver.v
@@ -23,19 +23,6 @@ Context (map_comp : ∀ {A1 A2 A3 B1 B2 B3 : cofeT}
map (f ◎ g, g' ◎ f') x ≡ map (g,g') (map (f,f') x)).
Context (map_contractive : ∀ {A1 A2 B1 B2}, Contractive (@map A1 A2 B1 B2)).
-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' :
- (∀ 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 : nat) : A k -n> A (S k) :=
@@ -51,16 +38,13 @@ 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.
+ rewrite -map_comp -{2}(map_id _ _ x). by apply (contractive_proper map).
Qed.
Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x.
Proof.
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.
+ * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. apply (contractive_0 map).
+ * rewrite f_S g_S -{2}(map_id _ _ x) -map_comp. by apply (contractive_S map).
Qed.
Record tower := {
@@ -197,10 +181,10 @@ Next Obligation.
assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
induction k as [|k IH]; simpl.
{ rewrite -f_tower f_S -map_comp.
- apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f. }
+ by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f. }
rewrite -IH -(dist_le _ _ _ _ (f_tower (k + n) _)); last lia.
rewrite f_S -map_comp.
- apply map_ne=> Y /=. by rewrite g_tower. by rewrite embed_f.
+ by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
Qed.
Definition unfold (X : T) : F T T := compl (unfold_chain X).
Instance unfold_ne : Proper (dist n ==> dist n) unfold.
@@ -214,7 +198,7 @@ Program Definition fold (X : F T T) : T :=
Next Obligation.
intros X k. apply (_ : Proper ((≡) ==> (≡)) (g k)).
rewrite g_S -map_comp.
- apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
+ apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
Qed.
Instance fold_ne : Proper (dist n ==> dist n) fold.
Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
@@ -229,7 +213,7 @@ Proof.
{ rewrite /unfold (conv_compl (unfold_chain X) n).
rewrite -(chain_cauchy (unfold_chain X) n (S (n + k))) /=; last lia.
rewrite -(dist_le _ _ _ _ (f_tower (n + k) _)); last lia.
- rewrite f_S -!map_comp; apply map_ne; fold A=> Y.
+ rewrite f_S -!map_comp; apply (contractive_ne map); split=> Y.
+ rewrite /embed' /= /embed_coerce.
destruct (le_lt_dec _ _); simpl; [exfalso; lia|].
by rewrite (ff_ff _ (eq_refl (S n + (0 + k)))) /= gf.
@@ -246,7 +230,8 @@ Proof.
apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
* intros X; rewrite equiv_dist=> n /=.
rewrite /unfold /= (conv_compl (unfold_chain (fold X)) n) /=.
- rewrite g_S -!map_comp -{2}(map_id _ _ X); apply map_ne=> Y /=.
+ rewrite g_S -!map_comp -{2}(map_id _ _ X).
+ apply (contractive_ne map); split => Y /=.
+ apply dist_le with n; last omega.
rewrite f_tower. apply dist_S. by rewrite embed_tower.
+ etransitivity; [apply embed_ne, equiv_dist, g_tower|apply embed_tower].
--
GitLab