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.

For those who, like me, can't stand the non-declarativeness of Coq tactics,
the answer looks like the code below:

   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 (x::l2 = l2') -> ULeq (x::l1) l3 with
      | ULeq_refl l => fun P:(x::l2=l) =>
                       match P in _ = l return ULeq (x::l1) l with
                       refl_equal => ULeq_skip x PE1
      end) refl_equal.

I.e. yu have to manually construct a proof of equality, refine that proof
via the `match', then match on the proof to finally do the substitution
you wanted.

The `inversion' tactic does that for you if you use tactics.


        Stefan