The Coq mailing list

[alexander AT math.ohio-state.edu]

Hello,

Forgive me for posting about what seems to be an FAQ.  I couldn't find this
specific thing addressed in any of the FAQ answers.  I want to define an
interpretation function which takes certain structures and outputs naturals;
the definition is not based on direct structural decrease (so a naive attempt
to define it yields "Cannot guess decreasing argument of fix").  The 
definition
is based on induction on a notion of depth which I've defined.  How can I get
Coq to do this definition?

It seems like the Program Fixpoint ... { measure ... } syntax from the bottom
of this page is exactly what I'm looking for: 
http://coq.inria.fr/refman/Reference-Manual028.html

Unfortunately, it *does not work*.  I get the error:  Unknown interpretation
for notation { _ }.

Here is the definition without any attempt to Program (which "cannot guess
decreasing argument"):

Fixpoint InterpretTerm (T : Term) (s : Assignment) : nat :=
  match T with
   | var n => s n
   | const n => n
   | apply m f Ts => M _ f (InterpretTerms _ Ts s)
   | varapply f u v m => M (S (InterpretTerm v s)) f (InterpretTerms (S
(InterpretTerm v s)) (VariadicSub u (InterpretTerm v s) m) s)
  end
 with
  InterpretTerms (Tssize : nat) (Ts : Terms Tssize) (s : Assignment) {struct
Ts} : nats Tssize :=
    match Ts in (Terms Tssize) return nats Tssize with
     | Tnil => Nnil
     | Tcons m t0 Ts0 => Ncons m (InterpretTerm t0 s) (InterpretTerms _ Ts0 s)
    end.

Here is the attempt to use Program...measure, which generates syntax error:

Program Fixpoint InterpretTerm (T : Term) (s : Assignment) : nat { measure
(TermDepth T) } :=
  match T with
   | var n => s n
   | const n => n
   | apply m f Ts => M _ f (InterpretTerms _ Ts s)
   | varapply f u v m => M (S (InterpretTerm v s)) f (InterpretTerms (S
(InterpretTerm v s)) (VariadicSub u (InterpretTerm v s) m) s)
  end
 with
  InterpretTerms (Tssize : nat) (Ts : Terms Tssize) (s : Assignment) {struct
Ts} : nats Tssize { measure (TermsDepth Ts Tssize) } :=
    match Ts in (Terms Tssize) return nats Tssize with
     | Tnil => Nnil
     | Tcons m t0 Ts0 => Ncons m (InterpretTerm t0 s) (InterpretTerms _ Ts0 s)
    end.

Thanks very much for helping.  This is my first post to the mailing list, by
the way :)  I'm happy to see such an active community behind this software. 
Hopefully someday I'll be able to make some contributions instead of just post
newbie questions!

-Sam Alexander