Поднимите экзистенциалы в Coq

Question

Может ли эта лемма быть доказана в Coq?

Lemma liftExists : forall (P : nat -> nat -> Prop),
  (forall n:nat, exists p:nat, P n p)
  -> exists (f : nat -> nat), forall n:nat, P n (f n).

Простое destruct не компилируется, потому что мы не можем исключить объект exists p:nat, P n p в виде Prop для получения функции f в сортировке Set.

Если Coq не может доказать эту лемму, то в чем смысл forall n:nat, exists p:nat, P n p?В конструктивной математике это означало бы существование функции f, но у меня сложилось впечатление, что мы никогда не увидим эту функцию f в Coq, даже в виде Prop, как выражено выше.

Answer 1

Это не доказуемо в Coq из-за ограничения на удаление Prop в Set.Что касается философского «значения», я не уверен, есть ли у кого-нибудь очень хорошая история об этом.Обитатели forall n:nat, exists p:nat, P n p - это функции, возвращающие пару p и доказательство, но в дополнение они являются функциями, которые можно игнорировать при компиляции программ, поскольку вы знаете, что ничто не будет смотреть на возвращенное значение.

Так что отчасти эта система «Пропорция против Сета» является способом более эффективной компиляции программ, но на самом деле это также используется для логических свойств.В Coq тип Prop является непредсказуемым, а тип Set - нет, и, тем не менее, непротиворечиво принять закон исключенной середины для реквизита в качестве аксиомы и доказать, что это согласованно, вы можете обратиться к « proof-неактуальная модель", где вы интерпретируете типы в Props как наборы, игнорируя всю информацию, кроме того, обитаемы они или нет.С точки зрения классической логики (где все, что вас волнует, это истинные ценности), это имеет смысл, но если вы заинтересованы в конструктивной математике, это немного странно!