Доказательство Coq теоремы, которая превращает формулу, содержащую y, в формулу, содержащую f (x)

Question

Я пытаюсь доказать:

forall (T : Type) (U : Type) (P : T -> U -> Prop),
  (forall (x : T), exists (y : U), P x y)
    -> (exists (f : T -> U), forall (x : T), P x (f x))

На простом английском языке я пытаюсь выразить способность превращать y в f(x) в формуле. Например, изменив y = x + 1 на f(x) = x + 1.

Доказательство цели с перевернутой стрелкой импликации (превращение f(x) в y) занимает 4 строки. Однако с этой целью я не могу придумать, что делать после intros.

Я даже не уверен, что это возможно в Coq. Если нет, то есть ли лучший способ выразить то, что я пытаюсь сделать?

Answer 1

Ваш результат является формой аксиомы выбора и не может быть доказан в Coq без дополнительных аксиом. Проблема в том, что для построения f необходимо извлечь элемент y : U из доказательства exists y, P x y. Это запрещено в Coq по замыслу, чтобы гарантировать, что доказательства не имеют вычислительного значения.

Способ обойти это ограничение состоит в том, чтобы заменить обычный экзистенциал его соответствующим в вычислительном отношении аналогом. Затем мы получаем то, что Боб Харпер называет теоремой выбора :

Goal forall (T : Type) (U : Type) (P : T -> U -> Prop),
  (forall (x : T), { y : U | P x y })
    -> (exists (f : T -> U), forall (x : T), P x (f x)).
Proof.
intros T U P H.
exists (fun x => proj1_sig (H x)).
intros x.
now apply proj2_sig.
Qed.