The Coq mailing list

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

I don't expect Program with measure to be a complete algorithm.
In your example, it is hard to automatically figure out the right structure.
So, I think one should do some work to make it to work correctly.
The following is my solution.
I hope this helps.

Program Fixpoint gmap {A B : Type} (l: list A) (f: forall a (IN: In a
l), B) : list B :=
  match l return (forall a (IN: In a l), B) -> list B with
  | nil => fun _ => nil
  | a :: t => fun f => f a _ :: gmap t (fun _ IN => f _ (or_intror _ IN))
  end f.

Program Fixpoint Interp (T : Term) (s : Assignment) {measure (Depth T)} : nat 
:=
  match T with
  | var x => s x
  | const c => c
  | apply f Ts => M f (gmap Ts (fun A IN => Interp A s))
  | varapply G u v x => M G (gmap (VarSub u x (S (Interp v s))) (fun A
IN => Interp A s))
  end.

Best,
Gil

On Mon, Nov 21, 2011 at 5:12 AM, Alexander, Samuel
<alexander AT math.ohio-state.edu>
 wrote:
>
>>> Just removing "in ... return ..." seems to work.
>
>> I am wondering why it doesn't work when "in ... return..." is used.
>
> To make matters even more mysterious, the definition at the bottom of the 
> following file suffers the same problem, and this time just messing around 
> with "in ... return ..." no longer fixes it:
>
> http://www.math.osu.edu/~alexander/variadic/variadic3.txt
>
> -Sam Alexander
>