From 327acdbd995d31e378c12c71dc8fce756e156b8e Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Sun, 24 Apr 2016 11:39:18 +0200
Subject: [PATCH] define Earlier: kind of the 'opposite' of later
---
algebra/cofe.v | 49 ++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 46 insertions(+), 3 deletions(-)
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 301e0399..469e34a1 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -464,13 +464,14 @@ Section later.
match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end.
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.
+ Next Obligation. intros c n i ?. apply (chain_cauchy c (S n)); lia. Qed.
Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
Definition later_cofe_mixin : CofeMixin (later A).
Proof.
split.
- - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
- split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
+ - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist. split.
+ + intros Hxy [|n]; [done|apply Hxy].
+ + intros Hxy n; apply (Hxy (S n)).
- intros [|n]; [by split|split]; unfold dist, later_dist.
+ by intros [x].
+ by intros [x] [y].
@@ -529,6 +530,48 @@ Proof.
apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
Qed.
+(** Earlier *)
+Inductive earlier (A : Type) : Type := Prev { earlier_car : A }.
+Add Printing Constructor earlier.
+Arguments Prev {_} _.
+Arguments earlier_car {_} _.
+Lemma earlier_eta {A} (x : earlier A) : Prev (earlier_car x) = x.
+Proof. by destruct x. Qed.
+
+Section earlier.
+ Context {A : cofeT}.
+ Instance earlier_equiv : Equiv (earlier A) :=
+ λ x y, earlier_car x ≡ earlier_car y.
+ Instance earlier_dist : Dist (earlier A) :=
+ λ n x y, earlier_car x ≡{S n}≡ earlier_car y.
+ Program Definition earlier_chain (c : chain (earlier A)) : chain A :=
+ {| chain_car n := earlier_car (c n) |}.
+ Next Obligation. intros c n i ?. by apply dist_S, (chain_cauchy c). Qed.
+ Instance earlier_compl : Compl (earlier A) :=
+ λ c, Prev (compl (earlier_chain c)).
+ Definition earlier_cofe_mixin : CofeMixin (earlier A).
+ Proof.
+ split.
+ - intros x y; unfold equiv, earlier_equiv; rewrite !equiv_dist. split.
+ + intros Hxy n; apply dist_S, Hxy.
+ + intros Hxy [|n]; [apply dist_S, Hxy|apply Hxy].
+ - intros n; split; unfold dist, earlier_dist.
+ + by intros [x].
+ + by intros [x] [y].
+ + by intros [x] [y] [z] ??; trans y.
+ - intros n [x] [y] ?; unfold dist, earlier_dist; by apply dist_S.
+ - intros n c. rewrite /compl /earlier_compl /dist /earlier_dist /=.
+ rewrite (conv_compl (S n) (earlier_chain c)). simpl.
+ apply (chain_cauchy c n). omega.
+ Qed.
+ Canonical Structure earlierC : cofeT := CofeT earlier_cofe_mixin.
+ Global Instance Earlier_inj n : Inj (dist (S n)) (dist n) (@Prev A).
+ Proof. by intros x y. Qed.
+End earlier.
+
+Arguments earlierC : clear implicits.
+
+
(** Notation for writing functors *)
Notation "∙" := idCF : cFunctor_scope.
Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
--
GitLab