This is a beginner question (although the examples involve the MetaCoq extension).

**Tl;dr**: I can't define a proof scheme (as in https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html#coq:cmd.scheme ) when one of the two types has a constructor, e.g. when it is of the form `list A`

for some type `A`

.

Verbose version: I want to define a predicate characterizing terms (assumed in normal forms) that correspond to first-formulas. Some background: the type `term`

is the type of reified terms in MetaCoq, and reified term constructors often take lists of terms as arguments. For instance, the second argument of `tApp`

below is a list of terms (and not just a term). This constrains me to write mutually inductive definitions.

The predicate below is obviously not enough to capture first-order types (observe the two function `is_Fo_type`

and `is_FO_type_list`

below)

```
Fixpoint is_FO_type (t:term) :=
match t with
| tProd na ty body => is_FO_type (body)
| tApp (tConst (MPfile ["Datatypes"; "Init"; "Coq"], "andb") []) u => is_FO_type_list u
| => false
end
with
is_FO_type_list (u: list term) :=
match u with
| nil => true
| t':: u' => (is_FO_type t') && (is_FO_type_list u')
end.
```

Coq rejects this definition and gives me the following reason:

Error: Recursive definition of is_FO_type_list is ill-formed.

In environment

is_FO_type : term -> bool

is_FO_type_list : list term -> bool

u : list term

t' : term

u' : list term

Recursive call to is_FO_type has principal argument equal to "t'" instead of "u'".

Recursive definition is: "fun u : list term => match u with

| [] => true

| t' :: u' => (is_FO_type t' && is_FO_type_list u')%bool

end".

Yet, if I (naively) follow https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html#coq:cmd.scheme and write

```
Scheme term_list_rec := Induction for term Sort Set
with list_term_rec := Induction for (list term) Sort Set.
```

Coq is also unhappy:

Error: Syntax error: [smart_global] expected after 'for' (in [scheme_kiquote

When I remove the parenthesis (`Induction for list term Sort Set.`

), Coq still outputs an error. Likewise when I define `lterm`

as `list term`

(Coq does not recognize this as an inductive type).

So, my question is: how do I make my mutual definition work using (or not) a proof scheme in presence of the constructor `list`

?

Indeed `Scheme`

does not handle nested inductive types like this one (where nesting of lists and terms happen). Instead of a `with is_FO_type_list`

, you will have to write the fixpoint locally in is_FO_type (or use some higher order function like List.existsb)

OK, thanks Matthieu!

Another common solution is to define two mutually recursive types, A and As, where As is just a specialized list of A. The price is writing and using conversions between As and list A, but the advantage is that quite some tooling is happier to deal with such inductive types.

Last updated: Jun 14 2024 at 19:02 UTC