The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Consider the well known contrasting approaches to definition:

Inductive ptrm : Set :=
| ptRel : ptrm
| ptApp : ptrm -> list ptrm -> ptrm.

Inductive Trm : Set :=
| TRel  : Trm
| TApp  : Trm -> Trms -> Trm
with Trms : Set :=
| tnil  : Trms
| tcons : Trm -> Trms -> Trms.

It is possible to directly define a size function for both definitions
of terms, e.g.

Function ptrmSize (t:ptrm) : nat :=
  match t with
    | ptRel => 1
    | ptApp fn args =>
      S (ptrmSize fn +
        (fold_left (fun x y => x + ptrmSize y) args 0))
  end.

Function TrmSize (t:Trm) : nat :=
  match t with
    | TRel => 1
    | TApp fn args => S (TrmSize fn + TrmsSize args)
  end
with TrmsSize (ts:Trms) : nat :=
       match ts with
         | tnil => 0
         | tcons u us => (TrmSize u + TrmsSize us)
       end.

BUT, the definition of ptrmSize in Coq (8.5pl1) is not able to
mechanically generate a functional induction principle, while the
definition of TrmSize is able to generate a functional induction
principle.

Is there a definition of size for ptrm that can mechanically generate
a functional induction principle?  (I insist on "mechanically
generate" because my real application is much bigger than this
example, and I'm interested in functions other than "size".)

I know of one way to do it: recurse over something different than the
term structure.  E.g. use a "fuel" parameter:

Function ptrmSize' (n:nat) (t:ptrm) {struct n} : option nat :=
  match n with
    | 0 => None
    | S n => match t with
               | ptRel => Some 1
               | ptApp fn args =>
                 match ptrmSize' n fn, ptrmsSize n args with
                   | Some x, Some y => Some (S (x + y))
                   | _, _ => None
                 end
             end
  end
with ptrmsSize (n:nat) (ts:list ptrm) {struct n} : option nat :=
       match n with
         | 0 => None
         | S n => match ts with
                    | nil => Some 0
                    | cons u us =>
                      match ptrmSize' n u, ptrmsSize n us with
                        | Some x, Some y => Some (x + y)
                        | _, _ => None
                      end
                  end
       end.

Does anyone know a cleaner way?

Thanks,
Randy