时间戳

首页 > 解决方案 > 如何在 Coq 中证明 (p -> q) -> (~ p \/ q)

coq - 如何在 Coq 中证明 (p -> q) -> (~ p \/ q)

问题描述

我正在尝试使用 Axiom 在 Coq 中证明 (p -> q) -> (~ p / q)：

Axiom tautology : forall P:Prop, P \/ ~ P.

我正在尝试通过应用 p -> q 将 ~ p / q 转换为 ~ p / p。所以做这样的事情：

Theorem Conversion: forall (p q: Prop),(p -> q) -> (~ p \/ q).
Proof.
  intros p q.
  intros p_implies_q.
  (do something here, change ~p\/q into ~p\/p)
  apply tautology...

但我不知道我该怎么做。如果有更好的方法可以做到这一点，请告诉我。谢谢！。

标签： coq

解决方案

使用你的一种方法是使用tautologytactic destruct。这允许您减少到p正确和p不正确的情况。

Axiom tautology : forall P:Prop, P \/ ~ P.

Theorem Conversion: forall (p q: Prop),(p -> q) -> (~ p \/ q).
Proof.
  intros p q.
  intros p_implies_q.
  destruct (tautology p) as [p_true | p_not_true].
  - (* prove ~p \/ q using p *)
  - (* prove ~p \/ q using ~p *)
Qed.

你能看到~p \/ q在每种情况下如何证明吗？

推荐阅读