The Coq mailing list

[Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>]

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