Утвердить предложение о нескольких свидетелях - PullRequest
Новая
       7

Утвердить предложение о нескольких свидетелях

0 голосов
/ 08 января 2019

Предположим, у меня есть экзистенциальное предложение P о натуральных числах, например 

Definition P (n : nat) : Prop
:= exists k:nat, True.

Предположим также, что я доказал P для всех чисел, 

Lemma allP : forall n : nat, P n.
Proof.
  intros. exists 0. trivial.
Defined.

Тогда у меня есть свидетель k для всех n (k всегда равен 0 в предыдущем примере), и я хочу сказать что-то обо всех k s, например, 

Definition allWitnessesBelowOne : Prop
  := forall n : nat,
    match allP n with
    | ex_intro _ k _ => k <= 1
    end.

кроме того, что это не компилируется, я получаю следующую ошибку: 

Incorrect elimination of "allP n" in the inductive type "ex":
the return type has sort "Type" while it should be "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.

Я не понимаю, что здесь типа Type, все выглядит в Prop. Я только пытаюсь создать доказательство, почему Coq не счастлив? В моей полной задаче P гораздо сложнее, и имеет смысл доказать что-то обо всех свидетелях.

1 Ответ

0 голосов
/ 08 января 2019

Разработка комментария @ eponier, когда вы пишете 

Definition allWitnessesBelowOne : Prop
  := forall n : nat,
    match allP n with
    | ex_intro _ k _ => k <= 1
    end.

вы на самом деле пишете 

Definition allWitnessesBelowOne : Prop
  := forall n : nat,
    match allP n return Prop with
    | ex_intro _ k _ => k <= 1
    end.

Если у вас есть return Prop, тип возврата Prop имеет тип Type, в то время как он должен иметь тип Prop, чтобы удовлетворять ограничению исключения. По сути, если вы снимите это ограничение, вы сделаете Coq несовместимым с классической логикой. См., Например, официальную документацию Prop, Неправильное исключение X в индуктивном типе "или": или CPDT в юниверсах .

Другой способ взглянуть на это состоит в том, что, если у вас нет аксиом, должна быть возможность интерпретировать все Prop s как либо одноэлементный набор (если они истинны), либо пустой набор (если они есть). ложный). Не существует непостоянной функции из одноэлементного набора, поэтому вы не можете определить какие-либо интересные свойства для доказательства exists k : nat, True.

Самый простой способ исправить это - прекратить использование Prop. Вместо этого используйте типы сигма (sig), чтобы сказать: 

Definition P (n : nat)
:= { k : nat | True }.

Lemma allP : forall n : nat, P n.
Proof.
  intros. exists 0. trivial.
Defined.

Definition allWitnessesBelowOne : Prop
  := forall n : nat,
    match allP n with
    | exist _ k _ => k <= 1
    end.

Альтернативное определение этого последнего: 

Definition allWitnessesBelowOne : Prop
  := forall n : nat,
    proj1_sig (allP n) <= 1.

Другое, что вы можете сделать, это то, что вы можете делать все в стиле продолжения: 

Definition P (n : nat) : Prop
:= exists k:nat, True.

Lemma allP : forall n : nat, P n.
Proof.
  intros. exists 0. trivial.
Defined.

Lemma allWitnessesBelowOne_cps
      (n : nat)
      (Result : P n -> Prop)
  : (forall k pf, k <= 1 -> Result (ex_intro _ k pf))
    -> Result (allP n).
Proof.
  unfold allP; intro H.
  apply H; repeat constructor.
Defined.

Здесь Result определяет Prop, который вы в конечном итоге будете доказывать. Эта лемма говорит, что всякий раз, когда вы пытаетесь доказать Result о allP n, вы можете предположить, что вы доказываете Result о значении, равном <= 1. Однако это довольно сложно, поэтому я бы предложил просто отбросить Prop, если вам удастся это сделать.

...