The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Indeed from reading:

https://github.com/coq/coq/blob/b8477fb38842016c226ba9d7be8f60486411a2ee/kernel/indtypes.ml#L285-L289

We can see a check that the inductive type outside the nesting must be covariant. Which is why this works for `List`, but would not work for some contravariant datatype (one that uses its parameter as an argument to a function, for instance).

You can also see additional restrictions (some specific to Coq) in the previous lines (for instance, the nested inductive type must only appear as a parameter of the nesting type, not as an index, and nested inductive-inductive definitions seem to be rejected).

Now that does not necessarily answer the question as far as CIC is concerned.

- Valentin

On Tue, 13 Aug 2019 at 10:38, William J. Bowman <wjb AT williamjbowman.com> wrote:

This is a understandable enough solution, and thanks for the pointer to CPDT;
I'll take a look.

Thanks!

--
William J. Bowman

On Wed, Aug 07, 2019 at 12:02:12PM -0400, Hans Jacob Fehrmann Rojas wrote:
> Hi William,
>
> I'm not an expert but a very sutil interpretation of the rules seems that
> the nested positive condition should be applied only considering the arity
> of the inductives without the parameters as if the `List (Rose A)` would be
> a new inductive.
>
> So for your example:
>
> Inductive Rose (A : Set) : Set :=
> | rose : (List (Rose A)) -> Rose A.
>
> Should check the positivity condition with respect to (assuming is a valid
> declaration)
>
> Inductive ListRose : Set :=
> | nil : ListRose
> | cons : Rose A -> ListRose -> ListRose.
>
> This is the argument in Certified Programming with Dependent Types (3.8
> Nested Inductive Types)
>
> Also, it seems that the check of the positive condition for an inductive
> definition is done in coq sources in checker/indtype.ml, specifically the
> function `check_positivity` and it seems that the parameters are not taking
> in consideration when checking the positivity condition, so the arguments
> of Chlipala seems right
>
> Hope these helps
>
> Best,
> Hans.
>
> On Tue, Aug 6, 2019 at 11:00 PM William J. Bowman <wjb AT williamjbowman.com>
> wrote:
>
> > I just finished implementing the CIC positivity checker as specified in
> > the Coq
> > docs, but the docs seem under specified about how the strict positivity
> > algorithm should work.
> >
> >   https://coq.inria.fr/doc/language/cic.html#positivity-condition
> >
> > If I try to implement the rules as specified, I get stuck in an infinite
> > loop
> > when checking nested inductive types.
> >
> > Consider rose trees:
> >
> > Inductive List (A : Set) : Set :=
> > | nil : List A
> > | cons : A -> List A -> List A.
> >
> > Inductive Rose (A : Set) : Set :=
> > | rose : (List (Rose A)) -> Rose A.
> >
> > I must show `Rose` occurs strictly positively in `(List (Rose A))`, from
> > the
> > type of the constructor `rose`.
> >
> > Loop:
> > To show that `Rose` occurs strictly positively in `List (Rose A)`,
> > since `List (Rose A)` is of the form `(I p_0 ... p_m u ...)` and `List` is
> > not
> > mutually inductive, we must show the nested positivity condition for each
> > constructor of `List` after instantiating the types of the constructors
> > with the
> > parameter `(Rose A)`.
> >
> > There are two cases:
> > - nil : `(List (Rose A))` satisfies nested positivity w.r.t. `Rose`
> > trivially.
> >
> > - cons : `Rose A -> List (Rose A) -> List (Rose A)`
> > To show this satisfies nested positivity w.r.t. `Rose`, we must show that
> > `Rose`
> > occurs strictly positively in `List (Rose A)`.
> > goto Loop
> >
> >
> > For now, I've "fixed" this by allowing myself to assume strict positivity
> > holds
> > for `List (Rose A)` while checking nested positivity.
> > This seems okay, in a vague, intuitive, "something something greatest
> > fixpoints?" kind of way, but I'd like to be a little more formal than that.
> >
> > Does anyone know what's missing from the Coq docs or what reference I
> > should
> > look at?
> >
> > I usually start from the Coq docs as they have the most readable and
> > complete
> > CIC spec in one place.
> > I tried reading the Coq kernel code but.. failed.
> > I also tried Paulin-Mohring's "Inductive Definitions in the system Coq
> > Rules and
> > Properties", but can't find anything about nested inductive types.
> >
> > --
> > William J. Bowman
> >