The Coq mailing list

[alexander AT math.ohio-state.edu]

Hello,

I am attempting a complicated definition by induction on a well-founded depth
measure.  I have gotten the definition to type-check, but the obligations seem
to be missing key hypotheses which make them impossible to prove!

The definition is as follows (for a complete file, see
http://www.math.osu.edu/~alexander/variadic/variadic1.txt and to understand
what I'm trying to define here, see Definition 5 at
http://arxiv.org/PS_cache/arxiv/pdf/1105/1105.4135v1.pdf)

Program Fixpoint Interp (n : length) (T : Terms n) (s : Assignment) { measure
(TermsDepth n T) } : nats n :=
  match T in (Terms n) return nats n with
  | Tnil => Nnil
  | var n0 T0 x => Ncons n0 (Interp n0 T0 s) (s x)
  | const n0 T0 c => Ncons n0 (Interp n0 T0 s) c
  | apply n0 m T0 f U => Ncons n0 (Interp n0 T0 s) (M m f (Interp m U s))
  | varapply n0 T0 G u v x => Ncons n0 (Interp n0 T0 s) (M (ToLength (Interp 1
v s)) G (Interp (ToLength (Interp 1 v s)) (VarSub u (ToLength (Interp 1 v s))
x) s))
  end.

This generates 7 obligations, all of which seem to be missing key hypotheses. 
The first obligation is as follows:

Coq < Obligation 1.
1 subgoal

  n : length
  T : Terms n
  s : Assignment
  Interp : forall (n0 : length) (T0 : Terms n0),
           Assignment -> TermsDepth n0 T0 < TermsDepth n T -> nats n0
  n0 : length
  T0 : Terms n0
  x : variable
  ============================
   TermsDepth n0 T0 < TermsDepth n T

This corresponds to the "var" case in the definition.  But it is missing the
most important hypothesis:  the relationship between n,T and n0,T0!  Namely,
there should be hypotheses something like...

Relationship1:  n = S n0
Relationship2:  T = var n0 T0 x

How can I force Coq to include these hypotheses, which really should be there
because that's the definition of the case where this obligation comes from? 
Similar remarks go for the other obligations.

Thanks very much for helping :)  I'm very gradually getting the hang of this
amazing language...

-Sam Alexander