The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Daniel Schepler wrote:
> On Wednesday 30 March 2011 07:13:22 David Baelde wrote:
>    
> > For example, any function of type (forall A:Type, A ->  bool) must be
> > equal (at least extensively) to a constant function. It also seems
> > that there is no model of (subsets) of the CIC that doesn't force
> > parametricity. But do we know whether this is ruled out by the
> > calculus itself? In other words, can we prove from inside Coq that any
> > function of type (forall A:Type, A ->  bool) is extensively equal to
> > some constant function?
> >      
> No, if you add
>
> Axiom classic_dec: forall P:Prop, {P} + {~P}.
>
> then you can define
>
> Definition inhabited_bool (A:Type) : bool :=
>    if classic_dec (inhabited A) then true else false.
>    

Is this function really a counterexample?  It doesn't include the 
argument of type [A] from the original question.  That seems to play an 
important role; a function whose argument type is an unprovable 
proposition can certainly be considered to be "constant" at _any_ return 
value.  In particular, it can be considered to be constant at [true].  
The provable propositions naturally always lead to returning [true], 
too, with this version:

Definition inhabited_bool (A:Type) (_ : A) : bool :=
  if classic_dec (inhabited A) then true else false.


I can see how the frightening [classic_dec] function allows you to do 
very un-parametric things (and compute uncomputable functions!); I'm 
only questioning whether your example answers the original question.

Is [classic_dec] really consistent with CIC?  It's not among the 
consistent axioms listed in the Coq FAQ.  Maybe it falls out obviously 
from the standard boolean models; if so, that just leads me to distrust 
those models somehow. ;)