The Coq mailing list

[Jieung Kim <gbali AT kaist.ac.kr>]

Dear Adam Chlipala,

Thank you for your advice.

2011/4/7 Adam Chlipala <adam AT chlipala.net>

Jieung Kim wrote:

I have one more question about a proof.

Is this a proof that you've already worked out informally?  That's an appropriate first step before asking for Coq-specific advice, in which case you should be asking how to encode particular steps of your informal proof, rather than the theorem overall.

For example, In this case, I think I cannot prove

   *Lemma sub_ty_same_or_not: forall t1 t2, (sub_ty t1 t2) \/

   ~(sub_ty t1 t2).*

This theorem looks provable to me.

--
Jieung Kim ( 김지응 )
Programming Language Research Group, KAIST
E-mail : gbali at kaist.ac.kr
            je1004k at gmail.com
Homepage : plrg.kaist.ac.kr/kje