The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Ralph is a black belt at this kind of thing, so I suspect his advice is very valuable.

There are a couple of cheap tricks that may work in certain circumstances, though. Here is one:

Context (f : Type -> Type).

Fixpoint foobar_n (n : nat) : Type :=

match n return Type with

 | 0 => False

 | S m => f (foobar_n m)

 end

Definition foobar := { n : nat & foobar_n n}.

If the type function f is very well behaved, you may be able to do something with (foobar f). I've used it successfully in the case where f is a monotone functional with reasonable properties.

Best,

Cody

On Tue, Jul 3, 2018 at 5:06 PM, Yixuan Chen <xlk AT umich.edu> wrote:

Dear Ralph and Dan,

Thanks for your suggestions. It seems like the problem is much more complicated than I expected to be :( I might just take a detour to avoid the problem for now, but I will take a look into your suggestions later. Anyway, thanks a lot!

On Jul 3, 2018, 9:19 AM -0400, Ralph Matthes <Ralph.Matthes AT irit.fr>, wrote:

Dear Yixuan Chen,

Your question refers to a very old problem of Coq. It is just not possible to do categorical datatypes there in a generic fashion. One would like to speak about an arbitrary "functor" f and later use the generic construction in concrete instances that would even mostly be strictly positive. But this is not supported by Coq.

I have written papers where I suggested other recursion schemes that would work - even in Coq - for a class of f that is far more liberal than strict positivity (see my papers in JFP and SCP). The requirement for that class can be encapsulated logically, as you described in your post.

You can also switch off the checks, see the benefits of it in my TYPES'18 talk (in particular the second last slide of it), available at https://types2018.projj.eu/conference-programme/#session8 - move two lines up there and click on the title of the talk.

Kind regards,    Ralph Matthes

Le 03/07/2018 à 02:20, Yixuan Chen a écrit :

Dear Coq users,

I met a situation where I need to define an inductive type like,

Context (f: Type -> Type).

Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.

This does not pass the positive occurrence check, and it shouldn’t. However, the actual definition that would be passed as f should always guarantee to generate only legitimate types. Is there a way to write “strictly positive occurrence” as an proposition in Coq and make it as an hypothesis for f in the client and proved by the provider(s) of f? Thanks.

Best Regards,

Yixuan (Luke) Chen