Как «исключить» в Coq работу над квантором существования?

Question

Я смущен Коком по пути, связанным с экзистенциальной количественной оценкой.

У меня есть предикат P и предположение H

P : nat -> Prop 
H : exists n, P n 

в то время как текущая цель состоит в том (независимо)

(Some goal) 

Если я хочу, чтобы создать экземпляр п в Н, Я сделаю

elim H. 

Однако после ликвидации текущая цель

forall n, P n -> (Some goal) 

Похоже, что Coq преобразует квантор существования в универсальный. Я знаю, что (forall a, P a -> Q a) -> ((существует a, P a) -> Q a) из моих ограниченных знаний по логике первого порядка. Но обратное предложение кажется неправильным. Если «forall» одно и «существует» не эквивалентны, почему Coq сделает такое преобразование?

Удаляет ли «изгнание» в Coq цель, чтобы доказать ее? Или кто-нибудь может показать, почему ((существует a, P a) -> Q a) -> (forall a, P a -> Q a) выполняется в логике первого порядка?

Answer 1

Может быть недостающим ключом является то, что цель:

forall n, P n -> (Some goal) 

следует читать как:

FORALL п, (Р п -> (Некоторые цели))

и не как :

(forall n, P n) -> (Some goal) 

То есть, цель вы получаете только дает произвольное n и доказательство P n, который действительно является правильным способом устранить экзистенциальный (вы не знаете значения свидетеля, поскольку это может быть любое значение, которое делает P правдой, вы просто узнаете, что есть n и что P n содержит).

Наоборот, последний предоставит вам функцию, которая может построить P n для любого n, который вы передаете, что действительно более сильное утверждение, чем тот, который у вас есть.