The Coq mailing list

["Grant Jurgensen" <mailing-lists.coq AT grant.jurgensen.dev>]

Fabian,

You are absolutely right. If there exists some `x` such that `~ P x` and `~ Q x`, then the assumption holds, but the conclusion certainly doesn't follow.

I imagine we could then disprove the theorem by reflecting this observation to Types. Still, there seems something "almost" true about the theorem. I wonder if it would hold if we added an assumption that the forall-types are inhabited (which should eliminate this particular counterexample).

Thanks,

Grant

On Wed, Nov 3, 2021, at 11:46 AM, Fabian Kunze wrote:

Dear Grant Jurgensen,

I'm sceptical the theorem holds. At least if one looks at Prop instead 

of Type, and looks at it through the eyes of classical logic, the 

theorem looks like

forall (P Q : X -> Prop),

  ((forall x, P x) <-> (forall x, Q x))

   -> forall x, P x <-> Q x

Which does not hold: For example take P and Q that hold for different x 

and are false for at least one x.

Best,

Fabian

On 03/11/2021 16:38, Grant Jurgensen wrote:

> Hi all,

> 

> I was wondering if the following property is provable (or disprovable) 

> in Coq:

> 

> Theorem forall_eq_elim: forall (A: Type) (B C: A -> Type),

>    (forall a, B a) = (forall a, C a) ->

>    (forall a, B a = C a).

> 

> This is the converse of `forall_extensionality`, found in the standard 

> module `Coq.Logic.FunctionalExtensionality`. Assuming functional 

> extensionality, this `forall_eq_elim` property essentially states the 

> injectivity of the forall binder.

> 

> The property appears very intuitive to me, but I don't see any proof 

> path, even assuming functional extensionality. I'm guessing it would be 

> sound to axiomatize it, but it also seems specific enough that there 

> should be a more palatable/generalized alternative to axiomatize.

> 

> For what its worth, the reason I first considered this property above is 

> because it appeared necessary in order to prove the following fact 

> concerning heterogeneous equalities:

> 

> Theorem JMeq_f :

>    forall A (B: A -> Type) (C: A -> Type) (f: forall a, B a) (g: forall 

> a, C a),

>      JMeq f g ->

>      forall x, JMeq (f x) (g x).

> 

> Thanks,

> Grant Jurgensen