The Coq mailing list

["Brian E. Aydemir" <baydemir AT cis.upenn.edu>]

Quoting Robbert Krebbers 
<robbertkrebbers AT student.ru.nl>:

> Fixpoint avar_rec2 (a : avar) : P a :=
>  match a as x return P x with
>  | avr v t => H4 v t (trm_rec2 t)
>  end
> with trm_rec2 (t : trm avar) : Q t :=
>  match t as t0 return Q t0 with
>  | srt s => H s
>  | bvr n => H0 n
>  | fvr a => H1 a (avar_rec2 a)
>  | bnd b t0 t1 => H2 b t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  | app t0 t1 => H3 t0 t1 (trm_rec2 t0) (trm_rec2 t1)
>  end.
>
> Unfortunately this does not work, the system gives the following error:
>
>  Error:
>  Recursive definition of trm_rec2 is ill-formed
>  ...
>  Recursive call to avar_rec2 has principal argument equal to "a"
>  instead of a subterm of t

I've encountered this problem before [1], and as far as I know, Adam's  
suggestion is the way to go.  For the sake of concreteness, I've  
included below code that implements the basic idea.

Cheers,
Brian

[1] A non-bug report involving lists and a separate inductive type:
    http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1751

(* *********************************************************************** *)

Parameter sort : Set.

Inductive binder : Set := abs | pi.
Inductive trm (var : Set) : Set :=
   srt : sort -> trm var
 | bvr : nat -> trm var
 | fvr : var -> trm var
 | bnd : binder -> trm var -> trm var -> trm var
 | app : trm var -> trm var -> trm var.

(* *********************************************************************** *)

Section Induction.

Variables
  (var : Set)
  (P : var -> Set)
  (Q : trm var -> Set)
  (f : forall v, P v).

Hypotheses
 (H  : forall s : sort, Q (srt _ s))
 (H0 : forall n : nat, Q (bvr _ n))
 (H1 : forall a : var, P a -> Q (fvr _ a))
 (H2 : forall b t1 t2, Q t1 -> Q t2 -> Q (bnd _ b t1 t2))
 (H3 : forall t1 t2, Q t1 -> Q t2 -> Q (app _ t1 t2)).

Fixpoint trm_rec' (t : trm var) : Q t :=
  match t with
    | srt s => H s
    | bvr n => H0 n
    | fvr v => H1 v (f v)
    | bnd b t1 t2 => H2 b t1 t2 (trm_rec' t1) (trm_rec' t2)
    | app t1 t2 => H3 t1 t2 (trm_rec' t1) (trm_rec' t2)
  end.

End Induction.

(* *********************************************************************** *)

Parameter var : Set.
Inductive avar : Set :=  avr : var -> trm avar -> avar.

Notation atrm := (trm avar).
Notation asrt := (srt avar).
Notation abvr := (bvr avar).
Notation afvr := (fvr avar).
Notation abnd := (bnd avar).
Notation aapp := (app avar).

(* *********************************************************************** *)

Section Induction2.

Variables
  (P : avar -> Set)
  (Q : atrm -> Set).

Hypothesis
 (H  : forall s : sort, Q (asrt s))
 (H0 : forall n : nat, Q (abvr n))
 (H1 : forall a : avar, P a -> Q (afvr a))
 (H2 : forall (b : binder) (t1 : atrm) (t2 : atrm),
    Q t1 -> Q t2 -> Q (abnd b t1 t2))
 (H3 : forall (t1 : atrm) (t2 : atrm),
    Q t1 -> Q t2 -> Q (aapp t1 t2))
 (H4 : forall (v : var) (t : atrm), Q t -> P (avr v t)).

Fixpoint avar_rec2 (v : avar) : P v :=
  match v with
    | avr v t => H4 v t (trm_rec' _ P Q avar_rec2 H H0 H1 H2 H3 t)
  end.

Definition trm_rec2 := trm_rec' _ P Q avar_rec2 H H0 H1 H2 H3.

End Induction2.

(*
avar_rec2
     : forall (P : avar -> Set) (Q : atrm -> Set),
       (forall s : sort, Q (asrt s)) ->
       (forall n : nat, Q (abvr n)) ->
       (forall a : avar, P a -> Q (afvr a)) ->
       (forall (b : binder) (t1 t2 : atrm), Q t1 -> Q t2 -> Q (abnd b  
t1 t2)) ->
       (forall t1 t2 : atrm, Q t1 -> Q t2 -> Q (aapp t1 t2)) ->
       (forall (v : var) (t : atrm), Q t -> P (avr v t)) ->
       forall v : avar, P v

trm_rec2
     : forall (P : avar -> Set) (Q : atrm -> Set),
       (forall s : sort, Q (asrt s)) ->
       (forall n : nat, Q (abvr n)) ->
       (forall a : avar, P a -> Q (afvr a)) ->
       (forall (b : binder) (t1 t2 : atrm), Q t1 -> Q t2 -> Q (abnd b  
t1 t2)) ->
       (forall t1 t2 : atrm, Q t1 -> Q t2 -> Q (aapp t1 t2)) ->
       (forall (v : var) (t : atrm), Q t -> P (avr v t)) ->
       forall t : atrm, Q t
*)