The Coq mailing list

[Levis John <johnleviscoq AT gmail.com>]

Hi, I tried to define first-order terms in Coq with the following definitions:

Record Language : Type := language {

Function : Set; 

arityFunction : Function -> nat}

Section FOL. 

Variable L:Language.

Inductive Term : Set :=

| var : string -> Term

| FunApp : forall func:Function L, Terms (arityFunction L func) -> Term 

with Terms : nat -> Set :=

| Tnil : Terms 0

| Tcons : forall n:nat, Term -> Terms n -> Terms (S n).

Now i want to define GroundTerms, a subset of Term, in which terms have no free variables:

Inductive GroundTerm:Term->Prop:=

|FuncApp_GroundTerm:forall (func:Function L)(ts : Terms (arityFunction L func)), 

    GroundTerms (arityFunction L func) ts -> GroundTerm (FunApp func ts)

with GroundTerms(n:nat):(Terms n)->Prop:=

|Tnil_GroundTerms:GroundTerms 0 Tnil

|Tcons_GroundTerms:forall(n:nat)(t:Term)(ts:Terms n), 

  GroundTerm t ->GroundTerms n ts-> GroundTerms (S n) (Tcons n t ts).       

The GoundTerm definition makes sense to me, but the Coq complains that Parameters should be 

syntactically the same for GroundTerm and GroundTerms. 

Any suggestions?

............

--
John Levis