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
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
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.
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
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
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
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: Jan 29 2023 at 06:02 UTC