The Coq mailing list

["Alessandro Warth" <alexwarth AT gmail.com>]

Thanks, Pierre - that was exactly what I was looking for. Although I
still need to learn more about how things work in Coq, your technique
worked beautifully for my proof. Thanks again, this is a big help.

Cheers,
Alex Warth

On 5/31/06, Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr> wrote:

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