Added a library for solving recursive domain equations.

lib/recdom/CBUltInst.v

+(** This file provides the proof that CBUlt, the category of complete,
+    bisected, ultrametric spaces, forms an M-category. *)
+
+Require Import MetricCore.
+Require Import MetricRec.
+
+Module CBUlt <: MCat.
+  Local Open Scope cat_scope.
+  Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
+
+  Definition M := cmtyp.
+  Instance MArr   : BC_morph M := fun U V : cmtyp => cmfromType (U -n> V).
+  Instance MComp  : BC_comp  M := fun U V W => comp.
+  Instance MId    : BC_id    M := fun U => (umid _).
+  Instance MTermO : BC_term  M := cmfromType unit.
+  Program Instance MTermA : BC_terminal M := fun U => n[(const tt)].
+
+  Instance Cat : BaseCat M.
+  Proof.
+    split; intros; intros n; simpl; reflexivity || exact I.
+  Qed.
+
+  Section Limits.
+    Context (T : Tower).
+
+    Definition guard := fun (σ : forall i, tow_objs T i) => forall n, tow_morphs T n (σ (S n)) == σ n.
+    Instance lpg : LimitPreserving guard.
+    Proof.
+      intros σ σc HG n.
+      rewrite !dep_chain_compl.
+      rewrite nonexp_continuous; apply umet_complete_ext; intros k.
+      simpl; apply HG.
+    Qed.
+
+    Definition lim_obj : cmtyp := cmfromType {σ : forall i, tow_objs T i | guard σ}.
+    Definition lim_proj i : lim_obj -n> tow_objs T i := MprojI i <M< inclM.
+
+    Program Definition lim_cone : Cone T := mkBaseCone T lim_obj lim_proj _.
+    Next Obligation.
+      intros [σ HG]; simpl; apply HG.
+    Qed.
+
+    Program Definition lim_map (C : Cone T) : (cone_t T C : cmtyp) -n> (cone_t T lim_cone : cmtyp) :=
+      n[(fun m => exist _ (fun i => cone_m T C i m) _)].
+    Next Obligation.
+      intros n; simpl.
+      assert (HT := cone_m_com T C n m); apply HT.
+    Qed.
+
+    Lemma AllLimits : Limit T.
+    Proof.
+      refine (mkBaseLimit T lim_cone lim_map _ _).
+      + intros C n x; simpl; reflexivity.
+      + intros C h HCom x n; simpl.
+        specialize (HCom n x); simpl in HCom.
+        symmetry; apply HCom.
+    Qed.
+
+  End Limits.
+End CBUlt.

lib/recdom/CSetoid.v

+(** Basic categorical definitions. The role of objects is played by
+    the class [type] which is a type equipped with an equivalence
+    relation.
+
+    Then there are standard constructions defined using these objects
+    (product, exponential, initial objects and functors at the end)
+    and some of their properties are proved.
+ *)
+Require Export Coq.Program.Program.
+Require Export Morphisms SetoidClass SetoidTactics.
+
+Generalizable Variables T U V W.
+
+(* Make sure equiv is in the right scope and that it's not simplified
+   too soon. *)
+Definition equiv `{Setoid T} := SetoidClass.equiv.
+Arguments equiv {_ _} _ _ /.
+
+Notation "'mkType' R" := (@Build_Setoid _ R _) (at level 10).
+
+(** A morphism between two types is an actual function together with a
+    proof that it preserves equality. *)
+Record morphism S T `{eqS : Setoid S} `{eqT : Setoid T} :=
+  mkMorph {
+    morph :> S -> T;
+    morph_resp : Proper (equiv ==> equiv) morph}.
+
+Arguments mkMorph [S T eqS eqT] _ _.
+Arguments morph_resp [S T eqS eqT] _ _ _ _.
+
+Infix "-=>" := morphism (at level 45, right associativity).
+Notation "'s[(' f ')]'" := (mkMorph f _).
+Ltac resp_set :=
+  intros t1 t2 HEqt; repeat (intros ?); simpl in *; try rewrite !HEqt; reflexivity.
+
+(** This seems just to be a package putting together all the
+    ingredients of [type], i.e. the carrier set, the relation and the
+    property that the relation is an equivalence relation. *)
+Record eqType :=
+  {eqtyp  :> Type;
+   eqtype :  Setoid eqtyp}.
+Instance eqType_proj_type {ET : eqType} : Setoid ET := eqtype _.
+Definition fromType T `{eT : Setoid T} : eqType := Build_eqType T _.
+
+Section Morphisms.
+  Context `{eT : Setoid T} `{eU : Setoid U} `{eV : Setoid V}.
+
+  (** The type of equivalence-preserving maps is again a type with
+      equivalence, defined pointwise. *)
+  Global Program Instance morph_type : Setoid (T -=> U) :=
+    mkType (fun f g => forall x, f x == g x).
+  Next Obligation.
+    clear; split.
+    - intros f x; reflexivity.
+    - intros f g HS x; symmetry; apply HS.
+    - intros f g h Hfg Hgh x; etransitivity; [apply Hfg | apply Hgh].
+  Qed.
+
+  (** The application of [morphsm] to its argument preserves equality
+      in both the function and the argument. *)
+  Global Instance equiv_morph :
+    Proper (equiv ==> equiv ==> equiv) (morph T U).
+  Proof.
+    intros f g HEq x y HEq'; etransitivity; [apply HEq | apply g, HEq'].
+  Qed.
+
+  (** Definition of composition of morphisms. Note the different
+      arrows, i.e., -=> and ->. *)
+  Program Definition mcomp (f: U -=> V) (g: T -=> U) : (T -=> V) :=
+    s[(f ∘ g)].
+  Next Obligation.
+    intros x y HEq; apply f, g; assumption.
+  Qed.
+
+  Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
+
+  (** Two specific morphisms, identity and constant maps. *)
+  Program Definition mid : T -=> T := s[(fun x => x)].
+
+  Program Definition mconst (u : U) : T -=> U := s[(const u)].
+
+End Morphisms.
+
+Infix "<<" := mcomp (at level 35).
+Arguments mid T {eT}.
+Arguments compose {_ _ _} _ _ _ /.
+
+Section MorphConsts.
+  Context `{eT : Setoid T} `{eU : Setoid U} `{eV : Setoid V} `{eW : Setoid W}.
+
+  (** Composition maps equal morphism to equal morphisms. *)
+  Global Instance equiv_mcomp :
+    Proper (equiv (T := U -=> V) ==> equiv ==> equiv) mcomp.
+  Proof.
+    intros f f' HEq g g' HEq' x; simpl; rewrite HEq, HEq'; reflexivity.
+  Qed.
+
+  (** Composition of morphisms is associative. *)
+  Lemma mcomp_assoc (f: V -=> W) (g: U -=> V) (h: T -=> U) :
+    f << (g << h) == (f << g) << h.
+  Proof. intros x; reflexivity. Qed.
+
+  (** Identity is left- and right- identity for composition *)
+  Lemma mcomp_idR (f : U -=> V) :
+    f << mid _ == f.
+  Proof. intros x; reflexivity. Qed.
+  Lemma mcomp_idL (f : U -=> V) :
+    mid _ << f == f.
+  Proof. intros x; reflexivity. Qed.
+
+  (** Lift an ordinary function to a function on [type]'s. *)
+  Definition lift2s (f : T -> U -> V) p q : (T -=> U -=> V) :=
+    mkMorph (fun x => mkMorph (f x) (p x)) q.
+
+  Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
+
+  (** Pre- and postcomposition, as equality-preserving maps *)
+  Program Definition precomp (f : T -=> U) : (U -=> V) -=> (T -=> V) :=
+    s[(fun g => g << f)].
+
+  Program Definition postcomp (f : T -=> U) : (V -=> T) -=> (V -=> U) :=
+    s[(fun g => f << g)].
+
+End MorphConsts.
+
+(*Instance Equiv_PropP : Equiv Prop := iff.
+Instance type_PropP : type Prop := iff_equivalence.*)
+
+Section SetoidProducts.
+  Context `{eU : Setoid U} `{eV : Setoid V}.
+
+  (** The product of two types is another type, with equality defined pointwise. *)
+  Global Program Instance prod_type : Setoid (U * V) :=
+    mkType (fun p1 p2 : U * V => (fst p1) == (fst p2) /\ (snd p1) == (snd p2)).
+  Next Obligation.
+    split.
+    - intros [u v]; split; reflexivity.
+    - intros [u1 v1] [u2 v2] [Hu Hv]; split; symmetry; assumption.
+    - intros [u1 v1] [u2 v2] [u3 v3] [Hu12 Hv12] [Hu23 Hv23]; split; etransitivity; eassumption.
+  Qed.
+
+  Global Instance prod_proper : Proper (equiv ==> equiv ==> equiv) (@pair U V).
+  Proof.
+    intros u1 u2 Hu v1 v2 Hv; split; assumption.
+  Qed.
+
+  Global Instance mfst_proper : Proper (equiv ==> equiv) (@fst U V).
+  Proof.
+    intros [u1 v1] [u2 v2] [Hu Hv]; assumption.
+  Qed.
+
+  Global Instance msnd_proper : Proper (equiv ==> equiv) (@snd U V).
+  Proof.
+    intros [u1 v1] [u2 v2] [Hu Hv]; assumption.
+  Qed.
+
+  Local Obligation Tactic := intros; resp_set || program_simpl.
+
+  (** The projections are in fact proper morphisms, i.e. they preserve equality. *)
+  Program Definition mfst : (U * V) -=> U := s[(fst)].
+
+  Program Definition msnd : (U * V) -=> V := s[(snd)].
+
+  Context `{eT : Setoid T}.
+
+  (** Tupling is also a proper morphism, i.e. respects equality. *)
+  Program Definition mprod (f: T -=> U) (g: T -=> V) : T -=> (U * V) :=
+    s[(fun t => (f t, g t))].
+  Next Obligation.
+    add_morphism_tactic; intros.
+    rewrite H; reflexivity.
+  Qed.
+
+  Lemma mprod_unique (f: T -=> U) (g: T -=> V) (h: T -=> U * V) :
+    mfst << h == f -> msnd << h == g -> h == mprod f g.
+  Proof.
+    intros HL HR x; split; simpl; [rewrite <- HL | rewrite <- HR]; reflexivity.
+  Qed.
+
+End SetoidProducts.
+
+Arguments mprod_unique [U eU V eV T eT f g h] _ _ _.
+
+Section IndexedProducts.
+  Context {I : Type} {P : I -> eqType}.
+
+  (** Equality on the indexed product. Essentially the same as for binary products, i.e. pointwise. *)
+  Global Program Instance prodI_type : Setoid (forall i, P i) :=
+    mkType (fun p1 p2 => forall i, p1 i == p2 i).
+  Next Obligation.
+    split.
+    - intros X x; reflexivity.
+    - intros X Y HS x; symmetry; apply HS.
+    - intros X Y Z HPQ HQR x; etransitivity; [apply HPQ | apply HQR].
+  Qed.
+
+  Local Obligation Tactic := intros; resp_set || program_simpl.
+
+  (** Projection functions. *)
+  Program Definition mprojI (i : I) : (forall i, P i) -=> P i :=
+    s[(fun X => X i)].
+
+  Context `{eT : Setoid T}.
+
+  (** Tupling into the indexed products. *)
+  Program Definition mprodI (f : forall i, T -=> P i) : T -=> (forall i, P i) :=
+    s[(fun t i => f i t)].
+
+  Lemma mprod_projI (f : forall i, T -=> P i) i : mprojI i << mprodI f == f i.
+  Proof. intros X; reflexivity. Qed.
+
+  (** Product with the projections is an actual product. *)
+  Lemma mprodI_unique (f : forall i, T -=> P i) (h : T -=> forall i, P i) :
+    (forall i, mprojI i << h == f i) -> h == mprodI f.
+  Proof.
+    intros HEq x i; simpl; rewrite <- HEq; reflexivity.
+  Qed.
+
+End IndexedProducts.
+
+Section Exponentials.
+  Context `{eT : Setoid T} `{eU : Setoid U} `{eV : Setoid V} `{eW : Setoid W}.
+
+  Local Obligation Tactic := intros; resp_set || program_simpl.
+
+  (** Composition of morphism _as a morphims_. *)
+  Program Definition comps : (U -=> V) -=> (T -=> U) -=> T -=> V :=
+    lift2s (fun f g => f << g) _ _.
+
+  Program Definition muncurry (f : T -=> U -=> V) : T * U -=> V :=
+    s[(fun p => f (fst p) (snd p))].
+  Next Obligation.
+    add_morphism_tactic; intros [t1 u1] [t2 u2] [Ht Hu]; simpl in *.
+    rewrite Ht, Hu; reflexivity.
+  Qed.
+
+  (** Currying map, i.e. the exponential transpose. *)
+  Program Definition mcurry (f : T * U -=> V) : T -=> U -=> V :=
+    lift2s (fun t u => f (t, u)) _ _.
+
+  (** f × g, i.e. 〈 f ∘ π, g ∘ π' 〉 *)
+  Definition mprod_map (f : T -=> U) (g : V -=> W) := mprod (f << mfst) (g << msnd).
+
+  (** Evaluation map. *)
+  Program Definition meval : (T -=> U) * T -=> U :=
+    s[(fun p => fst p (snd p))].
+  Next Obligation.
+    add_morphism_tactic; intros [f1 t1] [f2 t2] [Hf Ht]; simpl in *.
+    rewrite Hf, Ht; reflexivity.
+  Qed.
+
+End Exponentials.
+
+Section Exp_props.
+  Context `{eT : Setoid T} `{eU : Setoid U} `{eV : Setoid V} `{eW : Setoid W}.
+
+  (** (Λ(f) × id) ; eval = f, where Λ(f) is the exponential transpose. *)
+  Lemma mcurry_com (f : T * U -=> V) : f == meval << (mprod_map (mcurry f) (mid _)).
+  Proof. intros [a b]; reflexivity. Qed.
+
+  (** Exponential transposes are unique. *)
+  Lemma mcurry_unique (f : T * U -=> V) h :
+    f == meval << (mprod_map h (mid _)) -> h == mcurry f.
+  Proof. intros HEq a b; simpl; rewrite HEq; reflexivity. Qed.
+
+End Exp_props.
+
+Program Instance unit_type : Setoid unit := mkType (fun _ _ => True).
+Next Obligation.
+  split.
+  - intros _; exact I.
+  - intros _ _ _; exact I.
+  - intros _ _ _ _ _; exact I.
+Qed.
+
+(** The [unit] type is the terminal object, i.e., there's a unique
+    morphism from any [Setoid] to [unit] *)
+Section Terminals.
+  Context `{eT : Setoid T}.
+
+  Definition mone_term : T -=> unit := mconst tt.
+
+  Lemma mone_term_unique (f g : T -=> unit) : f == g.
+  Proof.
+    intros x; destruct (f x); destruct (g x); reflexivity.
+  Qed.
+
+End Terminals.
+
+Inductive empty : Set :=.
+Program Instance empty_type : Setoid empty := mkType (fun _ _ => False).
+Next Obligation.
+  split; intros x; case x.
+Qed.
+
+
+(** The empty [type] is the initial element, i.e. there is unique a
+    morphism from it to any other [type]. *)
+Section Initials.
+  Context `{eT : Setoid T}.
+
+  Program Definition mzero_init : empty -=> T := s[(fun x => match x with end)].
+  Next Obligation. intros x; case x; fail. Qed.
+
+  Lemma mzero_init_unique (f g : empty -=> T) : f == g.
+  Proof. intros x; case x. Qed.
+
+End Initials.
+
+(** Subsets. *)
+Section Subsetoid.
+  Context `{eT : Setoid T} {P : T -> Prop}.
+
+  (** [type] of elements that satisfy the predicate P, i.e. a
+      subset. Equality is inherited from the carrier type. *)
+  Global Program Instance subset_type : Setoid {t : T | P t} :=
+    mkType (fun x y => ` x == ` y).
+  Next Obligation.
+    split.
+    - intros [x Hx]; simpl; reflexivity.
+    - intros [x Hx] [y Hy] HS; simpl in *; symmetry; assumption.
+    - intros [x Hx] [y Hy] [z Hz] Hxy Hyz; simpl in *; etransitivity; eassumption.
+  Qed.
+
+  Global Instance proj1sig_proper :
+    Proper (equiv (T := {t : T | P t}) ==> equiv) (@proj1_sig _ _).
+  Proof. intros [x Hx] [y Hy] HEq; simpl in *; assumption. Qed.
+
+  (** Inclusion from the subset to the superset is an
+      equality-preserving morphism. *)
+  Program Definition mincl : {t : T | P t} -=> T := s[(@proj1_sig _ _)].
+
+  (** If we have a morphism from B to A whose image is in the subset
+      determined by P, then this morphism restricts to the one into
+      the subset determined by P. *)
+  Context `{eU : Setoid U}.
+  Program Definition minherit (f : U -=> T) (HB : forall u, P (f u)) :
+    U -=> {t : T | P t} := s[(fun u => exist P (f u) (HB u))].
+  Next Obligation.
+    intros x y HEq; unfold equiv; red; simpl; rewrite HEq; reflexivity.
+  Qed.
+
+  (** Inclusion from subset determined by P to the superset is a monomorphism. *)
+  Lemma mforget_mono (f g : U -=> {t : T | P t}) :
+    mincl << f == mincl << g -> f == g.
+  Proof.
+    intros HEq x; simpl; rewrite (HEq x); reflexivity.
+  Qed.
+
+End Subsetoid.
+
+(** Lifting of a type by adding a new distinct element.
+
+    This is used for several constructions: lookups in finite maps
+    return function types, for instance.
+ *)
+Section Option.
+  Context `{eT : Setoid T}.
+
+  Definition opt_eq (x y : option T) :=
+    match x, y with
+      | None, None => True
+      | Some x, Some y => x == y
+      | _, _ => False
+    end.
+
+  Global Program Instance option_type : Setoid (option T) :=
+    mkType opt_eq.
+  Next Obligation.
+    split.
+    - intros [a |]; simpl; reflexivity.
+    - intros [a |] [b |] HS; simpl in *; now trivial || symmetry; assumption.
+    - intros [a |] [b |] [c |] Hab Hbc; simpl in *; try (exact I || contradiction); [].
+      etransitivity; eassumption.
+  Qed.
+
+End Option.
+
+Section OptDefs.
+  Context `{eT : Setoid T} `{eU : Setoid U}.
+
+  Global Instance Some_proper : Proper (equiv ==> equiv) (@Some T).
+  Proof. intros a b HEq; simpl; apply HEq. Qed.
+
+  Program Definition msome : T -=> option T := s[(@Some T)].
+
+  Definition optbind (f : T -> option U) (ov : option T) : option U :=
+    match ov with
+      | Some v => f v
+      | None   => None
+    end.
+
+  Program Definition moptbind : (T -=> option U) -=> option T -=> option U :=
+    lift2s optbind _ _.
+  Next Obligation.
+    intros [v1 |] [v2 |] EQv; try (contradiction EQv || exact I); [].
+    unfold optbind; apply x, EQv.
+  Qed.
+  Next Obligation.
+    intros f1 f2 EQf [x |]; [simpl morph | exact I].
+    apply EQf.
+  Qed.
+
+End OptDefs.

lib/recdom/Constr.v

+(** This module provides some additional constructions on CBUlt. These
+    are:
+    - the "1/2" functor, which divides all the distances by 1/2,
+      and so makes any locally non-expansive functor locally
+      contractive,
+    - an extension operation on the space Tᵏ, for k ∈ nat, as a
+      non-expansive morphism. *)
+
+Require Import MetricRec.
+Require Export UPred.
+
+Section Halving.
+  Context (T : cmtyp).
+
+  Definition dist_halve n :=
+    match n with
+      | O  => fun (_ _ : T) => True
+      | S n => dist n
+    end.
+
+  Program Definition halve_metr : metric T := mkMetr dist_halve.
+  Next Obligation.
+    destruct n; [resp_set | simpl; apply _].
+  Qed.
+  Next Obligation.
+    split; intros HEq.
+    - apply dist_refl; intros n; apply (HEq (S n)).
+    - intros [| n]; [exact I |]; revert n; apply dist_refl, HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 HEq; destruct n; [exact I |]; symmetry; apply HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 t3 HEq12 HEq23; destruct n; [exact I |]; etransitivity; [apply HEq12 | apply HEq23].
+  Qed.
+  Next Obligation.
+    destruct n; [exact I | apply dist_mono, H].
+  Qed.
+
+  Definition halveM : Mtyp := Build_Mtyp T halve_metr.
+
+  Instance halve_chain (σ : chain halveM) {σc : cchain σ} : cchain (fun n => σ (S n) : T).
+  Proof.
+    unfold cchain; intros.
+    apply (chain_cauchy σ σc (S n)); auto with arith.
+  Qed.
+
+  Definition compl_halve (σ : chain halveM) (σc : cchain σ) :=
+    compl (fun n => σ (S n)) (σc := halve_chain σ).
+
+  Program Definition halve_cm : cmetric halveM := mkCMetr compl_halve.
+  Next Obligation.
+    intros [| n]; [exists 0; intros; exact I |].
+    destruct (conv_cauchy _ (σc := halve_chain σ) n) as [m HCon].
+    exists (S m); intros [| i] HLe; [inversion HLe |].
+    apply HCon; auto with arith.
+  Qed.
+
+  Definition halve : cmtyp := Build_cmtyp halveM halve_cm.
+
+End Halving.
+
+Ltac unhalve :=
+  match goal with
+    | |- dist_halve _ ?n ?f ?g => destruct n as [| n]; [exact I | change (f = n = g) ]
+    | |- ?f = ?n = ?g => destruct n as [| n]; [exact I | change (f = n = g) ]
+  end.
+
+(* TODO: Refactor the following so that one can make it work for PCM
+         instantiation without a lot of extra work. *)
+Require Import CBUltInst.
+
+Section Halving_Fun.
+  Context F {FA : BiFMap F} {FFun : BiFunctor F}.
+  Local Obligation Tactic := intros; resp_set || eauto.
+
+  Program Instance halveFMap : BiFMap (fun T1 T2 => halve (F T1 T2)) :=
+    fun m1 m2 m3 m4 => lift2m (lift2s (fun ars ob => fmorph (F := F) ars ob) _ _) _ _.
+  Next Obligation.
+    intros p1 p2 EQp x; simpl; rewrite EQp; reflexivity.
+  Qed.
+  Next Obligation.
+    intros e1 e2 EQ; simpl. unhalve.
+    rewrite EQ; reflexivity.
+  Qed.
+  Next Obligation.
+    intros p1 p2 EQ e; simpl; unhalve.
+    apply dist_mono in EQ.
+    rewrite EQ; reflexivity.
+  Qed.
+
+  Instance halveF : BiFunctor (fun T1 T2 => halve (F T1 T2)).
+  Proof.
+    split; intros.
+    + intros T; simpl.
+      apply (fmorph_comp _ _ _ _ _ _ _ _ _ _ T).
+    + intros T; simpl.
+      apply (fmorph_id _ _ T).
+  Qed.
+
+  Instance halve_contractive {m0 m1 m2 m3} :
+    contractive (@fmorph _ _ (fun T1 T2 => halve (F T1 T2)) _ m0 m1 m2 m3).
+  Proof.
+    intros n p1 p2 EQ f; simpl.
+    change ((fmorph (F := F) p1) f = n = (fmorph p2) f).
+    rewrite EQ; reflexivity.
+  Qed.
+
+End Halving_Fun.
+
+Module Type SimplInput(Cat : MCat).
+  Import Cat.
+
+  Parameter F : M -> M -> M.
+  Parameter FArr : BiFMap F.
+  Parameter FFun : BiFunctor F.
+
+  Parameter F_ne : (1 -t> F 1 1)%cat.
+End SimplInput.
+
+Module InputHalve (S : SimplInput (CBUlt)) : InputType(CBUlt)
+    with Definition F := fun T1 T2 => halve (S.F T1 T2).
+  Import CBUlt.
+  Local Existing Instance S.FArr.
+  Local Existing Instance S.FFun.
+  Local Open Scope cat_scope.
+
+  Definition F T1 T2 := halve (S.F T1 T2).
+  Definition FArr := halveFMap S.F.
+  Definition FFun := halveF S.F.
+
+  Definition tmorph_ne : 1 -t> F 1 1 :=
+    umconst (S.F_ne tt : F 1 1).
+
+  Definition F_contractive := @halve_contractive S.F _.
+End InputHalve.
+
+(** Trivial extension of a nonexpansive morphism to monotone one on a
+    metric space equipped with a trivial preorder. *)
+Section DiscM_Defs.
+  Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}.
+
+  Local Instance pt_disc P `{cmetric P} : preoType P | 2000 := disc_preo P.
+  Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
+
+  Definition disc_m (m : V -n> U) : V -m> U := m[(m)].
+
+End DiscM_Defs.
+
+Section DiscM_Props.
+  Context U V W `{cmU : cmetric U} `{cmV : cmetric V} `{cmW : cmetric W}.
+
+  Global Instance disc_equiv : Proper (equiv (T := U -n> V) ==> equiv) disc_m.
+  Proof. resp_set. Qed.
+  Global Instance disc_dist n : Proper (dist (T := U -n> V) n ==> dist n) disc_m.
+  Proof. resp_set. Qed.
+
+  Lemma disc_m_comp (f : V -n> W) (g : U -n> V) :
+    disc_m (f <M< g) == disc_m f ∘ disc_m g.
+  Proof. intros x; simpl morph; reflexivity. Qed.
+
+  Lemma disc_m_id : disc_m (umid W) == pid W.
+  Proof. intros x; simpl morph; reflexivity. Qed.
+
+End DiscM_Props.
+
+Section EvaluationClosure.
+  Context {T} {preoT : preoType T} (step : T -> T -> Prop).
+  Definition irr t := forall t', ~ step t t'.
+
+  Definition ext_step :=
+    forall t1 t2 t2' (HSub : t1 ⊑ t2) (HStep : step t2 t2'),
+    exists t1', step t1 t1' /\ t1' ⊑ t2'.
+  Context (HES : ext_step) (HEI : Proper (pord --> impl) irr).
+
+  Section Def.
+    Variable (R : UPred T).
+
+    Fixpoint pre_evalCl n t : Prop :=
+      (irr t -> R n t) /\
+      forall t' (HS : step t t'),
+        match n with
+          | O => True
+          | S n => pre_evalCl n t'
+        end.
+    Program Definition evalCl := mkUPred pre_evalCl _.
+    Next Obligation.
+      intros m n t t' HLe HSubt HEv.
+      revert m t t' HLe HSubt HEv; induction n; intros.
+      - simpl; split; [| tauto].
+        rewrite <- HSubt, HLe; destruct m; apply HEv.
+      - destruct m as [| m]; [now inversion HLe |]; simpl; split; [| intros].
+        rewrite <- HSubt, HLe; apply HEv.
+        destruct (HES _ _ _ HSubt HS) as [t1 [HS' HSub]].
+        simpl in HEv; apply proj2 in HEv.
+        eapply IHn, HEv; eassumption || auto with arith.
+    Qed.
+    Lemma evalCl_simpl n t :
+      evalCl n t == ((irr t -> R n t) /\ forall t' (HS : step t t'), (▹ evalCl)%up n t').
+    Proof. destruct n; reflexivity. Qed.
+    Opaque evalCl.
+
+  End Def.
+
+  Global Instance eval_equiv : Proper (equiv ==> equiv) evalCl.
+  Proof.
+    apply equiv_upred_simpl; [apply _ |]; intros R1 R2 n t EQR HEv; revert t HEv; induction n; intros.
+    - rewrite evalCl_simpl in *; simpl; split; [| tauto]; destruct HEv as [HIrr _].
+      rewrite <- EQR; assumption.
+    - rewrite evalCl_simpl in HEv; destruct HEv as [HIrr HEv].
+      rewrite evalCl_simpl; split; [rewrite <- EQR; assumption | intros].
+      apply IHn, HEv, HS.
+  Qed.
+
+  Global Instance eval_dist n : Proper (dist n ==> dist n) evalCl.
+  Proof.
+    apply dist_upred_simpl; [apply _ |]; intros R1 R2 m t HLt EQR HEv;
+    revert t HEv; induction m; intros.
+    - rewrite evalCl_simpl in *; destruct HEv as [HIrr _]; simpl; split; [| tauto].
+      intros HIrred; apply EQR, HIrr, HIrred; assumption.
+    - rewrite evalCl_simpl in HEv; rewrite evalCl_simpl.
+      split; [| intros; apply IHm, HEv, HS; now auto with arith].
+      intros HIrr; apply EQR, HEv, HIrr; assumption.
+  Qed.
+
+  Global Instance eval_pord : Proper (pord ==> pord) evalCl.
+  Proof.
+    intros R1 R2 HSub n; induction n; intros t HEv.
+    - rewrite evalCl_simpl in *; split; [rewrite <- HSub; apply HEv | simpl; tauto].
+    - rewrite evalCl_simpl in *; split; [rewrite <- HSub; apply HEv |].
+      intros; apply IHn, HEv, HS; now auto with arith.
+  Qed.
+
+  Definition rel_evalCl : UPred T -m> UPred T := m[(evalCl)].
+
+End EvaluationClosure.
+
+Require Fin.
+
+Definition transfer {A} {T : A -> Type} {x y : A} (EQ : x = y) (t : T x) : T y :=
+  eq_rect x T t y EQ.
+
+Definition transfer_nat_eq {T : nat -> Type} (x : nat) (EQ : x = x) (t : T x) :
+  transfer EQ t = t.
+Proof.
+  symmetry; apply D.eq_rect_eq.
+Qed.
+
+Section FiniteProducts.
+  Context {T : cmtyp}.
+
+  Definition FinI n := forall i : Fin.t n, T.
+
+  (* Type context extension *)
+  Definition extFinI {n} (RC : FinI n) (R : T) : FinI (S n) :=
+    fun i =>  match i in Fin.t k return (match k with
+                                             O => False
+                                           | S m => FinI m -> T end) with
+                | Fin.F1 n => fun _ => R
+                | Fin.FS n i => fun RC => RC i
+              end RC.
+
+  Global Instance extFinI_equiv n : Proper (equiv ==> equiv ==> equiv) (@extFinI n).
+  Proof.
+    intros RC1 RC2 EQRC R1 R2 EQR i.
+    refine (match i as i in Fin.t k return match k return Fin.t k -> Prop with
+                                               O => fun _ => False
+                                             | S m => fun i => forall (RC1 RC2 : FinI m),
+                                                                 RC1 == RC2 ->
+                                                                 extFinI RC1 R1 i == extFinI RC2 R2 i
+                                           end i with
+                Fin.F1 n => fun _ _ _ => EQR
+              | Fin.FS n i => fun RC1 RC2 EQRC => EQRC i
+            end RC1 RC2 EQRC).
+  Qed.
+
+  Global Instance extTC_dist n k : Proper (dist k ==> dist k ==> dist k) (@extFinI n).
+  Proof.
+    intros RC1 RC2 EQRC R1 R2 EQR i.
+    refine (match i as i in Fin.t m return match m return Fin.t m -> Prop with
+                                               O => fun _ => False
+                                             | S m => fun i => forall (RC1 RC2 : FinI m),
+                                                               RC1 = k = RC2 ->
+                                                               extFinI RC1 R1 i = k = extFinI RC2 R2 i
+                                           end i with
+                Fin.F1 n => fun _ _ _ => EQR
+              | Fin.FS n i => fun RC1 RC2 EQRC => EQRC i
+            end RC1 RC2 EQRC).
+  Qed.
+
+  Fixpoint fin_sum_split {k n} (x : Fin.t (k + n)) : Fin.t k + Fin.t n :=
+    match k return Fin.t (k + n) -> Fin.t k + Fin.t n with
+      | 0 => fun x => inr x
+      | S k => fun x =>
+                 match x in Fin.t m return m = S k + n -> Fin.t (S k) + Fin.t n with
+                   | Fin.F1 _ => fun _ => inl Fin.F1
+                   | Fin.FS m x' => fun EQ =>
+                                      match fin_sum_split (transfer (eq_add_S _ _ EQ) x') with
+                                        | inl y => inl (Fin.FS y)
+                                        | inr y => inr y
+                                      end
+                 end eq_refl
+    end x.
+
+  Definition extFinEnv {k n} (η : FinI k) (ρ : FinI n) : FinI (n + k) :=
+    fun x => match fin_sum_split x with
+               | inl y => ρ y
+               | inr y => η y
+             end.
+
+  Global Instance extFinEnv_equiv k n :
+    Proper (equiv ==> equiv ==> equiv) (@extFinEnv k n).
+  Proof.
+    intros η1 η2 EQη ρ1 ρ2 EQρ x; unfold extFinEnv.
+    destruct (fin_sum_split x) as [y | y]; [apply EQρ | apply EQη].
+  Qed.
+
+  Global Instance extFinEnv_dist k m n :
+    Proper (dist n ==> dist n ==> dist n) (@extFinEnv k m).
+  Proof.
+    intros η1 η2 EQη ρ1 ρ2 EQρ x; simpl; unfold extFinEnv.
+    destruct (fin_sum_split x) as [y | y]; [apply EQρ | apply EQη].
+  Qed.
+
+  Definition empFinI : FinI 0 :=
+    fun x => match x in Fin.t k return match k with
+                                         | O => T
+                                         | S n => True
+                                       end with
+               | Fin.F1 _ => I
+               | Fin.FS _ _ => I
+             end.
+
+  Lemma FinI_invert_O (ρ : FinI 0) :
+    ρ == empFinI.
+  Proof.
+    intros x; inversion x.
+  Qed.
+
+  Lemma extFinEnv_empR k (η : FinI k) : extFinEnv η empFinI == η.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Definition FinI_tail {k} (ρ : FinI (S k)) : FinI k :=
+    fun x => ρ (Fin.FS x).
+
+  Lemma FinI_invert_S {k} (ρ : FinI (S k)) :
+    ρ == extFinI (FinI_tail ρ) (ρ Fin.F1).
+  Proof.
+    intros x.
+    refine (match x as x in Fin.t m return
+                  match m return Fin.t m -> Prop with
+                    | O => fun _ => False
+                    | S n => fun x => forall (ρ : FinI (S n)),
+                                      ρ x == extFinI (FinI_tail ρ) (ρ Fin.F1) x
+                  end x with
+              | Fin.F1 m => _
+              | Fin.FS m y => _
+            end ρ); intros.
+    - simpl; reflexivity.
+    - unfold FinI_tail; simpl.
+      reflexivity.
+  Qed.
+
+  Lemma extFin_env_one {k m} (η : FinI k) (ρ : FinI m) R :
+    extFinI (extFinEnv η ρ) R == extFinEnv η (extFinI ρ R).
+  Proof.
+    intros x.
+    refine (match x as x in Fin.t i return
+                  match i return Fin.t i -> Prop with
+                    | O => fun _ => False
+                    | S i => fun x => forall m k (η : FinI k) (ρ : FinI m)
+                                             (HEq : S i = S m + k),
+                                        extFinI (extFinEnv η ρ) R (transfer HEq x) ==
+                                        extFinEnv η (extFinI ρ R) (transfer HEq x)
+                  end x with
+              | Fin.F1 n => fun m k η ρ EQ => _
+              | Fin.FS n x => fun m k η ρ EQ => _
+            end m k η ρ eq_refl).
+    - simpl in EQ; assert (EQ' := eq_add_S _ _ EQ); subst n.
+      rewrite !transfer_nat_eq.
+      unfold extFinEnv; simpl.
+      reflexivity.
+    - simpl in EQ; assert (EQ' := eq_add_S _ _ EQ); subst n.
+      rewrite transfer_nat_eq; clear EQ.
+      unfold extFinEnv; simpl.
+      destruct (fin_sum_split x0); simpl; reflexivity.
+  Qed.
+
+  Lemma extFinI_eq {n m} R (η : FinI m) (EQ : m = n) :
+    extFinI (transfer EQ η) R = transfer (eq_S _ _ EQ) (extFinI η R).
+  Proof.
+    subst n; rewrite transfer_nat_eq; reflexivity.
+  Qed.
+
+  (* TODO: make it so this thing works as an instance, and the casts are less horrible *)
+  Instance transfer_FinI_equiv n m (EQ : n = m) : Proper (equiv ==> equiv) (transfer (T := FinI) EQ).
+  Proof.
+    intros η1 η2 EQη; subst n; rewrite transfer_nat_eq; assumption.
+  Qed.
+
+  Lemma of_nat_lt_ext {n k} (HLt1 HLt2 : n < k) :
+    Fin.of_nat_lt HLt1 = Fin.of_nat_lt HLt2.
+  Proof.
+    revert n HLt1 HLt2; induction k; intros; [inversion HLt1 |].
+    destruct n as [| n]; simpl; [reflexivity |].
+    f_equal; apply IHk.
+  Qed.
+
+  Lemma fin_split_left {n m k}
+        (HLt : n < m) (HLt2 : n < m + k) :
+    fin_sum_split (Fin.of_nat_lt HLt2) = inl (Fin.of_nat_lt HLt).
+  Proof.
+    revert n HLt HLt2; induction m; intros; [inversion HLt |].
+    destruct n as [| n]; simpl in *.
+    - eexists; reflexivity.
+    - erewrite IHm; reflexivity.
+  Qed.
+
+  Lemma fin_split_right {n m k}
+        (HLt : n < k) (HLt2 : m + n < m + k) :
+    fin_sum_split (Fin.of_nat_lt HLt2) = inr (Fin.of_nat_lt HLt).
+  Proof.
+    induction m; intros; simpl in *; [f_equal; apply of_nat_lt_ext |].
+    erewrite IHm; reflexivity.
+  Qed.
+
+  Lemma extFinEnv_lookup_left {n m k} (η : FinI k) (ρ : FinI m)
+        (HLt : n < m) (HLt2 : n < m + k) :
+    extFinEnv η ρ (Fin.of_nat_lt HLt2) == ρ (Fin.of_nat_lt HLt).
+  Proof.
+    unfold extFinEnv.
+    erewrite fin_split_left; reflexivity.
+  Qed.
+
+  Lemma minus_le_lt {k m n} (HGe : m <= n) (HLt : n < m + k) :
+    n - m < k.
+  Proof.
+    apply Plus.plus_lt_reg_l with m.
+    replace (m + (n - m)) with n by auto with arith; assumption.
+  Qed.
+
+  Lemma extFinEnv_lookup_right {k m n} (η : FinI k) (ρ : FinI m)
+        (HGe : m <= n) (HLt : n < m + k) :
+    extFinEnv η ρ (Fin.of_nat_lt HLt) == η (Fin.of_nat_lt (minus_le_lt HGe HLt)).
+  Proof.
+    generalize (minus_le_lt HGe HLt) as HL'; intros.
+    revert HLt; pattern n at 1 2; replace n with (m + (n - m)) by auto with arith; intros.
+    unfold extFinEnv; erewrite fin_split_right; reflexivity.
+  Qed.
+
+  Lemma extFinEnv_lookup_right_sum {n m k} (η : FinI k) (ρ : FinI m)
+        (HLt : n < k) (HLt2 : m + n < m + k) :
+    extFinEnv η ρ (Fin.of_nat_lt HLt2) == η (Fin.of_nat_lt HLt).
+  Proof.
+    unfold extFinEnv.
+    erewrite fin_split_right; reflexivity.
+  Qed.
+
+  Lemma transfer_lookup {m n k} (η : FinI m) (EQ : m = n) (LT : k < n) :
+    transfer EQ η (Fin.of_nat_lt LT) = η (Fin.of_nat_lt (transfer (eq_sym EQ) LT)).
+  Proof.
+    subst; rewrite !transfer_nat_eq; reflexivity.
+  Qed.
+
+End FiniteProducts.
+
+Global Arguments FinI : default implicits.

lib/recdom/Makefile

+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.4pl3     ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -R . RecDom BI.v CBUltInst.v CSetoid.v Constr.v Finmap.v MetricCore.v MetricRec.v PCBUltInst.v PCM.v Predom.v PreoMet.v TOTInst.v UPred.v -o Makefile 
+#
+
+.DEFAULT_GOAL := all
+
+# 
+# This Makefile may take arguments passed as environment variables:
+# COQBIN to specify the directory where Coq binaries resides;
+# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
+# DSTROOT to specify a prefix to install path.
+
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+endef
+includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
+$(call includecmdwithout@,$(COQBIN)coqtop -config)
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+COQLIBS?= -R . RecDom
+COQDOCLIBS?=-R . RecDom
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+
+OPT?=
+COQDEP?=$(COQBIN)coqdep -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?=$(COQBIN)coqc
+GALLINA?=$(COQBIN)gallina
+COQDOC?=$(COQBIN)coqdoc
+COQCHK?=$(COQBIN)coqchk
+
+##################
+#                #
+# Install Paths. #
+#                #
+##################
+
+ifdef USERINSTALL
+XDG_DATA_HOME?=$(HOME)/.local/share
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL=${COQLIB}user-contrib
+COQDOCINSTALL=${DOCDIR}user-contrib
+endif
+
+######################
+#                    #
+# Files dispatching. #
+#                    #
+######################
+
+VFILES:=BI.v\
+  CBUltInst.v\
+  CSetoid.v\
+  Constr.v\
+  Finmap.v\
+  MetricCore.v\
+  MetricRec.v\
+  PCBUltInst.v\
+  PCM.v\
+  Predom.v\
+  PreoMet.v\
+  TOTInst.v\
+  UPred.v
+
+-include $(addsuffix .d,$(VFILES))
+.SECONDARY: $(addsuffix .d,$(VFILES))
+
+VOFILES:=$(VFILES:.v=.vo)
+GLOBFILES:=$(VFILES:.v=.glob)
+VIFILES:=$(VFILES:.v=.vi)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+#                                     #
+# Definition of the toplevel targets. #
+#                                     #
+#######################################
+
+all: $(VOFILES) 
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+validate: $(VOFILES)
+	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
+
+beautify: $(VFILES:=.beautified)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+
+.PHONY: all opt byte archclean clean install userinstall depend html validate
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+userinstall:
+	+$(MAKE) USERINSTALL=true install
+
+install:
+	for i in $(VOFILES); do \
+	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i`; \
+	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/RecDom/$$i; \
+	done
+
+install-doc:
+	install -d $(DSTROOT)$(COQDOCINSTALL)/RecDom/html
+	for i in html/*; do \
+	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/RecDom/$$i;\
+	done
+
+clean:
+	rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
+	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
+	- rm -rf html mlihtml
+
+archclean:
+	rm -f *.cmx *.o
+
+printenv:
+	@$(COQBIN)coqtop -config
+	@echo CAMLC =	$(CAMLC)
+	@echo CAMLOPTC =	$(CAMLOPTC)
+	@echo PP =	$(PP)
+	@echo COQFLAGS =	$(COQFLAGS)
+	@echo COQLIBINSTALL =	$(COQLIBINSTALL)
+	@echo COQDOCINSTALL =	$(COQDOCINSTALL)
+
+###################
+#                 #
+# Implicit rules. #
+#                 #
+###################
+
+%.vo %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+%.vi: %.v
+	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+%.g: %.v
+	$(GALLINA) $<
+
+%.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+%.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+%.g.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+%.g.html: %.v %.glob
+	$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@
+
+%.v.d: %.v
+	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+%.v.beautified:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+

lib/recdom/PCBUltInst.v

+(** This module provides the proof that PCBUlt, the category of
+    pre-ordered, complete, bisected ultrametric spaces, forms an
+    M-category. *)
+
+Require Import PreoMet.
+Require Import MetricRec.
+
+Module PCBUlt <: MCat.
+  Local Obligation Tactic := intros; resp_set || mono_resp || eauto with typeclass_instances.
+
+  Definition M := pcmtyp.
+  Instance MArr   : BC_morph M := fun U V => pcmFromType (U -m> V).
+  Program Instance MComp  : BC_comp M := fun U V W => lift2m (lift2s pcomp _ _) _ _.
+  Instance MId    : BC_id M := fun T => pid T.
+  Local Instance unit_preo : preoType unit := disc_preo unit.
+  Local Instance unit_pcm  : pcmType unit := disc_pcm unit.
+  Instance MTermO : BC_term M := pcmFromType unit.
+  Program Instance MTermA : BC_terminal M := fun U => m[(const tt)].
+
+  Instance Cat : BaseCat M.
+  Proof.
+    split; intros; intros n; simpl; reflexivity || exact I.
+  Qed.
+
+  Section Limits.
+    Context (T : Tower).
+
+    Definition guard := fun (σ : forall i, tow_objs T i) => forall n, tow_morphs T n (σ (S n)) == σ n.
+    Instance lpg : LimitPreserving guard.
+    Proof.
+      intros σ σc HG n.
+      rewrite !dep_chain_compl.
+      rewrite nonexp_continuous; apply umet_complete_ext; intros k.
+      simpl; apply HG.
+    Qed.
+
+    Program Definition lim_obj : pcmtyp := pcmFromType {σ : forall i, tow_objs T i | guard σ}.
+
+    Definition lim_proj i : lim_obj -m> tow_objs T i := (pcmProjI i ∘ muincl)%pm.
+
+    Program Definition lim_cone : Cone T := mkBaseCone T lim_obj lim_proj _.
+    Next Obligation.
+      intros [σ HG]; simpl; apply HG.
+    Qed.
+
+    Program Definition lim_map (C : Cone T) : (cone_t T C : pcmtyp) -m> (cone_t T lim_cone : pcmtyp) :=
+      m[(fun m => exist _ (fun i => cone_m T C i m) _)].
+    Next Obligation.
+      intros n; simpl.
+      assert (HT := cone_m_com T C n m); apply HT.
+    Qed.
+
+    Lemma AllLimits : Limit T.
+    Proof.
+      refine (mkBaseLimit T lim_cone lim_map _ _).
+      + intros C n x; simpl; reflexivity.
+      + intros C h HCom x n; simpl.
+        specialize (HCom n x); simpl in HCom.
+        symmetry; apply HCom.
+    Qed.
+
+  End Limits.
+End PCBUlt.

lib/recdom/PCM.v

+(** Partial commutative monoids. *)
+
+Require Export Predom.
+Require Import MetricCore.
+Require Import PreoMet.
+
+Class Associative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
+  assoc : forall t1 t2 t3, op t1 (op t2 t3) == op (op t1 t2) t3.
+Class Commutative {T} `{eqT : Setoid T} (op : T -> T -> T) :=
+  comm  : forall t1 t2, op t1 t2 == op t2 t1.
+
+Section Definitions.
+  Context (T : Type).
+  Local Instance eqT : Setoid T | 20000 := discreteType.
+
+  Class PCM_unit := pcm_unit : T.
+  Class PCM_op   := pcm_op : option T -> option T -> option T.
+  Class PCM {TU : PCM_unit} {TOP : PCM_op} :=
+    mkPCM {
+        pcm_op_assoc :> Associative (eqT := discreteType) pcm_op;
+        pcm_op_comm  :> Commutative (eqT := discreteType) pcm_op;
+        pcm_op_unit  :  forall t, pcm_op (Some pcm_unit) t = t;
+        pcm_op_zero  :  forall t, pcm_op None t = None
+      }.
+
+End Definitions.
+
+Notation "1" := (Some (pcm_unit _)) : pcm_scope.
+Notation "0" := None : pcm_scope.
+Notation "p · q" := (pcm_op _ p q) (at level 40, left associativity) : pcm_scope.
+
+Delimit Scope pcm_scope with pcm.
+
+(* PCMs with cartesian products of carriers. *)
+Section Products.
+  Context S T `{pcmS : PCM S, pcmT : PCM T}.
+  Local Open Scope pcm_scope.
+  Local Existing Instance eqT.
+
+  Global Instance pcm_unit_prod : PCM_unit (S * T) := (pcm_unit S, pcm_unit T).
+  Global Instance pcm_op_prod : PCM_op (S * T) :=
+    fun ost1 ost2 =>
+      match ost1, ost2 with
+        | Some (s1, t1), Some (s2, t2) =>
+          match Some s1 · Some s2, Some t1 · Some t2 with
+            | Some sr, Some tr => Some (sr, tr)
+            | _, _ => None
+          end
+        | _, _ => None
+      end.
+  Global Instance pcm_prod : PCM (S * T).
+  Proof.
+    split.
+    - intros [[s1 t1] |]; [| reflexivity].
+      intros [[s2 t2] |]; [| reflexivity].
+      intros [[s3 t3] |];
+        [unfold pcm_op, pcm_op_prod |
+         unfold pcm_op at 1 2, pcm_op_prod;
+           destruct (Some (s1, t1) · Some (s2, t2)) as [[s t] |]; simpl; tauto].
+      assert (HS := assoc (Some s1) (Some s2) (Some s3));
+        assert (HT := assoc (Some t1) (Some t2) (Some t3)).
+      destruct (Some s1 · Some s2) as [s12 |];
+        destruct (Some s2 · Some s3) as [s23 |]; [.. | reflexivity].
+      + destruct (Some t1 · Some t2) as [t12 |];
+        destruct (Some t2 · Some t3) as [t23 |]; [.. | reflexivity].
+        * simpl in HS, HT; rewrite HS, HT; reflexivity.
+        * erewrite comm, pcm_op_zero in HT by eassumption; simpl in HT.
+          rewrite <- HT; destruct (Some s12 · Some s3); reflexivity.
+        * erewrite pcm_op_zero in HT by eassumption; simpl in HT.
+          rewrite HT; destruct (Some s1 · Some s23); reflexivity.
+      + erewrite comm, pcm_op_zero in HS by eassumption; simpl in HS.
+        destruct (Some t1 · Some t2) as [t12 |]; [| reflexivity].
+        rewrite <- HS; reflexivity.
+      + erewrite pcm_op_zero in HS by eassumption; simpl in HS.
+        destruct (Some t2 · Some t3) as [t23 |]; [| reflexivity].
+        rewrite HS; reflexivity.
+    - intros [[s1 t1] |] [[s2 t2] |]; try reflexivity; []; simpl; unfold pcm_op, pcm_op_prod.
+      rewrite (comm (Some s1)); assert (HT := comm (Some t1) (Some t2)).
+      simpl in HT; rewrite HT; reflexivity.
+    - intros [[s t] |]; [| reflexivity]; unfold pcm_op, pcm_op_prod; simpl.
+      erewrite !pcm_op_unit by eassumption; reflexivity.
+    - intros st; reflexivity.
+  Qed.
+
+End Products.
+
+Section Order.
+  Context T `{pcmT : PCM T}.
+  Local Open Scope pcm_scope.
+  Local Existing Instance eqT.
+
+  Definition pcm_ord (t1 t2 : T) :=
+    exists ot, ot · Some t1 = Some t2.
+
+  Global Program Instance PCM_preo : preoType T := mkPOType pcm_ord.
+  Next Obligation.
+    split.
+    - intros x; exists 1; eapply pcm_op_unit; assumption.
+    - intros z yz xyz [y Hyz] [x Hxyz]; exists (x · y).
+      rewrite <- assoc; congruence.
+  Qed.
+
+  Local Existing Instance option_preo_top.
+
+  Global Instance prod_ord : Proper (pord ==> pord ==> pord) (pcm_op _).
+  Proof.
+    intros x1 x2 EQx y1 y2 EQy.
+    destruct x2 as [x2 |]; [| erewrite pcm_op_zero by eassumption; exact I].
+    destruct x1 as [x1 |]; [| contradiction]; destruct EQx as [x EQx].
+    destruct y2 as [y2 |]; [| erewrite (comm (Some x2)), pcm_op_zero by eassumption; exact I].
+    destruct y1 as [y1 |]; [| contradiction]; destruct EQy as [y EQy].
+    destruct (Some x2 · Some y2) as [xy2 |] eqn: EQxy2; [| exact I].
+    destruct (Some x1 · Some y1) as [xy1 |] eqn: EQxy1.
+    - exists (x · y); rewrite <- EQxy1.
+      rewrite <- assoc, (comm y), <- assoc, assoc, (comm (Some y1)); congruence.
+    - rewrite <- EQx, <- EQy in EQxy2.
+      rewrite <- assoc, (assoc (Some x1)), (comm (Some x1)), <- assoc in EQxy2.
+      erewrite EQxy1, (comm y), comm, !pcm_op_zero in EQxy2 by eassumption.
+      discriminate.
+  Qed.
+
+End Order.
+
+(* Package of a monoid as a module type (for use with other modules). *)
+Module Type PCM_T.
+
+  Parameter res : Type.
+  Declare Instance res_op : PCM_op res.
+  Declare Instance res_unit : PCM_unit res.
+  Declare Instance res_pcm : PCM res.
+
+End PCM_T.

lib/recdom/UPred.v

+Require Export PreoMet.
+
+Section Definitions.
+  Context {T} {pT : preoType T}.
+
+  Program Definition uniform (p : nat -> T -> Prop) :=
+    forall n m (t1 t2 : T) (HLe : m <= n) (HSub : t1 ⊑ t2), p n t1 -> p m t2.
+
+  Record UPred :=
+    mkUPred {pred     :> nat -> T -> Prop;
+             uni_pred :  uniform pred }.
+
+  Program Definition up_cr (p : T -> Prop) {HP : Proper (pord ==> impl) p}:=
+    mkUPred (fun n t => p t) _.
+  Next Obligation. intros m n t1 t2 _ HT; simpl; rewrite HT; tauto. Qed.
+
+  Definition up_equiv (p q : UPred) := forall n t, p n t == q n t.
+
+  Global Program Instance up_type : Setoid UPred := mkType up_equiv.
+  Next Obligation.
+    split.
+    - intros p n t; reflexivity.
+    - intros p q Hpq n t; symmetry; apply Hpq.
+    - intros p q r Hpq Hqr n t; etransitivity; [apply Hpq | apply Hqr].
+  Qed.
+
+  Definition up_dist n (p q : UPred) :=
+    forall m t, m < n -> (p m t <-> q m t).
+
+  Global Program Instance up_metric : metric UPred := mkMetr up_dist.
+  Next Obligation.
+    intros p q Hpq r s Hrs; split; intros HD m t HLt; [symmetry in Hpq, Hrs |];
+    rewrite (Hpq m t), (Hrs m t); apply HD; assumption.
+  Qed.
+  Next Obligation.
+    split; intros HEq.
+    - intros n t; apply (HEq (S n)); auto with arith.
+    - intros _ m t _; apply HEq.
+  Qed.
+  Next Obligation.
+    intros p q Hpq m t HLt; symmetry; apply Hpq, HLt.    
+  Qed.
+  Next Obligation.
+    intros p q r Hpq Hqr m t HLt; etransitivity; [apply Hpq, HLt | apply Hqr, HLt].
+  Qed.
+  Next Obligation.
+    intros m t HLt; apply H; auto with arith.    
+  Qed.
+  Next Obligation.
+    intros m t HLt; inversion HLt.    
+  Qed.
+
+  Program Definition up_compl (σ : chain UPred) (σc : cchain σ) :=
+    mkUPred (fun n t => σ (S n) n t) _.
+  Next Obligation.
+    intros n m t1 t2 HLt HSub HCn.
+    eapply (chain_cauchy σ σc (S m) (S n)); auto with arith; [].
+    eapply uni_pred; eassumption.
+  Qed.
+
+  Global Program Instance up_cmetric : cmetric UPred := mkCMetr up_compl.
+  Next Obligation.
+    intros n; exists n; intros i HLe k t HLt; simpl.
+    eapply (chain_cauchy σ σc (S k)); eauto with arith.
+  Qed.
+
+  Definition up_ord (p q : UPred) := forall n t, p n t -> q n t.
+
+  Global Program Instance up_preotype : preoType UPred := mkPOType up_ord.
+  Next Obligation.
+    split.
+    + intros p n t; tauto.
+    + intros p q r Hpq Hqr n t Hp; apply Hqr, Hpq, Hp.
+  Qed.
+
+  Global Instance up_pcmetric : pcmType UPred.
+  Proof.
+    split.
+    + intros p q Hpq r s Hrs; split; intros Hpr n t Hq;
+      apply Hrs, Hpr, Hpq, Hq.
+    + intros σ ρ σc ρc HSub n t Hpc; simpl in *; apply HSub, Hpc.
+  Qed.
+
+  Global Instance upred_equiv : Proper (equiv ==> eq ==> eq ==> iff) pred.
+  Proof.
+    add_morphism_tactic; intros R1 R2 EQR n t; split; intros HH; apply EQR; assumption.
+  Qed.
+
+  Global Instance upred_pord : Proper (pord ==> le --> pord ==> impl) pred.
+  Proof.
+    intros R1 R2 SubR n1 n2 Len t1 t2 Subt HR1; eapply SubR, uni_pred; eassumption.
+  Qed.
+
+  Definition laterF (p : nat -> T -> Prop) n t :=
+    match n with
+      | O => True
+      | S n => p n t
+    end.
+  Program Definition later_up (p : UPred) :=
+    mkUPred (laterF p) _.
+  Next Obligation.
+    intros [| m] [| n] t1 t2 HLe HSubt; simpl; try tauto; [now inversion HLe |].
+    intros HP; eapply uni_pred; [| eassumption | eassumption]; auto with arith.
+  Qed.
+
+  Global Instance later_up_equiv : Proper (equiv ==> equiv) later_up.
+  Proof.
+    intros P Q EQPQ [| n] t; simpl; [reflexivity | apply EQPQ].
+  Qed.
+
+  Global Instance later_up_dist n : Proper (dist n ==> dist n) later_up.
+  Proof.
+    intros P Q EQPQ [| k] t HLt; simpl; [reflexivity | apply EQPQ; auto with arith].
+  Qed.
+
+  Lemma equiv_upred_simpl U (R : relation U) (f : U -> UPred) {RS : Symmetric R}
+        (HP : forall u1 u2 n t, R u1 u2 -> f u1 n t -> f u2 n t) :
+    Proper (R ==> equiv) f.
+  Proof.
+    intros u1 u2 HRu; split; intros HF; (eapply HP; [| eassumption]);
+    [| symmetry]; assumption.
+  Qed.
+  Lemma dist_upred_simpl U (R : relation U) (f : U -> UPred) n {RS : Symmetric R}
+        (HP : forall u1 u2 m t (HLt : m < n), R u1 u2 -> f u1 m t -> f u2 m t) :
+    Proper (R ==> dist n) f.
+  Proof.
+    intros u1 u2 HRu m t HLt; split; intros HF;
+    (eapply HP; [eassumption | | eassumption]); [| symmetry]; assumption.
+  Qed.
+
+  Global Instance const_resp P : Proper (pord (T := T) ==> impl) (const P).
+  Proof. add_morphism_tactic; unfold impl; unfold const; tauto. Qed.
+
+End Definitions.
+
+Global Arguments UPred T {pT}.
+Notation "▹ p" := (later_up p) (at level 20) : upred_scope.
+
+Section Products.
+  Context {R S} {pR : preoType R} {pS : preoType S}.
+
+  Program Definition prod_up (p : UPred R) (q : UPred S) : UPred (R * S) :=
+    mkUPred (fun n rs => p n (fst rs) /\ q n (snd rs)) _.
+  Next Obligation.
+    intros n m [r1 s1] [r2 s2] HLe [Subr Subs] [HP HQ]; simpl in HP, HQ.
+    simpl; split; [rewrite <- Subr | rewrite <- Subs]; rewrite HLe; assumption.
+  Qed.
+
+  Global Instance prod_up_equiv : Proper (equiv ==> equiv ==> equiv) prod_up.
+  Proof.
+    intros p1 p2 EQp q1 q2 EQq n [r s]; simpl.
+    rewrite EQp, EQq; tauto.
+  Qed.
+  Global Instance prod_up_dist n : Proper (dist n ==> dist n ==> dist n) prod_up.
+  Proof.
+    intros p1 p2 EQp q1 q2 EQq m [r s] HLt; simpl.
+    split; intros [HP HQ]; (split; [apply EQp | apply EQq]); assumption.
+  Qed.
+  Global Instance prod_up_pord : Proper (pord ==> pord ==> pord) prod_up.
+  Proof.
+    intros p1 p2 Subp q1 q2 Subq n [r s]; simpl; intros [HP HQ].
+    split; [apply Subp | apply Subq]; assumption.
+  Qed.
+
+End Products.
+
+Notation "p × q" := (prod_up p q) (at level 40, left associativity) : upred_scope.
+Delimit Scope upred_scope with up.
+
+Section Closures.
+  Context {T} `{pcmT : pcmType T} {R} `{poT : preoType R} (P : T -> Prop) (Q : T -> UPred R).
+  Local Obligation Tactic := intros.
+
+  Program Definition all_cl : UPred R :=
+    mkUPred (fun n r => forall t (HP : P t), Q t n r) _.
+  Next Obligation.
+    intros n m r1 r2 HLe HSubr HQ t' HP.
+    rewrite <- HSubr, HLe; apply HQ, HP.
+  Qed.
+
+  Program Definition xist_cl : UPred R :=
+    mkUPred (fun n r => exists t, P t /\ Q t n r) _.
+  Next Obligation.
+    intros n m r1 r2 HLe HSubr [t' [HP HQ]].
+    exists t'; split; [assumption |].
+    rewrite HLe, <- HSubr; apply HQ.
+  Qed.
+
+End Closures.
+
+Notation "∀ w ∈ P , Q" := (all_cl P (fun w => Q)) (at level 60, w at level 30, P, Q at next level) : upred_scope.
+Notation "∃ w ∈ P , Q" := (xist_cl P (fun w => Q)) (at level 60, w at level 30, P, Q at next level) : upred_scope.