coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] discriminate JMequalities

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

[Coq-Club] discriminate JMequalities, Damien Pous
- Re: [Coq-Club] discriminate JMequalities, Adam Chlipala
  - Re: [Coq-Club] discriminate JMequalities, Taral
    - Re: [Coq-Club] discriminate JMequalities, Hugo Herbelin