Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] inequality of inductive types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inequality of inductive types


chronological Thread 
  • From: muad <muad.dib.space AT gmail.com>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] inequality of inductive types
  • Date: Sun, 15 Mar 2009 06:54:38 -0700 (PDT)
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

It's possible to prove nat and bool are different. For example:

Definition P (T : Set) : Prop :=
 exists x : T, exists y : T, exists z : T,
  x <> y /\ x <> z /\ y <> z.

P says that this type has 3 distinct elements, that's true for nat but false
for bool.

I think it's impossible to prove that:

Inductive answer := yes | not.

is different to bool, though.

-- 
View this message in context: 
http://www.nabble.com/inequality-of-inductive-types-tp22523222p22523432.html
Sent from the Coq mailing list archive at Nabble.com.





Archive powered by MhonArc 2.6.16.

Top of Page