The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Whoops, I accidentally sent this reply just to Adam instead of the whole list...

---------- Forwarded message ----------
From: Daniel Schepler <dschepler AT gmail.com>
Date: Wed, Mar 30, 2011 at 12:27 PM
Subject: Re: [Coq-Club] Parametricity
To: Adam Chlipala <adam AT chlipala.net>

On Wed, Mar 30, 2011 at 10:43 AM, Adam Chlipala <adam AT chlipala.net> wrote:

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:

Ah, sorry, I misread the desired type.  Here's one using classic_dec which actually answers the question:

Require Import Classical.
Require Import Description.
Require Import Setoid.

Lemma classic_bool: forall P:Prop, {b:bool | if b then P else ~P}.
Proof.
intro P.
apply constructive_definite_description.
rewrite <- unique_existence.
split.
destruct (classic P).
exists true; trivial.
exists false; trivial.
intros [|] [|]; tauto.
Qed.

Definition classic_dec: forall P:Prop, {P} + {~P} :=
  fun P => match (classic_bool P) with
  | exist true p => left _ p
  | exist false np => right _ np
  end.

(* if A is bool, return the identity function, otherwise return the constant true function *)
Definition nonconst_on_bool: forall A:Type, A->bool :=
  fun A => match (classic_dec ((bool:Type)=A)) with
  | left p => match p in (_=T) return (T->bool) with
     | eq_refl => fun b:bool => b
     end
  | right np => fun _ => true
  end.

Lemma nonconst_on_bool_indeed_nonconst:
  nonconst_on_bool bool true <> nonconst_on_bool bool false.
Proof.
intro e.
cut (forall b:bool, nonconst_on_bool bool b = b).
intro H.
congruence.
intro b.
unfold nonconst_on_bool.
destruct classic_dec.
replace e0 with (eq_refl (bool:Type)) by apply proof_irrelevance.
reflexivity.
contradiction n; reflexivity.
Qed.

Print Assumptions nonconst_on_bool_indeed_nonconst.

As for the question on consistency, the Print Assumptions returns just classic and constructive_definite_description.  If the combination of those is inconsistent, which I highly doubt, then much of the work I've been doing reduces to triviality...
--
Daniel Schepler