时间戳

首页 > 解决方案 > 如何在 Coq 中证明逻辑等价？

logic - 如何在 Coq 中证明逻辑等价？

问题描述

如何使用 Coq 证明以下内容？

(q V p) ∧ (¬p -> q) <-> (p V q)。

我的尝试

Lemma work: (forall p q: Prop, (q \/ p)/\(~p -> q) <-> (p \/ q)).
Proof.
intros p q.
split.
intros q_or_p_and_not_p_implies_q.
intros p_or_q.
split.

标签： logiclogical-operatorscoqdiscrete-mathematics

解决方案

这是一个非常相似的陈述的证明。p \/ q为了q \/ p匹配您给出的语句，需要做更多的工作来交换第一个。

Theorem work : (forall p q : Prop, (p \/ q) /\ (~p -> q) <-> (p \/ q)).
Proof.
  intros p q.
  split.

  (* Prove the "->" direction *)
  intros given.
  destruct given as [p_or_q _].
  exact p_or_q.

  (* Prove the "<-" direction *)
  intros p_or_q.
  refine (conj p_or_q _).
  case p_or_q.
    (* We're given that p is true, so ~p implies anything *)
    intros p_true p_false.
    case (p_false p_true).
    (* We're given that q is true *)
    intros q_true p_false.
    exact q_true.
Qed.

推荐阅读