The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Just removing "in ... return ..." seems to work.

Program Fixpoint Interp (n : length) (T : Terms n) (s : Assignment)
{measure (TermsDepth n T) } : nats n :=
  match T 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.

- Gil

On Sat, Nov 19, 2011 at 8:08 PM,  
<alexander AT math.ohio-state.edu>
 wrote:
> 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
>