Stream: Coq users

Topic: Defining a proof scheme when using a type constructor

Pierre Vial (Jul 01 2020 at 16:31):

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?

Matthieu Sozeau (Jul 01 2020 at 16:51):

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)

Pierre Vial (Jul 01 2020 at 17:22):

OK, thanks Matthieu!

Paolo Giarrusso (Jul 01 2020 at 20:52):

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: Oct 01 2023 at 19:01 UTC