The Coq mailing list

[Christian Kjær Larsen <christianden AT gmail.com>]

Hi Guillaume,
> Definition map_fusion t G (e : exp G t) :=
>   match e in exp _ t' return exp G t' -> exp G t' with
>   | emap t2 t1 g em => ...
>   |  _ => fun e => e
>   end e. (* notice "e" here! *)
>
> Now for the "..." part. The "em" binder is of type "exp G (TList t2)".
> But if you match on it, you necessarily lose the "TList t2" part. For
> instance, in the "etrue" case, this part is "TBool". This is obviously
> contradictory and thus "em" cannot be "etrue", but this is not readily
> apparent to Coq's type system. So you have to preserve the information
> manually.
>
> To do so, you need to change "em" so that it is of type "exp G lt2" for
> some arbitrary lt2 while keeping the identity "TList t2 = lt2" in your
> context. So the "..." part becomes
>
> (fun lt2 (em' : exp G lt2) =>
>   match em' in exp _ lt2 return (TList t2 = lt2 -> _) with
>   | emap t3 t2' f eb => fun Heq _ => emap (compose f ...) eb
>   | _ => fun _ e => e
>   end) (TList t2) em eq_refl
>
Thanks! I was trying something like this using the refine tactic, but
with your help I got it working.

Do you know if the Program tactic does something like this under the hood?

Cheers,
Christian