The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

I tried to look at "test" in an interactive way :

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

 k : Set
 l1 : list k
 l2 : list k
 l3 : list k
 x : k
 H : ULeq l1 l2
 H0 : ULeq (x :: l2) l3
 ============================
  ULeq (x :: l1) l3
*)
case H0.
(*

2 subgoals
 ...
 x : k
 H : ULeq l1 l2
 H0 : ULeq (x :: l2) l3
 ============================
  forall l : list k, ULeq (x :: l1) l

subgoal 2 is:
forall (l4 l5 : list k) (x0 : k), ULeq l4 l5 -> ULeq (x :: l1) (x0 :: l5)
*)

The first subgoal is associed with the expected type you complained about.

>     match PE2 in ULeq l2' l3 return ULeq (x::l1) l3 with
>     | ULeq_refl l => ULeq_skip x PE1
>     end.
>
>  
When you eliminate the hypothesis PE2, you try to build a function which 
maps any variable
H of type (ULeq l2' l3') to a term of type ULeq (x::l1) l3'

The first case for H is a term of the form (ULeq_refl l l) ; So what you 
have to provide is a term of
type ULeq (x::l1) l    


When dealing with such cases (eliminating hypotheses which contain some 
constrained variables) its sometimes
better to use inversion tactics.

  Definition test : forall k (l1:list k) l2 , ULeq l1 l2 -> forall x l3,
              ULeq (x::l2) l3 -> ULeq (x::l1) l3.
induction 1.
auto.
intros.
inversion H0.
constructor 2.
constructor 2.
auto.
constructor 2.
auto.
Qed.


Pierre


> 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
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>