From a121e07784969067f2edf2824def09f4a18115f2 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Mon, 21 Dec 2015 14:26:16 +0100 Subject: [PATCH] Contractive and non-expansiveness properties of later. --- modures/cofe.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/modures/cofe.v b/modures/cofe.v index 2692e0b0..adfaa867 100644 --- a/modures/cofe.v +++ b/modures/cofe.v @@ -278,8 +278,10 @@ Canonical Structure boolC := leibnizC bool. (** Later *) Inductive later (A : Type) : Type := Later { later_car : A }. +Add Printing Constructor later. Arguments Later {_} _. Arguments later_car {_} _. + Section later. Instance later_equiv `{Equiv A} : Equiv (later A) := λ x y, later_car x ≡ later_car y. @@ -305,12 +307,14 @@ Section later. Qed. Canonical Structure laterC (A : cofeT) : cofeT := CofeT (later A). + Global Instance Later_contractive `{Dist A} : Contractive (@Later A). + Proof. by intros n ??. Qed. Definition later_map {A B} (f : A → B) (x : later A) : later B := Later (f (later_car x)). - Instance later_fmap_ne `{Cofe A, Cofe B} (f : A → B) : - (∀ n, Proper (dist n ==> dist n) f) → - ∀ n, Proper (dist n ==> dist n) (later_map f). - Proof. intros Hf [|n] [x] [y] ?; do 2 red; simpl. done. by apply Hf. Qed. + Global Instance later_map_ne `{Cofe A, Cofe B} (f : A → B) n : + Proper (dist (pred n) ==> dist (pred n)) f → + Proper (dist n ==> dist n) (later_map f) | 0. + Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed. Lemma later_fmap_id {A} (x : later A) : later_map id x = x. Proof. by destruct x. Qed. Lemma later_fmap_compose {A B C} (f : A → B) (g : B → C) (x : later A) : -- GitLab