The Coq mailing list

[Vilhelm Sjöberg <vilhelm AT cis.upenn.edu>]

On Sun, Jan 29, 2012 at 10:49:37PM -0500, Wojtek Moczydlowski wrote:
>   Hello,
> 
> I've been looking for the answer to these questions, but couldn't find a
> decisive answer. Is it possible to prove in Coq that nat != bool? 

Yes, by a counting argument:
   
   Definition AtMostTwoElts (X : Type) :=
    exists x, exists y, forall (z:X), z = x \/ z = y.
   
   Lemma bool_2 : AtMostTwoElts bool.
     exists true. exists false. destruct z; auto.
   Qed.
   
   Lemma not_nat_2 : ~ AtMostTwoElts nat.
     unfold not. destruct 1 as [x [y H]].
     destruct (H 0); destruct (H 1); destruct (H 2); congruence.
   Qed.
   
   Theorem bool_neq_nat : bool <> nat.
    assert (H1 := bool_2). assert (H2 := not_nat_2).
    unfold not. intros H.
    rewrite H in H1. auto.
   Qed.
   
Similarly, you can prove e.g. nat<>(nat->bool) by reusing Cantor's proof
that the powerset of nat is uncountable.

However, this kind on counting arguments is the best you can do. It has been
shown ("homotopy type theory") that it is consistent to add as an axiom that
"if there is a bijection between two types, then those types are equal".
So e.g. the statement  
  nat<>nat*nat
is independent of the rest of Coq.

  Vilhelm Sjoberg