The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

In Coq 8.4 (things may differ in 8.5), the following is not accepted:

Inductive fin_ (fin_n : Set) : Set :=

| G : fin_ fin_n

| U : fin_n -> fin_ fin_n

.

Inductive fin (n : nat) : Set :=

| F : match n with O => Empty_set | S n => fin_ (fin n) end -> fin n.

I do not really care about workarounds, I perfectly know how to deal with it.

Still, I was wondering if positivity checkings could not deal with pattern matching.

Clearly, in each branch, positivity holds, thus my wondering.

I think this kind of construction could be useful, and seems to be related to induction-recursion as in Agda.

Its main point is to avoid an indice and have a parameter inside without relying on tricks such as inserting an equality inside of the branch [which in fact delays the indice inside of the equality]. It also avoids using explicitely a fixpoint to build the type.

Happy new year