The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello,

> Is it anyway true, that ~nat==bool? Do you know any other means to decide
> type equality (computationally)?

If by "deciding type equality (computationally)" you mean finding a function
of type (A,B:Set)A==B\/~A==B, I am almost sure that this is not possible.
However, you can still prove that nat is not bool by introducing a property 
that is satisfied by one of the sets, but not by the other. Here is an 
example of such a property.

Cheers,
Eduardo Gimenez.

================================
Definition Cardinal2 [A:Set] := 
 (EX f : A -> bool | (x,y:A)(f x)=(f y)->x=y).

Lemma boolHasCardinalTwo : (Cardinal2 bool).
Proof.
Exists [x:bool]x;Auto.
Qed.

Lemma TwoOfThreeAreEqual : 
  (f:nat->bool)(f (0))=(f (1))\/(f (0))=(f (2))\/(f (1))=(f (2)).
Proof.
Intros;Case (f (0));Case (f (1));Case (f (2));Auto.
Qed.

Lemma natDoesNotHaveCardinalTwo : ~(Cardinal2 nat).
Proof.
Unfold Cardinal2; Red; Intros [f Inj].
Specialize (TwoOfThreeAreEqual f).
Intros [Abs|[Abs|Abs]].
 Absurd 'N:0 '='N:1 '; Auto; Discriminate.
 Absurd 'N:0 '='N:2 '; Auto; Discriminate.
 Absurd 'N:1 '='N:2 '; Auto; Discriminate.
Qed.

Theorem DiscriminateNatAndBool : ~nat==bool.
Proof.
Red;Intro Abs.
Absurd (Cardinal2 bool).
 Rewrite <- Abs;Apply natDoesNotHaveCardinalTwo.
 Apply boolHasCardinalTwo.
Qed.
============================================