The Coq mailing list

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

I have the following definition:

   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 I'd like to prove:

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

I expected the following to work (modulo incomplete pattern matching, of
course):

   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 tells me:

   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 it seems that it hasn't refined `l3' to (x::l2) in the branch.
Or conversely it has refined `l3' to `l' but failed to refine (x::l2) to l.
Since refining (x::l2) to l is hard, I figured maybe Coq would accept
a syntax like:

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

but that's clearly not the case.  And I don't understand the problem
enough to be convinced that it'd be a step in the right direction anyway.

Could someone explain to me in detail what's going on and how I can adjust
the code of `test' so Coq accepts it?


        Stefan