The Coq mailing list

[Murali Vijayaraghavan <vmurali AT csail.mit.edu>]

Does that mean the above definition does not lead to an inconsistency? I want to know if I can keep the above definition with the fixed point instead of having an isomorphic definition (almost like) below which is accepted by default, and convert back and forth in my development.

Inductive Foo: Type :=
| Simple: nat -> Foo
| Bad n (vals: Fin.t n -> Foo): Foo.

Would one be able to fix the (strict) positivity requirement to allow these cases in the future?

On Thu, May 1, 2025 at 7:14 AM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

fixpoints are not understood by the positivity checker, so it rejects the declaration.

Gaëtan Gilbert

On 01/05/2025 08.15, Murali Vijayaraghavan wrote:
> Hi
>
> I was wondering why the following definition fails:
>
> Inductive Foo: Type :=
> | Simple: nat -> Foo
> | Bad n (vals: (fix helper n :=
>                    match n with
>                    | 0 => unit
>                    | S m => (Foo * helper m)%type
>                    end) n): Foo.
> Error: Non strictly positive occurrence of "Foo" in
> "forall n : nat, (fix helper (n0 : nat) : Set :=
>                      match n0 with
>                      | 0 => unit
>                      | S m => (Foo * helper m)%type
>                      end) n -> Foo".
>
>  From my understanding, strictly positive occurrence requirement is violated if I supply the inductive type as an argument to one of the constructor arguments (as discussed in http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30 <http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html#lab30>), but in the above example, I am just trying to use an size-indexed tuple as a constructor argument. How can I prove False if the above definition were accepted?
>
> Thanks
> Murali