The Coq mailing list

[xinyu.jiang AT yale.edu]

Hi,

Thank you and everyone else. It my fault to ignore the apparent
mistake. In fact, what I want is not a such general (and wrong)
axiom. And the addition to Coq I need can be simplified and explained here:

Suppose I have a HOAS representation of a part of an (impredicative) assertion
language:

Inductive assert (t : Type) : Type :=
| avar : t -> assert t
| aand : assert t -> assert t -> assert t
| aexist : (t -> assert t) -> assert t.

Then I would like to have such an axiom:

"forall (f g : forall t, t -> assert t) (t : Type), f t = g t -> f = g"

which is a specific version of the wrong axiom I proposed.

The counter example which falsify the general version of the axiom does not
work here, because "F" is now "fun t => t -> assert t", which always returns 
an
inhabited type not isomorphic to "False". Would this kind of specific axioms
inconsistant to Coq again? Thanks very much!

                                         Xinyu Jiang

Quoting Chad E Brown 
<cebrown2323 AT yahoo.com>:

> Hi Xinyu, and all,
>
> The axiom as you gave it is inconsistent with Coq.  A proof is below.
>  Maybe you
> meant something else?
>
> Axiom pa : forall (F : Type -> Type) (f g : forall t, F t) (t :
> Type), f t = g t
> -> f = g.
>
> Definition f_ (X : Type) : Type := X -> False.
> Definition g_ (X : Type) : Type := False -> X.
>
> Goal False.
> cut (f_ = g_). intros e.
> cut (g_ True). rewrite <- e. auto.
> unfold g_. auto.
> apply (pa (fun X => Type) f_ g_ False).
> auto.
> Qed.
>
> - Chad
>
>
>
> ________________________________
> From: Xinyu Jiang 
>Â <xj27 AT pantheon.yale.edu>
> To: 
>Â coq-club AT inria.fr
> Sent: Wed, September 22, 2010 4:22:11 PM
> Subject: [Coq-Club] An axiom about parametricity
>
>
> 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.
>
>
>