From 332b89cee5fe6c660f1432ffe7b78d7ed771fe42 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 Mar 2015 14:26:11 +0100
Subject: [PATCH] define a "halve" type; make world_prop no longer depend on
 CatBasics

This means that bundled types are *not* visible to the Iris logic itself!
---
 iris_plog.v              | 17 ++++----
 iris_vs_rules.v          | 21 ++++-----
 lib/ModuRes/CBUltInst.v  | 34 +++++++++------
 lib/ModuRes/CatBasics.v  | 61 ++++----------------------
 lib/ModuRes/MetricCore.v | 93 +++++++++++++++++++++++++++++++++++++++-
 lib/ModuRes/Predom.v     |  3 +-
 world_prop.v             | 21 ++++-----
 world_prop_recdom.v      | 17 ++++----
 8 files changed, 161 insertions(+), 106 deletions(-)

diff --git a/iris_plog.v b/iris_plog.v
index 92957efa2..66727a9d5 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -23,7 +23,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     (** Invariants **)
     Definition invP i P w : UPred res :=
-      intEq (w i) (Some (ı' P)) w.
+      intEq (w i) (Some (ı' (halved P))) w.
     Program Definition inv i : Props -n> Props :=
       n[(fun P => m[(invP i P)])].
     Next Obligation.
@@ -41,7 +41,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
     Qed.
     Next Obligation.
       intros p1 p2 EQp w; unfold invP.
-      cut ((w i === Some (ı' p1)) = n = (w i === Some (ı' p2))).
+      cut ((w i === Some (ı' (halved p1))) = n = (w i === Some (ı' (halved p2)))).
       { intros Heq. now eapply Heq. }
       eapply met_morph_nonexp.
       now eapply dist_mono, (met_morph_nonexp ı').
@@ -120,7 +120,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
                       /\ forall i (Hm : m i),
                            (i ∈ dom rs <-> i ∈ dom w) /\
                            forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
-                             ı π w n ri) _).
+                             (unhalved (ı π)) w n ri) _).
     Next Obligation.
       intros n1 n2 _ _ HLe _ [rs [HLS HRS] ]. exists rs; split; [assumption|].
       setoid_rewrite HLe; eassumption.
@@ -146,15 +146,16 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
         assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
         destruct (w1 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp (ı π')) in EQw; apply EQw; [omega |].
+        apply ı in EQπ. apply halve_eq in EQπ.
+        apply EQÏ€; [now auto with arith |].
+        apply (met_morph_nonexp (unhalved (ı π'))) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
       - split; [assumption | split; [rewrite (domeq EQw); apply HM, Hm |] ].
         intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
         assert (EQÏ€ := EQw i); rewrite-> HLw in EQÏ€; clear HLw.
-        destruct (w2 i) as [Ï€' |]; [| contradiction]; do 3 red in EQÏ€.
-        apply ı in EQπ; apply EQπ; [now auto with arith |].
-        apply (met_morph_nonexp (ı π')) in EQw; apply EQw; [omega |].
+        destruct (w2 i) as [Ï€' |]; [| contradiction]. do 3 red in EQÏ€.
+        apply ı in EQπ. apply halve_eq in EQπ. apply EQπ; [now auto with arith |].
+        apply (met_morph_nonexp (unhalved (ı π'))) in EQw; apply EQw; [omega |].
         apply HR; [reflexivity | assumption].
     Qed.
 
diff --git a/iris_vs_rules.v b/iris_vs_rules.v
index b12434f14..2d4b90f2e 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -29,11 +29,9 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       (inv i P) ⊑ pvs (mask_sing i) mask_emp (▹P).
     Proof.
       intros w n r HInv w'; intros.
-      change (match w i with Some x => x = S n = ı' P | None => False end) in HInv.
+      change (match w i with Some x => x = S n = ı' (halved P) | None => False end) in HInv.
       destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite ->(isoR P) in HInv.
-      (* get rid of the invisible 1/2 *)
-      do 8 red in HInv.
+      apply ı in HInv; rewrite ->(isoR (halved P)) in HInv.
       destruct HE as [rs [HE HM] ].
       destruct (rs i) as [ri |] eqn: HLr.
       - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
@@ -41,7 +39,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         exists w' (r · ri).
         split; [reflexivity |].
         split.
-        + simpl; eapply HInv; [now auto with arith |].
+        + simpl. apply halve_eq in HInv. eapply HInv; [now auto with arith |].
           eapply uni_pred, HM with i;
             [| exists r | | | rewrite HLr]; try reflexivity.
           * left; unfold mask_sing, mask_set.
@@ -64,11 +62,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       (inv i P ∧ ▹P) ⊑ pvs mask_emp (mask_sing i) ⊤.
     Proof.
       intros w n r [HInv HP] w'; intros.
-      change (match w i with Some x => x = S n = ı' P | None => False end) in HInv.
+      change (match w i with Some x => x = S n = ı' (halved P) | None => False end) in HInv.
       destruct (w i) as [μ |] eqn: HLu; [| contradiction].
-      apply ı in HInv; rewrite ->(isoR P) in HInv.
-      (* get rid of the invisible 1/2 *)
-      do 8 red in HInv.
+      apply ı in HInv; rewrite ->(isoR (halved P)) in HInv.
+      apply halve_eq in HInv.
       destruct HE as [rs [HE HM] ].
       exists w' 1; split; [reflexivity | split; [exact I |] ].
       rewrite ->(comm r), <-assoc in HE.
@@ -226,13 +223,13 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
       destruct n as [| n]; [now inversion HLe | simpl in HP].
       rewrite ->HSub in HP; clear w HSub; rename w' into w.
       destruct (fresh_region w m HInf) as [i [Hm HLi] ].
-      assert (HSub : w ⊑ fdUpdate i (ı' P) w).
+      assert (HSub : w ⊑ fdUpdate i (ı' (halved P)) w).
       { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
         now rewrite ->fdUpdate_neq by assumption.
       }
-      exists (fdUpdate i (ı' P) w) 1; split; [assumption | split].
+      exists (fdUpdate i (ı' (halved P)) w) 1; split; [assumption | split].
       - exists (exist _ i Hm).
-        change (((fdUpdate i (ı' P) w) i) = S (S k) = (Some (ı' P))).
+        change (((fdUpdate i (ı' (halved P)) w) i) = S (S k) = (Some (ı' (halved P)))).
         rewrite fdUpdate_eq; reflexivity.
       - erewrite ra_op_unit by apply _.
         destruct HE as [rs [HE HM] ].
diff --git a/lib/ModuRes/CBUltInst.v b/lib/ModuRes/CBUltInst.v
index 1225ffc3b..c452cd82b 100644
--- a/lib/ModuRes/CBUltInst.v
+++ b/lib/ModuRes/CBUltInst.v
@@ -64,34 +64,44 @@ 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) _ _) _ _.
+  Definition HF := fun T1 T2 => halveCM (F T1 T2).
+
+  Program Instance halveFMap : BiFMap HF :=
+    fun m1 m2 m3 m4 => lift2m (lift2s (fun (ars: (m2 -t> m1) * (m3 -t> m4)) (ob: halveCM (F m1 m3)) => halvedT (fmorph (F := F) ars (unhalvedT ob))) _ _) _ _.
+  Next Obligation.
+    repeat intro. unfold halvedT, unhalvedT, HF in *. simpl.
+    unhalveT. simpl. rewrite H. reflexivity.
+  Qed.
   Next Obligation.
     intros p1 p2 EQp x; simpl; rewrite EQp; reflexivity.
   Qed.
   Next Obligation.
-    intros e1 e2 EQ; simpl. unhalve.
-    rewrite EQ; reflexivity.
+    intros e1 e2 EQ; simpl. unfold halvedT, unhalvedT, HF in *. unhalveT.
+    destruct n as [|n]; first by exact I.
+    simpl in *. rewrite EQ; reflexivity.
   Qed.
   Next Obligation.
-    intros p1 p2 EQ e; simpl; unhalve.
-    apply dist_mono in EQ.
-    rewrite EQ; reflexivity.
+    intros p1 p2 EQ e; simpl. unfold halvedT, unhalvedT, HF in *. unhalveT.
+    destruct n as [|n]; first by exact I. simpl.
+    apply dist_mono. rewrite EQ. reflexivity.
   Qed.
 
-  Instance halveF : BiFunctor (fun T1 T2 => halve (F T1 T2)).
+  Instance halveF : BiFunctor HF.
   Proof.
     split; intros.
     + intros T; simpl.
+      unfold unhalvedT, HF in *. unhalveT. simpl.
       apply (fmorph_comp _ _ _ _ _ _ _ _ _ _ T).
     + intros T; simpl.
+      unfold unhalvedT, HF in *. unhalveT. 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).
+    contractive (@fmorph _ _ HF _ m0 m1 m2 m3).
   Proof.
     intros n p1 p2 EQ f; simpl.
+    unfold unhalvedT, HF in *. unhalveT. simpl.
     change ((fmorph (F := F) p1) f = n = (fmorph p2) f).
     rewrite EQ; reflexivity.
   Qed.
@@ -109,18 +119,18 @@ Module Type SimplInput(Cat : MCat).
 End SimplInput.
 
 Module InputHalve (S : SimplInput (CBUlt)) : InputType(CBUlt)
-    with Definition F := fun T1 T2 => halve (S.F T1 T2).
+    with Definition F := fun T1 T2 => halveCM (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 F T1 T2 := halveCM (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).
+    umconst (halvedT (S.F_ne tt)).
 
   Definition F_contractive := @halve_contractive S.F _.
 End InputHalve.
diff --git a/lib/ModuRes/CatBasics.v b/lib/ModuRes/CatBasics.v
index f8d8f176e..02126ad50 100644
--- a/lib/ModuRes/CatBasics.v
+++ b/lib/ModuRes/CatBasics.v
@@ -251,63 +251,18 @@ Section IndexedProductsPCM.
 End IndexedProductsPCM.
 
 
-
 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.
+  Definition halveT (T: eqType): eqType := fromType (halve T).
+  Definition halvedT {T}: eqtyp T -> eqtyp (halveT T) := fun h => halved h.
+  Definition unhalvedT {T}: eqtyp (halveT T) -> eqtyp T := fun h => unhalved h.
 
+  Definition halveM (T: Mtyp) : Mtyp := Build_Mtyp (halveT T) halve_metr.
+  Definition halveCM (T: cmtyp): cmtyp := Build_cmtyp (halveM T) halve_cm.
 End Halving.
+Ltac unhalveT := repeat (unhalve || match goal with
+                       | x: eqtyp (mtyp (cmm (halveCM _))) |- _ => destruct x as [x]
+                       end).
 
-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.
 
 (** Trivial extension of a nonexpansive morphism to monotone one on a
     metric space equipped with a trivial preorder. *)
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 59d3c94b3..0b8b1d2ec 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -379,6 +379,97 @@ End MCompP.
 
 Arguments umid T {eqT mT}.
 
+Section Halving.
+  Context {T: Type} `{cmT : cmetric T}.
+
+  CoInductive halve := halved: T -> halve.
+  Definition unhalved (h: halve) := match h with halved t => t end.
+
+  Definition dist_halve n :=
+    match n with
+      | O  => fun _ _ => True
+      | S n => fun h1 h2 => match h1, h2 with halved t1, halved t2 => dist n t1 t2 end
+    end.
+
+  Global Program Instance halve_ty : Setoid halve :=
+    mkType (fun h1 h2 =>  match h1, h2 with halved t1, halved t2 => t1 == t2 end).
+  Next Obligation.
+    split; repeat intro;
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    - reflexivity.
+    - symmetry; assumption.
+    - etransitivity; eassumption.
+  Qed.
+
+  Global Instance unhalve_proper : Proper (equiv ==> equiv) unhalved.
+  Proof.
+    repeat intro. repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    simpl in *. assumption.
+  Qed.
+
+  Global Program Instance halve_metr : metric halve := mkMetr dist_halve.
+  Next Obligation.
+    destruct n; [now resp_set | repeat intro ];
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+    simpl. rewrite H, H0. reflexivity.
+  Qed.
+  Next Obligation.
+    split; intros HEq.
+    - repeat (match goal with [ x : halve |- _ ] => destruct x end).
+      apply dist_refl; intros n; apply (HEq (S n)).
+    - intros [| n]; [exact I |]. simpl.
+      repeat (match goal with [ x : halve |- _ ] => destruct x end).
+      revert n; apply dist_refl, HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 HEq; destruct n; [exact I |].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    symmetry; apply HEq.
+  Qed.
+  Next Obligation.
+    intros t1 t2 t3 HEq12 HEq23; destruct n; [exact I |].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    etransitivity; [apply HEq12 | apply HEq23].
+  Qed.
+  Next Obligation.
+    destruct n; [exact I | ].
+    repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl in *.
+    apply dist_mono, H.
+  Qed.
+
+  Instance halve_chain (σ : chain halve) {σc : cchain σ} : cchain (fun n => unhalved (σ (S n))).
+  Proof.
+    unfold cchain; intros.
+    apply le_n_S in HLei. apply le_n_S in HLej.
+    specialize (chain_cauchy _ σc (S n) (S i) (S j)). simpl. intros Hcauchy.
+    destruct (σ (S i)), (σ (S j)). assumption.
+  Qed.
+
+  Definition compl_halve (σ : chain halve) (σc : cchain σ) : halve :=
+    halved (compl (fun n => unhalved (σ (S n))) (σc := halve_chain σ)).
+
+  Program Definition halve_cm : cmetric halve := 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 |]. unfold compl_halve.
+    apply le_S_n in HLe.
+    specialize (HCon i _). destruct (σ (S i)). simpl. assumption.
+  Qed.
+
+  Global Instance halve_eq n: Proper (dist (S n) ==> dist n) unhalved.
+  Proof.
+    repeat intro. repeat (match goal with [ x : halve |- _ ] => destruct x end). simpl. assumption.
+  Qed.
+End Halving.
+Arguments halve : clear implicits.
+Ltac unhalve := repeat match goal with
+                       | x: halve _ |- _ => destruct x as [x]
+                       | H: halved _ == halved _ |- _ => simpl in H
+                       | H: halved _ = _ = halved _ |- _ => simpl in H
+                       end.
+
+
 (** Single element space and the distance on it. *)
 Program Instance unit_metric : metric unit :=
   mkMetr (fun _ _ _ => True).
@@ -508,7 +599,7 @@ End ChainApps.
 Section NonexpCMetric.
   Context `{cT : cmetric T} `{cU : cmetric U}.
 
-  (** THe set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
+  (** The set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
   Global Program Instance nonexp_cmetric : cmetric (T -n> U) | 5 :=
     mkCMetr fun_lub.
   Next Obligation.
diff --git a/lib/ModuRes/Predom.v b/lib/ModuRes/Predom.v
index 6b12e7737..fe31a3a40 100644
--- a/lib/ModuRes/Predom.v
+++ b/lib/ModuRes/Predom.v
@@ -1,6 +1,5 @@
 Require Import ssreflect.
-Require Export Coq.Program.Program.
-Require Import CSetoid.
+Require Export CSetoid.
 
 Generalizable Variables T U V W.
 
diff --git a/world_prop.v b/world_prop.v
index 8f9f22921..07bd21a46 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -1,13 +1,15 @@
 (** In this file, we we define what it means to be a solution of the recursive
     domain equations to build a higher-order separation logic *)
 Require Import ModuRes.PreoMet ModuRes.Finmap.
-Require Import ModuRes.CatBasics. (* Get the "halve" functor. This brings in bundled types... *)
 Require Import ModuRes.RA ModuRes.UPred.
 
 (* This interface keeps some of the details of the solution opaque *)
 Module Type WORLD_PROP (Res : RA_T).
   (* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
-  Parameter PreProp    : cmtyp.
+  Parameter PreProp    : Type.
+  Declare Instance PProp_t  : Setoid PreProp.
+  Declare Instance PProp_m  : metric PreProp.
+  Declare Instance PProp_cm : cmetric PreProp.
   Instance PProp_preo  : preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm   : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext   : extensible PreProp := disc_ext PreProp.
@@ -17,16 +19,15 @@ Module Type WORLD_PROP (Res : RA_T).
   Definition Props     := Wld -m> UPred (Res.res).
 
   (* Define all the things on Props, so they have names - this shortens the terms later. *)
-  (* TODO: Why again does this not use priority 0? *)
-  Instance Props_ty   : Setoid Props  | 1 := _.
-  Instance Props_m    : metric Props  | 1 := _.
-  Instance Props_cm   : cmetric Props | 1 := _.
-  Instance Props_preo : preoType Props| 1 := _.
-  Instance Props_pcm  : pcmType Props | 1 := _.
+  Instance Props_ty   : Setoid Props  | 0 := _.
+  Instance Props_m    : metric Props  | 0 := _.
+  Instance Props_cm   : cmetric Props | 0 := _.
+  Instance Props_preo : preoType Props| 0 := _.
+  Instance Props_pcm  : pcmType Props | 0 := _.
 
   (* Establish the recursion isomorphism *)
-  Parameter ı  : PreProp -n> halve (cmfromType Props).
-  Parameter ı' : halve (cmfromType Props) -n> PreProp.
+  Parameter ı  : PreProp -n> halve Props.
+  Parameter ı' : halve Props -n> PreProp.
   Axiom iso : forall P, ı' (ı P) == P.
   Axiom isoR: forall T, ı (ı' T) == T.
 End WORLD_PROP.
diff --git a/world_prop_recdom.v b/world_prop_recdom.v
index 36764a1df..11271b1bb 100644
--- a/world_prop_recdom.v
+++ b/world_prop_recdom.v
@@ -63,16 +63,17 @@ Module WorldProp (Res : RA_T) : WORLD_PROP Res.
       the space of worlds. We'll store the actual solutions in the
       worlds, and use the action of the FPropO on them as the space we
       normally work with. *)
-  Definition PreProp := DInfO.
-  Definition Props   := FProp PreProp.
-  Definition Wld     := (nat -f> PreProp).
-
-  (* Define an order on PreProp. *)
+  Definition PreProp : Type := DInfO.
+  Instance PProp_t  : Setoid PreProp := _.
+  Instance PProp_m  : metric PreProp := _.
+  Instance PProp_cm : cmetric PreProp := _.
   Instance PProp_preo: preoType PreProp   := disc_preo PreProp.
   Instance PProp_pcm : pcmType PreProp    := disc_pcm PreProp.
   Instance PProp_ext : extensible PreProp := disc_ext PreProp.
 
-  (* Give names to the things for Props, so the terms can get shorter. *)
+  (* Define worlds and propositions *)
+  Definition Wld     := (nat -f> PreProp).
+  Definition Props   := FProp PreProp.
   Instance Props_ty   : Setoid Props     := _.
   Instance Props_m    : metric Props     := _.
   Instance Props_cm   : cmetric Props    := _.
@@ -80,8 +81,8 @@ Module WorldProp (Res : RA_T) : WORLD_PROP Res.
   Instance Props_pcm  : pcmType Props    := _.
 
   (* Establish the isomorphism *)
-  Definition ı  : PreProp -t> halve (cmfromType Props) := Unfold.
-  Definition ı' : halve (cmfromType Props) -t> PreProp := Fold.
+  Definition ı  : DInfO -t> halveCM (cmfromType Props) := Unfold.
+  Definition ı' : halveCM (cmfromType Props) -t> DInfO := Fold.
 
   Lemma iso P : ı' (ı P) == P.
   Proof. apply (FU_id P). Qed.
-- 
GitLab