Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] discriminate JMequalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] discriminate JMequalities


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: Adam Chlipala <adamc AT hcoop.net>
  • Cc: Damien Pous <Damien.Pous AT inria.fr>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] discriminate JMequalities
  • Date: Tue, 11 Aug 2009 13:55:27 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=FLTHPaN1W57TI6xHA3iL3rguknHxVCwXvGbRvkWpv+veZVFvW+VYRMmXmw3HU1uo5F OF3o0rB4z6YgUsM7W7mqpmMAm2e7JQ9KZxzYdyCqeWqp+AelqYMq5jio26Nqy61sMNcB tTovgoWIGxDryphuOgHIMLXNCbQYGAIXCi3hE=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Aug 11, 2009 at 4:35 AM, Adam 
Chlipala<adamc AT hcoop.net>
 wrote:
> This goal has a lot in common with a class of goals that often turn out
> unsolvable.  The crux of the theorem is in proving the inequality of types.
>  The only effective way I've yet found to prove type inequality is by
> demonstrating unequal cardinalities.  (Proving that a true [Prop] isn't
> equal to a false [Prop] is a special case of this.)

Is this one any more provable?

Goal forall (x : bool) (b : B x), b = (if x as x0 return (B x0) then
tt else ff).

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown





Archive powered by MhonArc 2.6.16.

Top of Page