Доказать, что два жителя в Проп не равны? - PullRequest
Новая
       82

Доказать, что два жителя в Проп не равны?

1 голос
/ 16 апреля 2020

Можно ли иметь некоторые A, B : Prop такие, что мы можем предоставить доказательство: 

Section QUESTION.
A: Prop := <whatever you want> .
B : Prop := <whatever you want> .
Theorem ANeqB: A <> B.
Proof.
<a proof of this fact>
Qed.

Интуитивно, я думаю, нет, поскольку это позволило бы нам "отличить guish" между доказательствами, но нельзя делать это без вычислений на A или B. Однако Coq явно запрещает нам проверять доказательства, поскольку они должны быть удалены во время выполнения. Таким образом, только Prop должен иметь возможность проверять Prop (из-за стирания), но проверка всегда вычислительная, поэтому Prop не может проверять Prop. Следовательно, ничто не может проверить Prop, и приведенная выше теорема ANeqB не может быть доказана.

  • Если приведенное выше объяснение неверно, не могли бы вы объяснить, почему оно это так?
  • Если теорема ANeqB не может быть доказана, можете ли вы указать мне доказательство этого факта?
  • Если теорема ANeqB может быть доказана , можете ли вы сказать мне, где моя интуиция терпит неудачу?

РЕДАКТИРОВАТЬ:

Меня просто поразило, что, поскольку мы можем принять доказательство неуместности в качестве дополнительной аксиомы (Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.), теорема ANeqB не может быть доказано в Coq - если бы это было возможно, было бы неразумно допустить proof_irrelevance в качестве дополнительной аксиомы.

Это сдвигает мой вопрос, тогда:

  • Можно ли доказать ANeqB для некоторых жителей A и B? (proof_irrelevance сильнее: говорится, что мы не можем доказать A <> B [на самом деле, более сильное утверждение, что мы можем доказать A = B] для все A, B)
  • Если нет, то может ли кто-нибудь предоставить sh доказательство того, что ANeqB не может быть доказано в системе аксиомати c на основе Кока?

1 Ответ

1 голос
/ 16 апреля 2020

Я думаю, вы думаете о чем-то другом. Prop само по себе не является доказательством неуместным. Это определенно имеет различимые элементы. Например, True <> False. 

Section QUESTION.
Definition A: Prop := True.
Definition B : Prop := False.

Theorem ANeqB: A <> B.
Proof.
  unfold A, B.
  intro p.
  destruct p.
  exact I.
Qed.

End QUESTION.

Вместо этого, это элементов из Prop, которые могут быть несущественными для доказательства. В аксиоме 

Axiom proof_irrelevance: forall (P: Prop) (p q: P), p = q.

p и q сами не являются элементами Prop, а скорее элементами некоторого элемента Prop.

...