The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hello Alessandro,
I am not sure that the inductive type 'subtyping' really reflects what  
you want to express. In fact, we can easily prove the following lemma:

 Lemma sub_cst: forall T1 T2, subtyping T1 T2 -> T1 = T2.
 induction 1.
 auto.
 rewrite IHsubtyping1; auto.
Qed.

so this predicate only relates two equal AType, its second constructor  
(s_trans) is then useless.

Concerning your lemma, it can be straightforwardly proved using the  
lemma above
Lemma l : forall (n:nat) (T:AType),
            subtyping (Red n) T ->
            exists m:nat, T = (Red m).
intros.
rewrite <- (sub_cst _ _ H).
exists n.
auto.
Qed.


Hope this helps!

Regards,

Houda


> Hello,
>
> I'm trying to use Coq to formalize a programming language that I've
> been working on. Unfortunately, a few days ago I ran into trouble
> while proving what (I think) should be a very simple lemma. I've spent
> the past few days banging my head against the wall and have made no
> progress, so I was hoping someone might be able to give me a few
> pointers...
>
> Here is the simplest formulation of that lemma that I could come up with:
>
>
> 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).
>
>
> This should be easy to prove, but I haven't had any luck so far. Does
> anybody have any ideas about how I might be able to prove this?
>
> Thank you kindly,
> Alex Warth
>
> --------------------------------------------------------
> 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



===============================
         Houda Anoun

    Bordeaux1-LaBRI-Signes
     phone:05 40 00 35 15
  web: www.labri.fr/perso/anoun
        ++++++++++++++
Electric lamps were not invented
    by improving candles
=================================

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.