The Coq mailing list

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

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