Using length of list X as an argument for a constructor of X in Coq

Question

The title is not very informative, so let me explain.

I'm trying to formalize what it means to be a term in first-order logic. Here is the textbook definition of terms of an arbitrary language L:

(1) Each variable or constant is a term. 
(2) If n ≥ 1, f is an n-ary function of L, and t1 ... tn are terms of L, then f t1 ... tn is a term of L.

I have already defined variables, constants, functions, and languages as var, const, func, and lang. I also have functions f_arity and L_funcs that returns the arity of a function and the ensemble of all functions in a language, respectively. So giving an inductive definition of terms should be pretty straightforward :

Inductive term ( L : lang ) : Type :=
| t_v : var -> term L
| t_c : const -> term L
| t_f : forall ( f : func ) 
  ( l : list ( term L ) ),
  length l = f_arity f 
  -> In func ( L_funcs L ) f 
  -> term L.

But it doesn't work. Instead, I get this error message.

Error: Non strictly positive occurrence of "term" in
 "forall (f : func) (l : list (term L)),
  length l = f_arity f -> In func (L_funcs L) f -> term L".

I have a vague idea of what's going on here. The constructor t_f has an argument length l = f_arity, which Coq doesn't like because it has term L on the left side of an arrow. But I think Coq is being overly cautious here, because it lets me do pretty much the same thing if I tweak the types a bit. I could, for instance, define a custom list type listN indexed by its size, so that list X n would be a list of X with n elements. Then I would have

Inductive term ( L : lang ) : Type :=
| t_v : var -> term L
| t_c : const -> term L
| t_f : forall ( f : func ) 
  ( l : listN ( term L ) ( f_arity f ) ),
  In func ( L_funcs L ) f -> term L .

But I don't want to go this way, because it is ad-hoc, and makes all the useful list libraries unusable. So I'm looking for a way to convince Coq that what I'm trying to do is perfectly safe, so it will accept length l = f_arity f as a constructor argument. Is there a way to do this?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2014-11-10T20:52:13

This is a nice problem indeed, I hadn't encountered it in this form before.

Quite frankly, unfortunately, I don't see a way of getting Coq to accept your definition as is. Here are some options for mitigating this problem:

Use a separate inductive predicate for term well-formedness. Manipulating terms will be much more convenient, because you won't have to worry about the length constraints when writing your functions. On the other hand, you will have to reason about well-formedness separately when proving anything about it. Thus, you would have something like
```
Inductive term L : Type :=
| t_v : var -> term L
| t_c : const -> term L
| t_f f (ts : list (term L)) : term L.

Inductive wf_term L : term L -> Prop :=
| wf_v v : wf_term L (t_v v)
| wf_c c : wf_term L (t_c c)
| wf_f f ts :
  In f (L_funcs L) ->
  Forall (wf_term L) ts ->
  length ts = f_arity f ->
  wf_term L (t_f f ts).
```
Use a dependently typed encoding for term. You can add e.g. a nat parameter to term for expressing how many arguments are "missing", which would give you something like
```
Inductive term L : nat -> Type :=
| t_v : var -> term L 0 
| t_c : const -> term L 0
| t_f f : In f (L_funcs L) -> term L (f_arity f)
| t_a n (t : term L (S n)) (t : term L 0) : term L n.
```
This might not be what you want, since you don't get the list of arguments to manipulate, but it might be helpful.
Use a "bad" encoding with a length-indexed list, and use auxiliary types ("views") and functions to make this "bad" definition more convenient to use. You define term like in your second definition, but then define a new term' on top of it, like
```
Inductive term' L : Type :=
| t_v' : var -> term' L
| t_c' : const -> term' L
| t_f' f (ts : list (term L)) :
  In f (L_funcs L) ->
  length ts = f_arity f ->
  term' L.

Definition term_view L (t : term L) : term' L := (* ... *)

(* Wrapper around the original constructor *)
Definition t_f'' L f ts : In f (L_funcs L) -> length ts = f_arity f -> term L :=
  (* ... *)
```
You can even define custom induction/recursion principles that work directly with t_f'' instead of t_f, effectively hiding the annoying details of your original definition.

Using length of list X as an argument for a constructor of X in Coq

1 Answers