The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Tue, May 30, 2006 at 05:04:35PM -0700, Alessandro Warth wrote:
> Hello,
> 
> Inductive AType : Set :=
> | Red : nat -> AType
> | Black : nat -> AType.
> 
> Inductive subtyping : AType -> AType -> Prop :=
> | s_refl   : forall T,
>                subtyping T T
> | s_trans  : forall T1 T2 T3,
>                subtyping T1 T2 ->
>                subtyping T2 T3 ->
>                subtyping T1 T3.
> 
> Lemma l : forall (n:nat) (T:AType),
>            subtyping (Red n) T ->
>            exists m:nat, T = (Red m).
> 

You can proceed by induction over the subtyping hypothesis. 
The pitfall is that you should do it directly, since coq would 
forget that the first argument of subtyping is of the form (Red n). 
So you need to store that information: 

Lemma l' : forall (T0 T:AType),
           subtyping T0 T -> 
           forall n, T0 = Red n ->
           exists m:nat, T = (Red m).
Proof.
induction 1.
intros; exists n; auto.
intros.
destruct (IHsubtyping1 _ H1) as (m,Hm). 
destruct (IHsubtyping2 _ Hm) as (p,Hp). 
exists p; auto.
Qed.

Lemma l : forall (n:nat) (T:AType),
           subtyping (Red n) T ->
           exists m:nat, T = (Red m).
Proof.
intros.
destruct (l' (Red n) T H n) as (m,Hm); auto.
exists m; auto.
Qed.

Best regards, 

Pierre Letouzey