The Coq mailing list

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

Hi,

Alessandro Warth wrote:

> 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.


The subtyping relation you describe is the least reflexive and 
transitive relation, hence  the
identity over AType.

Lemma L0 : forall (T T1:AType), subtyping T T1 -> T = T1.
Proof.
induction 1.
auto.
transitivity T2;[assumption | symmetry;auto].
Qed.

So, your lemma follows directly:

Lemma l : forall (n:nat) (T:AType),
          subtyping (Red n) T ->
          exists m:nat, T = (Red m).
Proof.
intros n T; exists n;symmetry;apply L0.
assumption.
Qed.


I guess  this is not the relation you meant.  You need perhaps the 
reflexive end transitive closure of
some simple relation defined on AType. Am I right ?

Hope this helps,

Pierre




> 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