The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Even though I came up with all this myself, and it obviously results in the 
expressions I wanted, I'm still not sure I understand how it actually works.  
For example, would there be any way to flatten the definitions to using a 
single 
level of the continuation passing monad?  Also, I'm stuck trying to prove a 
couple simple example properties which I know must be true...

Ultimately, I'd want to convert these definitions to typeclass instances, 
with 
the goal to be able to write things like "open (fun x y:R => x*x + y*y < 1)", 
or eventually "continuous Rplus".

Class Bind (X' X Y:Type) : Type :=
bind : X' -> (X -> Y) -> Y.

Class Return (X Y:Type) : Type :=
return_ : X -> Y.

Class MonadAlgebraSignature (m:Type -> Type) (X:Type) : Type :=
monad_alg_bind :> forall Y:Type, Bind (m Y) Y X.

(*
Instance prod2_algebra (m:Type -> Type) (X Y:Type)
  `{MonadAlgebraSignature m X} `{MonadAlgebraSignature m Y} :
  MonadAlgebraSignature m (X * Y) :=
fun A (a:m A) (f:A -> X * Y) =>
  (bind a (fun a' => fst (f a')), bind a (fun a' => snd (f a'))).

Instance prod_algebra (m:Type -> Type) (X:Type) (P:X->Type)
  `{forall x:X, MonadAlgebraSignature m (P x)} :
  MonadAlgebraSignature m (forall x:X, P x) :=
fun A (a:m A) (f:A -> forall x:X, P x) (x:X) =>
  bind a (fun a' => f a' x).

Instance func_space_algebra (m:Type -> Type) (X Y:Type)
  `{MonadAlgebraSignature m Y} : MonadAlgebraSignature m (X->Y).
*)

Class MonadSignature (m:Type -> Type) : Type := {
  monad_bind :> forall X:Type, MonadAlgebraSignature m (m X);
  monad_return :> forall X:Type, Return X (m X)
}.

Definition continuation (R:Type) : Type -> Type :=
fun X => (X -> R) -> R.

Instance cont_result_monad_alg (R:Type) :
  MonadAlgebraSignature (continuation R) R :=
fun Y y => y.

Instance cont_monad (R:Type) : MonadSignature (continuation R) := {|
  monad_bind := fun X Y (y:continuation R Y) (f:Y -> continuation R X)
    (cont : X -> R) => y (fun y0 => f y0 cont);
  monad_return := fun X (x:X) (cont : X -> R) => cont x
|}.

Notation "x >>= f" := (bind x f) (left associativity, at level 91).
Notation "'do' x0 <- x ; y" := (x >>= (fun x0 => y))
  (right associativity, at level 92, x0 ident).
Notation "x >> y" := (do _ <- x; y) (left associativity, at level 91).

Definition topspace : Type := { X:Type & (X->Prop) -> Prop }.

Require Import List.
Open Scope list_scope.

Fixpoint subset_type (l : list topspace) : Type :=
match l with
| nil => Prop
| (existT X _) :: l' => X -> subset_type l'
end.

(*
Instance subset_type_alg (l : list topspace) :
  MonadAlgebraSignature (continuation Prop) (subset_type l).
induction l as [ | [X Xopen] l' ]; typeclasses eauto.
Defined.
*)

Fixpoint nhd_builder {l:list topspace} :
  continuation Prop (continuation Prop (subset_type l)) -> subset_type l :=
match l with
| nil => fun P => do Q <- P; do R <- Q; R
| (existT X Xopen) :: l' => fun U =>
  fun x:X => nhd_builder (fun cont1 => do U' <- U;
    exists A : X -> Prop, A x /\ Xopen A /\
    cont1 (fun cont2 => do U'' <- U';
    forall x':X, A x' -> cont2 (U'' x')))
end.

Definition multidim_nhd {l:list topspace} : subset_type l -> subset_type l :=
  fun U => nhd_builder (return_ (return_ U)).

Eval compute in (fun X Xopen Y Yopen Z Zopen => @multidim_nhd
  (existT _ X Xopen :: existT _ Y Yopen :: existT _ Z Zopen :: nil)).

Fixpoint open_builder {l:list topspace} :
  subset_type l -> continuation Prop (continuation Prop (subset_type l)) ->
  Prop :=
match l with
| nil => fun P Q =>
    P -> (do Q' <- Q; do Q'' <- Q'; Q'' : Prop)
| existT X Xopen :: l' => fun U V =>
  forall x:X, open_builder (U x) (fun cont1 => do V' <- V;
    exists A : X -> Prop, A x /\ Xopen A /\
    cont1 (fun cont2 => do V'' <- V';
    forall x':X, A x' -> cont2 (V'' x')))
end.

Definition multidim_open {l:list topspace} : subset_type l -> Prop :=
  fun U => open_builder U (return_ (return_ U)).

Eval compute in (fun X Xopen Y Yopen Z Zopen => @multidim_open
  (existT _ X Xopen :: existT _ Y Yopen :: existT _ Z Zopen :: nil)).

Fixpoint contained {l:list topspace} :
  subset_type l -> subset_type l -> Prop :=
match l with
| nil => fun P Q => P -> Q
| existT X Xopen :: l' => fun U V =>
  forall x:X, contained (U x) (V x)
end.

Lemma multidim_nhd_contained (l:list topspace) : forall U:subset_type l,
  contained (multidim_nhd U) U.
Proof.
(*
fun U x y z ... Hnhd => match Hnhd with
| ex_intro A (conj Ax (conj Aopen
 (ex_intro B (conj By (conj Bopen
 (ex_intro C (conj Cz (conj Copen ... Hinc)))))))) =>
  Hinc x Ax y By z Cz ...
end.
*)
admit.
Qed.

Lemma multidim_nhd_open (l:list topspace) : forall U:subset_type l,
  multidim_open (multidim_nhd U).
Proof.
admit.
Qed.