The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

Ciao Claudio,

> could I prove that two "different" inductive types are not equal in Type?

You can, provided they are really different !  (see below)

> example: ~nat==bool is provable? If yes, how? If no, why really?

To prove it, you have to exhibit a property verified by bool and
(provably) not by nat.

One such property is "having at most two elements", formaly:

Definition P := [X:Set](EX x:X | (EX y:X | (z:X)z=x\/z=y)).

This predicate is easily provable for bool, and proven false for nat.




I should have let you do the proof, since it is a good and fun
exercise. But I could not resist !  :)

A possible solution is below. There sure are shorter ones.


Note however that if you had redefined an inductive type isomorphic to
the booleans but with a new name:

Inductive calcio_bo : Set :=
  rosso : calcio_bo  |  azzuro : calcio_bo.

Then you could not prove ~bool==calcio_bo. Actually in former versions of
Coq, these two definitions were convertible (and thus equal).


Cheers,




Benjamin





>>>>>>>>>>> Spoiler 
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>>>>>>>>>








Lemma Pb : (P bool).
Exists true; Exists false; Intros b; Elim b; Auto.
Qed.


Lemma Pnat : ~(P nat).
Unfold not; Destruct 1; Intros x; Destruct 1; Intros y hy.
Elim (hy O); Intros; Elim (hy (S O)); Intros; Elim (hy (S (S O)));
  Intros.
Cut O=(S O); Try Discriminate; EAuto .
Apply trans_equal with x; Auto.
Cut O=(S O); Try Discriminate; Apply trans_equal with x; Auto.
Cut O=(S (S O)); Try Discriminate; Apply trans_equal with x; Auto.
Cut (S O)=(S (S O)); Try Discriminate; Apply trans_equal with y; Auto.
Cut (S O)=(S (S O)); Try Discriminate; Apply trans_equal with x; Auto.
Cut O=(S (S O)); Try Discriminate; Apply trans_equal with y; Auto.
Cut O=(S O); Try Discriminate; Apply trans_equal with y; Auto.
Cut O=(S O); Try Discriminate; Apply trans_equal with y; Auto.
Qed.



Goal ~nat==bool.
Unfold not; Intros; Apply Pnat.
Rewrite H.
Exact Pb.






> 
>                                                       T.I.A.
>                                                       C.S.C.
> 
> -- 
> -----------------------------------------
> Real Name: Claudio Sacerdoti Coen
> Address: via del Colle n.6
>        S. Lazzaro di Savena (BO)
>        Italy
> e-mail:  
> sacerdot AT cs.unibo.it
> -----------------------------------------
>