theorem-proving - 如何使用 LEAN 证明命题逻辑中的两个陈述？

Question

LEAN 教程第 3 章末尾的两个证明我仍然在努力（因此阻止我进一步阅读手册）如下：

theorem T11 : ¬(p ↔ ¬p) := sorry

为此，我试图证明正确的含义在这一点上停止了：

theorem T11R : ¬(p → ¬p) := 
begin 
    assume hyp : p → ¬ p, 
    cases (em p) with hp hnp, 
    exact (hyp hp) hp, 
    exact sorry 
end

显然我还不知道如何使用¬p. 也不知道如何显示左边的含义。另一个是这样的：

theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
begin
    intros porqr, sorry
end

我应该使用（作为正确的含义）来显示以下内容：

theorem T2 : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) := 
begin    
    have goR : ((p ∨ q) → r) → (p → r) ∧ (q → r), from T2R p q r,
    have goL : (p → r) ∧ (q → r) → ((p ∨ q) → r), from T2L p q r,
    exact iff.intro (goR) (goL)
end

在这里，我得到了左侧：

theorem T2L : (p → r) ∧ (q → r) → ((p ∨ q) → r) := 
begin
    intros prqr,
    assume porq : p ∨ q,
    exact or.elim porq prqr.left prqr.right
end

Answer 1

theorem T11R不为真，例如 if pis falsethenp → ¬ p为真。

¬(p ↔ ¬p)不等于(¬ (p → ¬ p)) ∧ ¬ (¬ p → p); 它相当于¬ ((p → ¬ p) ∧ (¬ p → p))，这是不同的。

因为theorem T2R如果你使用这个split策略，它会给你两个目标，一个用于and. 您可以使用left和right策略将目标p ∨ q变为p或q。定理or.inl和or.inr也可以用来证明 a or。

这是一个证明T2R

theorem T2R : ((p ∨ q) → r) → (p → r) ∧ (q → r) := 
begin
    intros porqr,
    split,
    { assume hp : p,
      apply porqr,
      left,
      exact hp },
    { assume hq : q,
      apply porqr,
      right,
      exact hq },
end