The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 17 Dec 2005, Stefan Monnier wrote:

> 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"

The problem is that match PE2 in ULeq l2' l3 creates a fresh variable l in
place of l3.  Of course this fresh variable has no relation to (x::l2) and
that is why the type checker fails.

The correct way to handle this is to use the inversion tactic.

Definition test k (l1:list k) l2 l3 x :
              ULeq l1 l2 -> ULeq (x::l2) l3 -> ULeq (x::l1) l3.
intros.
inversion H0.
constructor.
assumption.
Show Proof.

As you can see, this isn't really somthing you would want to write by
hand.

However, I don't think this will be a good way of proceeding in your
proof.



Your inductive definition seems a bit silly (maybe I misunderstand what
you are trying to do).  But the skip consturctor is really unneccessary.

 Inductive ULeq2 (k:Set) : list k -> list k -> Set :=
     | ULeq2_refl : forall l, ULeq2 l l.

Is adequate by the following lemma.

Lemma skip_redudent : forall k, forall (l1 l2 : list k), ULeq l1 l2 ->
ULeq2 l1 l2.
Proof.
intros.
induction H.
constructor.
destruct IHULeq.
constructor.
Qed.

And now ULeq2 x y is really equivalent to (x=y), so you might as well use
the eq type.

Anyhow, if you insist on a proof of your test lemma, here is how I would
prove it.  Notice the assert at the beginning.

Definition test k (l1:list k) l2 l3 x :
              ULeq l1 l2 -> ULeq (x::l2) l3 -> ULeq (x::l1) l3.
intros.
assert (forall (l1 l2: list k), ULeq l1 l2 -> l1=l2).
intros.
induction H1.
reflexivity.
rewrite IHULeq.
reflexivity.
replace l3 with (x::l2).
constructor.
assumption.
apply H1.
assumption.
Qed.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''