coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] discriminate JMequalities, Taral
- Re: [Coq-Club] discriminate JMequalities,
Adam Chlipala
Archive powered by MhonArc 2.6.16.