The Coq mailing list

["Russell O'Connor" <roconnor AT Math.Berkeley.EDU>]

On Wed, 19 Nov 2003, Sébastien Hinderer wrote:

> Dear Coq users,
>
> Assume we have the following definitions :
>
> Inductive variable : Set := V : nat -> variable.
> Inductive function : Set := F : nat -> function.
> Definition signature := function -> nat.
> Definition arity := [s:signature;f:function] (s f).
>
> Then the following declaration is not accepted by Coq :
>
> Inductive term [s:signature] : Set :=
>   | Var : variable -> (term s)
>   | Fun :
>     (f:function) (l:(list (term s))) (H:(length l)=(arity s f)) (term s).
>
> Coq 7.4 returns the following error message :
>
> Error: Non strictly positive occurrence of _UNBOUND_REL_6 in
>  (f:function; l:(list (term s)))(length l)=(arity s f)->(term s)
>
> Does someone have an idea about what is wrong with the definition of term ?

This doesn't work because Coq can prove (or it isn't) a monotone type.
term cannon be passed as a parameter to list because list might be doing
bad things with it.  At least that is my take on the problem.

Here is how my friend Robert solved this problem for me:

(* From fol.v *)

Record Language : Type := language {
  Relations : Set;
  Functions : Set;
  arity : (Relations + Functions)->nat
}.

Section First_Order_Logic.

Variable L : Language.

Inductive Term : Set :=
   var : nat -> Term
 | apply : (f:(Functions L))(Terms (arity L (inr ? ? f))) -> Term
with Terms : nat -> Set :=
   Tnil : (Terms O)
 | Tcons : (n:nat)Term -> (Terms n) -> (Terms (S n)).

Scheme Term_Terms_ind := Induction for Term Sort Prop
with Terms_Term_ind := Induction for Terms Sort Prop.

Scheme Term_Terms_rec := Minimality for Term Sort Set
with Terms_Term_rec := Minimality for Terms Sort Set.

Scheme Term_Terms_rec_full := Induction for Term Sort Set
with Terms_Term_rec_full := Induction for Terms Sort Set.

-- 
Russell O'Connor                <http://math.berkeley.edu/~roconnor/>
                Work to ensure that Iraq is run by Iraqis.