The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 22 Sep 2010 22:22:11 +0800,
Xinyu Jiang 
<xj27 AT pantheon.yale.edu>
 a écrit :

> 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.

That is inconsistant with many logics:

Variables f g: Type -> nat.

Hypothesis f_spe1: 0 = f bool.
Hypothesis f_spe2: 1 = f nat.
Hypothesis g_spe1: 0 = g bool.
Hypothesis g_spe2: 0 = g nat.

Variable Absurd: forall (F : Type -> Type) (f g : forall t, F t)
         (t : Type), f t = g t -> f = g.

Goal False.
 generalize (Absurd (fun (_: Type) => nat) f g bool).
 destruct f_spe1; destruct g_spe1.
 intro.
 assert (K := H (refl_equal _)).
 assert (L := g_spe2).
 destruct K.
 destruct f_spe2.
 discriminate.
Qed.

In fact your axioms states that if "f" and "g" are equal in one point,
then they are equal; it looks a little like to "proof irrelevance" but
in "Type".

But I know that axiom-free inhabitants of "Type -> Type" in Coq are
constant functions, as matching is not allowed for Type;
that means that such functions cannot inspect their argument to produce
something depending on it; and can only be constant functions.

As you cannot produce axiom-free counter examples of
"CST: forall (F: Type -> Type) (f: forall t, F t)
     (t1 t2: Type), f t1 = f t2",
I assume that "CST" is a weird but would be consistant if were well
typed (let us say using JMeq).
And with such a lemma, you might prove your axiom, using
extensionnality.

In brief, I think that if "CST" and "Extensionnality" are consistant,
then your axiom should be.

But as I am pretty sure that
Variables f g: Type -> nat.

Hypothesis f_spe1: 0 = f bool.
Hypothesis f_spe2: 1 = f nat.
Hypothesis g_spe1: 0 = g bool.
Hypothesis g_spe2: 0 = g nat.

is consistent with Coq (axiom-free) logic, your axiom certainly cannot
be proved in Coq.