如何使用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不为真，例如，如果p为false，则p → ¬ 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也可以用来证明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