The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

And here's a proof that not_all_ex_not_pred is equivalent to the axiom
of choice, modulo propositional excluded middle:

Require Import Classical.

Definition choice := forall (A B:Type) (R:A->B->Prop),
  (forall x:A, exists y:B, R x y) ->
  exists f:A->B, forall x:A, R x (f x).

Definition dep_type_choice := forall (A:Type) (B:A->Type),
  (forall x:A, inhabited (B x)) ->
  inhabited (forall x:A, B x).

Lemma dep_type_choice_impl_choice :
  dep_type_choice -> choice.
Proof.
intros ? A B R ?.
pose proof (H A (fun x:A => { y:B | R x y })).
refine (let _ := H1 _ in _).
intros.
destruct (H0 x) as [y].
constructor.
exists y; trivial.

destruct _H as [f].
exists (fun x:A => proj1_sig (f x)).
intros; apply proj2_sig.
Qed.

Lemma choice_impl_dep_type_choice :
  choice -> dep_type_choice.
Proof.
intros ? A B ?.
set (B' := sigT B).
set (R := fun (x:A) (y:B') => projT1 y = x).
pose proof (H A B' R).
refine (let _ := H1 _ in _).
intros.
destruct (H0 x) as [y].
exists (existT B x y).
reflexivity.

destruct _H as [f].
constructor.
exact (fun x:A => eq_rect _ _ (projT2 (f x)) _ (H2 x)).
Qed.

Ltac suppose_not := apply NNPP; intro.

Lemma not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P 
n.
Proof.
intros.
suppose_not.
contradict H.
intros.
suppose_not.
contradict H0.
eauto.
Qed.

Definition not_all_ex_not_pred :=
 forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) ->
exists n : U, P n -> False.

Lemma not_all_ex_not_pred_impl_dep_type_choice :
  not_all_ex_not_pred -> dep_type_choice.
Proof.
intros ? A B ?.
suppose_not.
pose proof (H A B).
refine (let _ := H2 _ in _).
intros.
contradict H1.
eauto.
destruct (_H) as [x].
destruct (H0 x) as [y].
auto.
Qed.

Lemma dep_type_choice_impl_not_all_ex_not_pred :
  dep_type_choice -> not_all_ex_not_pred.
Proof.
intros ? U P ?.
suppose_not.
assert (inhabited (forall n:U, P n)).
apply H.
intros.
suppose_not.
contradict H1.
exists x.
intros; contradict H2.
auto.

destruct H2 as [f].
auto.
Qed.
-- 
Daniel Schepler

On Wed, May 14, 2014 at 12:27 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> You'd probably need to assume the axiom of choice as well, in order to
> say anything about whether (forall n:U, P n) is empty or not.
> --
> Daniel Schepler
>
> On Wed, May 14, 2014 at 11:22 AM, Eddy Westbrook 
> <westbrook AT kestrel.edu>
>  wrote:
>> All,
>>
>> The library Coq.Logic.Classical_Pred_Type gives a proof, using 
>> (propositional) excluded middle, that the negation of a forall is an 
>> exists:
>>
>> Lemma not_all_ex_not :
>>  forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ 
>> P n.
>>
>> Does anyone know if the version of this that makes P predicative, using 
>> Type, is provable as well? That is, I am trying to prove:
>>
>> Lemma not_all_ex_not_pred :
>>  forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) -> exists 
>> n : U, P n -> False.
>>
>> Thanks,
>> -Eddy