The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

[ Apologies if this is a repeat: I tried to send it via Gmane (where I read
  this list) and it appears to have disappeared in the ether. ]

Let's say I have the following code:

   Inductive ULeq (k:Set) : list k -> list k -> Set :=
     | ULeq_refl : forall l, ULeq l l
     | ULeq_skip : forall l1 l2 x, ULeq l1 l2 -> ULeq (x::l1) (x::l2).

and want to show that

   Definition test : forall k (l1:list k) l2 l3 x,
              ULeq l1 l2 -> ULeq (x::l2) l3) -> ULeq (x::l1) l3.

I expected the following code to work (modulo incomplete matching,
obviously):

   Definition test k (l1:list k) l2 l3 x
              (PE1: ULeq l1 l2) (PE2 : ULeq (x::l2) l3)
              : ULeq (x::l1) l3 :=
     match PE2 in ULeq l2' l3 return ULeq (x::l1) l3 with
     | ULeq_refl l => ULeq_skip x PE1
     end.

but Coq actually complains

   The term "ULeq_skip x PE1" has type "ULeq (x :: l1) (x :: l2)"
    while it is expected to have type "ULeq (x :: l1) l"

So Coq doesn't do the type refinement in the dependent elimination like
I expect it to.  My understanding right now is that Coq fails to substitute
l3 by (x::l2) or that I'm basically asking it to substitute (x::l2) by
l which it (reasonably) refuses to do.

Can someone explain to me exactly what's happening and/or how I could adjust
my code so that Coq understands what I want to do?


        Stefan