The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Hello,

The distinction between Prop and Set provides several features,
especially extraction and different computing capabilities in
these 2 sorts; but they seem to be independant, are they?

Let us consider "weak Booleans" defined in Prop.

Inductive pbool : Prop : f : pbool | t : pbool.

It is well known that f <> t cannot be proved by the 
usual trick, since strong elimination is not allowed here.

Now let us assume it axiomatically: 

Axiom discr_pbool : f <> t.

1) Is it safe to add this axiom?
(Without assuming proof irrelevance at the same time, of course).

I think that the answer is yes, because if we could get a
contradiction in a given development D (without further axiom), we
would as well derive False in the translation D' of D, where all Props
are replaced with Set, and without any axiom.

2) Is it still impossible to derive a test function on pbool?
For instance it is easy to define 
Theorem eq_pbool_dec : forall x y:pbool, x=y \/ x<>y.
while the similar testing function seems impossible to define
(at least using naive attempts).
Definition eq_pbool_test : forall x y:pbool, {x=y}+{x<>y}.

  JF

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46