Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to state a hypothesis with the help of another hypothesis

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to state a hypothesis with the help of another hypothesis


chronological Thread 
  • From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
  • To: Adam Chlipala <adam AT chlipala.net>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] how to state a hypothesis with the help of another hypothesis
  • Date: Wed, 10 Nov 2010 18:27:44 +0900
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=mOnPlSdFEonHYqakJz7axgzCaK+vMknC2FTiVTm2igIsl57LmdB4xrC2AX/R5kZ1fG b25TJ6OtqB0jPj3O/4su75U1zTX/TBURxfJPpWO8B9PB3uR6k+KddKJchmRnin1ZhnBH hyKGqMhT4v2oVcP2FTcfpM15msZcqiBrUpYNs=
Sorry, a bit late in the discussion.

> There are two main options.  First, you can use a cast:
>
> Hypothesis t_full :
>  forall n:nat, exists s:States, match t_nat in _ = T return T with
> refl_equal => s t end = n.

I really like this "case" trick. But I am really wondering if we can
avoid using  [JMeq] in principle or at least in many (how many?)
cases?

Gyesik


Archive powered by MhonArc 2.6.16.

Top of Page