The Coq mailing list

[Andrei Popescu <uuomul AT yahoo.com>]

Dear Coq,

Greetings from Isabelle/HOL! 

I have recently undergone a major category-theory-based surgery at my datatype system (of course without affecting my kernel). Due to inherent limitations of my underlying logic, I still cannot handle dependent datatype families, or inner-nested (co)corecursion such as:

Inductive TermModuloAlpha (A:Type) : Type :=

   | Var : A -> TermModuloAlpha (A)

   | App : TermModuloAlpha (A) -> TermModuloAlpha (A) -> TermModuloAlpha (A)

   | Lam : TermModuloAlpha (Option (A)) -> TermModuloAlpha (A)

But within the HOL fragment I can now model things like:

(1) Outer-nested (co)recursion through (co)datatypes, such as

(1.a) Inductive RoseTree (A:Type) : Type :=

   | Node : List (RoseTree (A)) -> RoseTree (A)

(1.b) Inductive RoseTree (A:Type) : Type :=

   | Node : Stream (RoseTree (A)) -> RoseTree (A)

(1.c) Coinductive RoseTree (A:Type) : Type :=

   | Node : List (RoseTree (A)) -> RoseTree (A)

(2) Outer-nested (co)recursion through (suitably bounded) non-datatypes, such as

Inductive RoseTree (A:Type) : Type :=

   | Node : FiniteSet (RoseTree (A)) -> RoseTree (A)

Now comes my question:  My surgeons are finishing the camera-ready version of an ITP paper on this, and would like to provide an accurate comparison with other systems. How do you model the above situations?  As far as I

understand after glimpsing through your medical records, you can handle (1.a) by (automatically?) reducing the situation to mutual recursion.  However, you cannot directly represent (1.b), (1.c) and (2) -- I may of course be wrong, and this is why I am asking you.  

All the best,

  Isabelle/HOL