From 2ac8887921fbac592b820acda0227076ebab3191 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Jan 2015 22:20:50 +0100
Subject: [PATCH] start writing a signature for the world-prop solution

---
 world_prop_sig.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 world_prop_sig.v

diff --git a/world_prop_sig.v b/world_prop_sig.v
new file mode 100644
index 000000000..deeb1af39
--- /dev/null
+++ b/world_prop_sig.v
@@ -0,0 +1,44 @@
+(* For some reason, the order matters. We cannot import Constr last. *)
+Require Import ModuRes.Finmap ModuRes.Constr ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet.
+
+
+Module Type WorldPropSig (Res : PCM_T).
+
+  (** The construction is parametric in the monoid we choose *)
+  Import Res.
+
+  (* The functor is fixed *)
+  Section Definitions.
+    (** We'll be working with complete metric spaces, so whenever
+        something needs an additional preorder, we'll just take a
+        discrete one. *)
+    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 FProp P `{cmP : cmetric P} :=
+      (nat -f> P) -m> UPred res.
+  End Definitions.
+
+  Parameter PreProp  : Type.
+  Parameter PrePropS : Setoid PreProp.
+  Parameter PrePropM : metric PreProp.
+  Parameter PrePropCM: cmetric PreProp.
+  
+  Definition Props     := FProp PreProp.
+  Parameter PropS      : Setoid Props.
+  Parameter PropM      : metric Props.
+  Parameter PropCM     : cmetric Props.
+  
+  Definition Wld     := (nat -f> PreProp).
+
+  Parameter ı  : PreProp -> halve (cmfromType Props).
+  Parameter ı' : halve (cmfromType Props) -> PreProp.
+
+  Axiom iso : forall P, ı' (ı P) == P.
+  Axiom isoR : forall T, ı (ı' T) == T.
+
+(*Parameter PProp_preo : preoType PreProp.
+  Parameter PProp_pcm  : pcmType PreProp.
+  Parameter PProp_ext  : extensible PreProp.*)
+
+End WorldPropSig.
-- 
GitLab