The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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