The Coq mailing list

[jeanfrancois.monin AT rd.francetelecom.com]

Hi Lukasz,

It is possible to formalize a proof of ~nat==bool using cardinality arguments.
I recently did the exercise for finite sets, i.e. 
(finset n)==(finset m) -> n=m,
 then (A,B: Set; n,m:nat) (finite A n) -> (finite B m) -> n<>m -> ~A==B.

using:

Inductive finset : nat->Set :=
| F0 : (n:nat) (finset (S n))
| FS : (n:nat) (finset n) -> (finset (S n)).

Definition finite [A:Set; n:nat] := (equipollent A (finset n)).


We can deduce e.g. ~bool==(bool->bool), but not ~(finset (4))==(bool->bool).

My knowledge on models of CIC is weak, but I guess that there are
models of CIC where functions on finite sets are interpreted
extensionally, and it should even be possible to force the interpretation
of (finset (4)) to be equal to the interpretation of bool->bool.

Similarly, I guess that there are models where e.g. nat->bool is
interpreted by a countable set of constructive functions, and then
~nat==(nat->bool) cannot be proven.

But it is only an intuition, I hope that type theorists reading the list
will answer more appropriately.

Best regards,
  Jean-Francois

-- 
France Télécom R&D, DTL/TAL
2 av P. Marzin 22307 Lannion
tél : 02 96 05 26 79 - fax : 02 96 05 39 45

Lukasz Stafiniak wrote:
 > Hi List,
 > 
 > Can the following equality be decided?
 > 
 > Inductive typterm : Set->Set :=
 >    tybool : (typterm bool)
 >  | tynat : (typterm nat)
 >  | tyfun : (a, b : Set)(typterm a)->(typterm b)->(typterm (a->b)).
 > 
 > Definition deceq : (a,b:Set)(typterm a)->(typterm b)->
 > {a==b}+{~a==b}.
 > 
 > Is it anyway true, that ~nat==bool? Do you know any other means to decide
 > type equality (computationally)?
 > 
 > Thank You, Best Regards,
 > Lukasz
 > 
 > 
 > 
 > 
 > 
 > Uwaga! Do koñca sierpnia przed³u¿yli¶my promocje, do pakietów
 > wielostanowiskowych dok³adamy PenDrive  Sprawd¼:
 > http://www.mks.com.pl/promocja-mobile.html
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club