The Coq mailing list

[Arthur Chargu�raud <arthur.chargueraud AT inria.fr>]

> Hi all,
>   I would like to add an axiom somehow like:
>
>   "forall (F : Type -> Type) (f g : forall t, F t) (t : Type), f t = g
> t -> f = g"
>
>   to Coq. It seems to be reasonable because of the parametricity of
> Coq's logic. But I wonder if the axiom is indeed consistent with Coq.
> If so, would it collide against other axioms like exclusive of the
> middle? If not, what would the counter example be like? Thanks very much.

Hi,

Your parametricity axiom is inconsistent with the strong
excluded middle (which follows, in particular, from Hilbert's
epsilon used in conjunction with excluded middle). In Coq
without any axiom, one can prove the fact "bool <> unit".
With a strong excluded middle, one can write a function that
takes a type as argument and then tests whether this argument
is equal to "unit". This contradicts your axiom, as shown
through the Coq proof below.

Now, I do not know whether your axiom is sound if you
consider only the excluded middle and not the strong
excluded middle. Maybe someone else knows.
It just seems to me that it is generally unsafe to try
and exploit Coq parametricity result inside Coq itself.

Arthur



(*----------*)

Axiom parametricity :
  forall (F : Type -> Type) (f g : forall t, F t) (t : Type),
  f t = g t -> f = g.

Axiom classicT : (* the strong excluded middle *)
  forall (P:Prop), {P} + {~ P}.

(*----------*)

Lemma bool_not_unit : bool <> unit :> Type.
Proof.
  set (P := fun (t:Type) =>
    exists a:t, forall b:t, b = a).
  intros H.
  assert (P unit).
    exists tt. intros []. reflexivity.
  assert (~ P bool).
    destruct (classicT (P bool)) as [HP|HP].
      apply False_ind. destruct HP as [x Hx].
        specialize (Hx (negb x)). destruct x; discriminate.
      apply HP.
  apply H1. rewrite H. apply H0.
Qed.

(*----------*)

Ltac caseif :=
  match goal with |- context [if ?X then _ else _] =>
    let x := fresh in set (x:=X); destruct x end.
 
(*----------*)

Definition f (t:Type) :=
  if classicT (t = unit) then True else False.

Definition g (t:Type) :=
  True.

Lemma contradiction : False.
Proof.
  assert (H1: f = g).
    apply parametricity with (t:=unit). unfold f, g. caseif.
      reflexivity.
      apply False_ind. apply n. reflexivity.
  assert (H2: f bool <> g bool).
    unfold f, g. caseif.
      apply False_ind. apply bool_not_unit. auto.
      intros M. rewrite M. apply I.
  apply H2. rewrite H1. reflexivity.
Qed.
    
(*----------*)