Lean语言数学之旅—

发布于

2025年1月12日

上一章介紹了Lean的一些基本概念和環境配置。本章開始，我們將介紹如何證明一個定理。讓我們先從基礎的命題邏輯開始。

命題邏輯涉及命題與命題之間的關係，有時又被稱為零階邏輯。

命題指的是一個可以判斷真假的陳述句，根據其真假命題可以分為真命題或假命題。例如

√2是無理數
有無窮多個自然數
矩陣乘法沒有交換律
2012年，世界末日到來

以上各種陳述句或真或假，都屬於命題。

section
  variable (p q r : Prop)

在Lean中，命題的類型為Prop。上面的代碼聲明了三個命題p、q和r。

定義在命題上的基本運算包括與運算、或運算、非運算等。在Lean中，And運算即命題的與運算：

  #check And     -- 與運算
  -- 輸出為：And (a b : Prop) : Prop
  #check And p q -- 表示p和q都是真命題
  #check p ∧ q   -- And p q 的另一種寫法

上面的代碼中演示了“與”的運算，其中#check用於輸出算式的類型。與運算可以使用And或∧符號構造，符號∧可以在編輯器中用\and打出。

類似的，下面是或運算、非運算等運算的用法。

  #check Or     -- 或運算
  -- 輸出為：Or (a b : Prop) : Prop
  #check Or p q -- 表示p或q其中之一是真命題
  #check p ∨ q  -- Or p q 的另一種寫法
  -- ∨ 可以在編輯器中用\or打出

  #check Not    -- 非
  #check Not p  -- 表示p是假命題
  #check ¬p     -- Not p 的另一種寫法
  -- ¬ 可以在編輯器中用\not打出

  #check p → q  -- 蘊含關係，表示如果p為真，那麼q也為真
  -- → 可以在編輯器中用\to或者\r打出
  #check p ↔ q  -- 表示p成立當且僅當q成立
  -- ↔ 可以在編輯器中用\lr打出

end

2.1 公理

公理是不言自明的真命題，是不需要證明的。

下面的例子中，我在crazy_axioms命名空間下聲明了一個公理：

namespace crazy_axioms
  -- 聲明了一個命題p
  variable (p : Prop)
  -- 聲明了一個公理em
  -- 該公理的含義是：對於任意的命題p，p要麼為真，要麼為假。
  -- 它被叫做排中律（Law Of Excluded Middle）
  axiom em : p ∨ ¬p
end crazy_axioms

#check crazy_axioms.em
-- 類型為：em (p : Prop) : p ∨ ¬p

公理em的類型是p ∨ ¬p，表示對於任意的命題p，p要麼為真，要麼為假。

我不提供em的證明，因為它是公理。你可以拒絕一個公理或者接受一個公理，可以討論一個公理的引入是否合理。但只要我們引入了它，就默認它是真的。

我將其放在crazy_axioms命名空間下。如果不想使用這個公理，你需要避免在代碼中使用crazy_axioms這個命名空間。

2.2 類型即命題

接下來說明如何在Lean中證明一個命題為真。

在Lean中，命題也是一種類型。對於任意命題，如果你能構造類型為該命題的實例，就相當於證明這個命題為真。

下面將展示一些具體的例子。我們要證明：

section
  variable (p : Prop)
  example : ¬p ∨ ¬¬p := sorry
end

在Lean中，作為練習，我們經常會證明一些不重要的定理，我們懶得給它們取名字，這時我們使用example.

我們暫時沒有給出¬p ∨ ¬¬p的證明，因此我們將證明設為sorry，表示我們暫時給不了證明，但是請Lean不要報錯。

上面的寫法也等價於：

example (p : Prop) : ¬p ∨ ¬¬p := sorry

即可以將變量p的聲明與定理合併在一行。

加下來我們給出如何證明。p是一個命題，因此p的否定¬p也是一個命題。假如我們將其應用於em公理，將會得到什麼呢？

section
  variable (p : Prop)
  #check crazy_axioms.em ¬p -- crazy_axioms.em ¬p : ¬p ∨ ¬¬p
end

我們得到了一個類型為¬p ∨ ¬¬p的實例。因此，它可以作為¬p ∨ ¬¬p的證明。

example {p : Prop} : ¬p ∨ ¬¬p := crazy_axioms.em ¬p

在Lean中，我們使用theorem來定義定理。theorem就是有名字的example。

theorem np_or_nnp {p : Prop} : ¬p ∨ ¬¬p := crazy_axioms.em ¬p
#check np_or_nnp -- 類型為 ¬p ∨ ¬¬p

我們將得到的新命題命名為np_or_nnp，這實際上是一個返回類型為¬p ∨ ¬¬p的函數，我們用crazy_axioms.em ¬p作為它的返回值。

綜上所述，我們這麼理解Lean中的證明過程：一條定理實際上是一個函數。這個函數的輸入是定理使用的變量或者前提，輸出類型是定理所對應的命題，我們需要構造一個滿足類型要求的返回值作為其證明。

類型的證明也並不總是需要引用公理或先前的命題。下面是一個例子。

example {p q: Prop} : p → q → p := fun hp : p => fun hq : q => hp

在這個例子中，我們需要構造一個類型為p → q → p的值。

注意Lean中，→符號是右結合的，所以p → q → p表示的是p → (q → p). 函數fun hp : p => fun hq : q => hp的類型恰為p → q → p，這就完成了證明。

注意如果函數的輸入類型為a，輸出類型為b，那麼函數的類型為a → b，恰好對應著“a蘊含b”這一命題。

接下來，讓我們正式著手證明一些命題。

2.3 編寫證明

2.3.1 與運算

p ∧ q表示命題p和命題q同時成立，其定義為：

#print And
-- 輸出：
-- structure And (a b : Prop) : Prop
-- number of parameters: 2
-- fields:
--   And.left : a
--   And.right : b
-- constructor:
--   And.intro {a b : Prop} (left : a) (right : b) : a ∧ b

可見And是一個結構體，包含left和right兩個字段，並且有一個構造函數And.intro.

And.left的用法如下：

例 1 And.left

example {p q : Prop} : p ∧ q → p := fun h : p ∧ q => h.left

這個例子中，h的類型為And p q，因此h.left的類型為p.

上面的證明也可以寫成：

example {p q : Prop} : p ∧ q → p := fun h : p ∧ q => And.left h

接下來，請仿照And.left的用法，使用And.right完成練習。

习题 1

證明p ∧ q → q

參考答案

example {p q : Prop} : p ∧ q → q := fun h => h.right

例 2 And.intro

And.intro是And的構造函數，其用法如下：

example  {p q : Prop} : p → q → p ∧ q :=
  fun hp : p =>
    fun hq : q =>
      And.intro hp hq

該例子表明給定條件p和q成立，就有p ∧ q成立。

习题 2 And的交換律

證明：p ∧ q → q ∧ p

參考答案

example  {p q : Prop} : p ∧ q → q ∧ p :=
  fun h : p ∧ q =>
    And.intro h.right h.left

习题 3 And的冪等律

證明：p ∧ p → p

參考答案

example  {p : Prop} : p ∧ p → p :=
  fun h : p ∧ p =>
    h.left

2.3.2 或運算

p ∨ q表示命題p或命題q其中之一成立，或運算的定義為：

#print Or
-- inductive Or : Prop → Prop → Prop
-- number of parameters: 2
-- constructors:
-- Or.inl : ∀ {a b : Prop}, a → a ∨ b
-- Or.inr : ∀ {a b : Prop}, b → a ∨ b

可以看到Or有兩種構造函數，inl和inr。以inl為例，其含義為：若命題a成立，則命題a ∨ b成立。同理可知inr的用法。

例 3 Or.inl

example {p q : Prop} : p → p ∨ q :=
  fun hp : p => Or.inl hp

仿照這些例子，你可以完成下面的這些練習。

习题 4

證明：q → p ∨ q

參考答案

example {p q : Prop} : q → p ∨ q :=
  fun hq : q => Or.inr hq

p ∨ q表明p和q中至少有一個為真，因此在證明過程中我們常常需要分情況討論。對應的定理在Lean中為Or.elim. Or.elim的定義為：

#check Or.elim
-- Or.elim {a b c : Prop} (h : a ∨ b) (left : a → c) (right : b → c) : c

即已知a和b中至少有一個為真，且分兩種情況討論都能推出c為真，那麼c是真命題。

Or.elim的用法舉例如下：

习题 5

或運算的交換律：證明: p ∨ q → q ∨ p

參考答案

example {p q : Prop} : p ∨ q → q ∨ p :=
  fun hpq : p ∨ q =>
    Or.elim hpq
      ( -- 假如p為真
        fun hp : p =>
          Or.inr hp
      )
      ( -- 假如q為真
        fun hq : q =>
          Or.inl hq
      )

2.3.3 非運算

Lean定義了兩個特殊的命題，True和False. 它們分別代表真命題和假命題。

#check True  -- Prop
#check False -- Prop

在Lean中，非運算的定義比較特別——它被定義為一個函數：

#print Not
-- def Not : Prop → Prop :=
-- fun a => a → False

由Not的定義可見，非運算被定義為一個返回False命題的函數。即，如果Not p（或¬p）為真，那麼我們以p為前提應該能得到一個假命題。

example {p q : Prop} : ¬p → ¬(p ∧ q) :=
  -- 當前目標為證明 ¬p → ¬(p ∧ q)
  fun hnp : ¬p =>
    -- 此時目標為證明¬(p ∧ q)，等同於(p ∧ q) → False
    fun hpq : p ∧ q =>
      -- 目標為`False`
      hnp hpq.left
      -- 👆hnp輸入為`p`類型時，能返回False。我們利用這一點完成證明

注意在這個例子中，hnp被當做一個函數使用，用於返回False類型。

2.3.4 等價關係

當p ↔︎ q是，我們說p與q等價，或者p成立當且僅當q成立。等價關係被定義為：

#print Iff
-- structure Iff (a b : Prop) : Prop
-- number of parameters: 2
-- fields:
--   Iff.mp : a → b
--   Iff.mpr : b → a
-- constructor:
--   Iff.intro {a b : Prop} (mp : a → b) (mpr : b → a) : a ↔ b

可以看到Iff是一個結構體，包含mp和mpr兩個字段，並且有一個構造函數Iff.intro.

Iff.mp (p ↔︎ q)，也可以寫成(p ↔︎ q).mp，表示有p → q成立，即p為真時，q為真。反之Iff.mpr (p ↔︎ q)的箭頭方向相反，表示q → p成立。

Iff.intro的用法如下：

example {p q : Prop} : (p → q) → (q → p) → (p ↔ q) :=
  fun hpq : (p → q) =>
    fun hqp : (q → p) =>
      Iff.intro hpq hqp

2.4 一些有用的工具

2.4.1 `show`關鍵詞

在Lean中，我們可以使用show關鍵詞來指定我們要證明的類型。例如，

example {p q : Prop} : ¬p → ¬(p ∧ q) :=
  fun hnp : ¬p =>
    show p ∧ q → False from
    fun hpq : p ∧ q =>
      show False from hnp hpq.left

show的用處是增加我們代碼的可讀性。將當前證明目標顯式展現出來。

2.4.2 `let`關鍵詞

let關鍵詞用於局部變量的聲明。例如，

example {p q : Prop} (h : p ∧ q) : q ∧ p :=
  let hp : p := h.left
  let hq : q := h.right
  show q ∧ p from And.intro hq hp

在這個函數中，我們定義了hp和hq這兩個局部變量。

2.4.3 `have`關鍵詞

在Lean中，我們可以使用have關鍵詞聲明和完成一些中間步驟的證明。例如，

example {p q : Prop} (h : p ∧ q) : q ∧ p :=
  have hp : p := h.left
  have hq : q := h.right
  show q ∧ p from And.intro hq hp

在這個例子中，hp和hq是完成最終證明所需的中間步驟。

實際上have關鍵詞是一種語法糖。have h : p := s; t等價於(fun (h : p) => t) s. 因此，上面的代碼等價於：

example {p q : Prop} (h : p ∧ q) : q ∧ p :=
    (fun (hp : p) =>
      (
        fun (hq : q) =>
          show q ∧ p from And.intro hq hp
      ) h.right
    ) h.left

注记

請注意聲明中間步驟的have和聲明局部變量的let之間的差異，思考它們有什麼區別。

2.5 練習一

在證明下列命題時，請不要使用排中律，即（p ∨ ¬p）。

儘管在經典邏輯中，我們認為一個命題要麼為真要麼為假（排中律）；但也有一些人並不認可排中律，認為也應允許非真非假的命題存在。實際上，不依賴排中律我們也能完成許多定理的證明，包括下面這些定理。

习题 6

∧和∨的交換律： 證明p ∧ q ↔︎ q ∧ p和證明p ∨ q ↔︎ q ∨ p

參考答案

example {p q : Prop} : p ∧ q ↔ q ∧ p :=
  Iff.intro
    (
      fun h : p ∧ q =>
        have hp : p := h.left
        have hq : q := h.right
        And.intro hq hp
    )
    (
      fun h : q ∧ p =>
        have hq : q := h.left
        have hp : p := h.right
        And.intro hp hq
    )

example {p q : Prop} : p ∨ q ↔ q ∨ p :=
  Iff.intro
    (
      fun h : p ∨ q =>
        Or.elim h
          (fun hp : p => Or.intro_right q hp)
          (fun hq : q => Or.intro_left p hq)
    )
    (
      fun h : q ∨ p =>
        Or.elim h
          (fun hq : q => Or.intro_right p hq)
          (fun hp : p => Or.intro_left q hp)
    )

习题 7

∧和∨的結合律： 證明：example : (p ∧ q) ∧ r ↔︎ p ∧ (q ∧ r)和 example : (p ∨ q) ∨ r ↔︎ p ∨ (q ∨ r)

參考答案

example {p q r : Prop} : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (
      fun h : (p ∧ q) ∧ r =>
        let hpq : p ∧ q := h.left
        let hr : r := h.right
        let hp : p := hpq.left
        let hq : q := hpq.right
        And.intro hp (And.intro hq hr)
    )
    (
      fun h : p ∧ (q ∧ r) =>
        let hp : p := h.left
        let hqr : q ∧ r := h.right
        let hq : q := hqr.left
        let hr : r := hqr.right
        And.intro (And.intro hp hq) hr
    )

example {p q r: Prop} : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  Iff.intro
    (
      fun h : (p ∨ q) ∨ r =>
        Or.elim h
          (fun hpq : p ∨ q =>
            Or.elim hpq
              (fun hp : p => Or.intro_left (q ∨ r) hp)
              (fun hq : q => Or.intro_right p (Or.intro_left r hq))
          )
          (fun hr : r => Or.intro_right p (Or.intro_right q hr))

    )
    (
      fun h : p ∨ (q ∨ r) =>
        Or.elim h
          (fun hp: p => Or.intro_left r (Or.intro_left q hp))
          (fun hqr: q ∨ r =>
            Or.elim hqr
              (fun hq : q => Or.intro_left r (Or.intro_right p hq))
              (fun hr : r => Or.intro_right (p ∨ q) hr)
          )
    )

习题 8

∧和∨的分配律：證明p ∧ (q ∨ r) ↔︎ (p ∧ q) ∨ (p ∧ r) 和p ∨ (q ∧ r) ↔︎ (p ∨ q) ∧ (p ∨ r)

參考答案

example {p q r: Prop} : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
  Iff.intro
    (
      fun h : p ∧ (q ∨ r) =>
        let hp: p := h.left
        let hqr: q ∨ r := h.right
        Or.elim hqr
          (fun hq : q => Or.intro_left (p ∧ r) (And.intro hp hq))
          (fun hr : r => Or.intro_right (p ∧ q) (And.intro hp hr))
    )
    (
      fun h : (p ∧ q) ∨ (p ∧ r) =>
        Or.elim h
          (fun hpq : p ∧ q =>
            let hp : p := hpq.left
            let hq : q := hpq.right
            And.intro hp (Or.intro_left r hq)
          )
          (fun hpr : p ∧ r =>
            let hp := hpr.left
            let hr := hpr.right
            And.intro hp (Or.intro_right q hr)
          )
    )
example {p q r : Prop} : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
  Iff.intro
    (
      fun h : p ∨ (q ∧ r) =>
        Or.elim h
          (fun hp : p => And.intro (Or.intro_left q hp) (Or.intro_left r hp))
          (fun hqr : q ∧ r =>
            have hq :q := hqr.left
            have hr :r := hqr.right
            And.intro (Or.intro_right p hq) (Or.intro_right p hr)
          )
    )
    (
      fun h : (p ∨ q) ∧ (p ∨ r) =>
        have hpq : p ∨ q := h.left
        have hpr : p ∨ r := h.right
        Or.elim hpq
          (fun hp: p => Or.intro_left (q ∧ r) hp)
          (fun hq: q => Or.elim hpr
            (fun hp: p => Or.intro_left (q ∧ r) hp)
            (fun hr: r =>
              have hqr : q ∧ r := And.intro hq hr
              Or.intro_right p hqr
            )
          )
    )

习题 9 證明：(p → (q → r)) ↔︎ (p ∧ q → r)

參考答案

example {p q r : Prop} : (p → (q → r)) ↔ (p ∧ q → r) :=
  Iff.intro
    (
      fun hpqr : p → (q → r) =>
        fun hpq : p ∧ q =>
          have hp := hpq.left
          have hq := hpq.right
          hpqr hp hq
    )
    (
      fun hpqr : p ∧ q → r =>
        fun hp : p =>
          fun hq : q =>
            have hpq := And.intro hp hq
            hpqr hpq
    )

习题 10

證明：((p ∨ q) → r) ↔︎ (p → r) ∧ (q → r)

參考答案

example {p q r : Prop} : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
  Iff.intro
    (
      fun hpqr : p ∨ q → r =>
        And.intro
          (fun hp : p => hpqr (Or.intro_left q hp))
          (fun hq : q => hpqr (Or.intro_right p hq))
    )
    (
      fun hprqr : (p → r) ∧ (q → r) =>
        have hpr : p → r := hprqr.left
        have hqr : q → r := hprqr.right
        fun hpq : p ∨ q =>
          Or.elim hpq
            (fun hp : p => hpr hp)
            (fun hq : q => hqr hq)
    )

习题 11

證明：¬(p ∨ q) ↔︎ ¬p ∧ ¬q

參考答案

example {p q : Prop} : ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
  Iff.intro
    (
      fun hnpq : ¬(p ∨ q) =>
        And.intro
          (fun hp : p => hnpq (Or.intro_left q hp))
          (fun hq : q => hnpq (Or.intro_right p hq))
    )
    (
      fun hnpnq : ¬p ∧ ¬q =>
        have hnp : ¬p := hnpnq.left
        have hnq : ¬q := hnpnq.right
        (
          fun hpq : p ∨ q => Or.elim hpq
            (fun hp : p => hnp hp)
            (fun hq : q => hnq hq)
        )
    )

习题 12

證明：¬p ∨ ¬q → ¬(p ∧ q)

參考答案

example {p q : Prop} : ¬p ∨ ¬q → ¬(p ∧ q) :=
  fun hnpnq : ¬p ∨ ¬q =>
    Or.elim hnpnq
      (fun hnp : ¬p => fun hpq : p ∧ q => hnp hpq.left)
      (fun hnq : ¬q => fun hpq : p ∧ q => hnq hpq.right)

习题 13

證明：¬(p ∧ ¬p)

參考答案

example {p : Prop} : ¬(p ∧ ¬p) :=
  fun hpnp : p ∧ ¬p =>
    have hp : p := hpnp.left
    have hnp: ¬p := hpnp.right
    hnp hp

习题 14

證明：p ∧ ¬q → ¬(p → q)

參考答案

example {p q : Prop} : p ∧ ¬q → ¬(p → q) :=
  fun hpnq : p ∧ ¬q =>
    have hp : p := hpnq.left
    have hnq : ¬q := hpnq.right
    fun hpq : p → q =>
      have hq : q := hpq hp
      hnq hq

习题 15

證明：¬p → (p → q)

參考答案

example {p q : Prop} : ¬p → (p → q) :=
  fun hnp : ¬p =>
    fun hp : p =>
      False.elim (hnp hp)

习题 16

證明：(¬p ∨ q) → (p → q)

參考答案

example {p q : Prop} : (¬p ∨ q) → (p → q) :=
  fun hnpq : ¬p ∨ q =>
    fun hp : p =>
      Or.elim hnpq
        (fun hnp : ¬p => False.elim (hnp hp))
        (fun hq : q => hq)

习题 17

同一律

參考答案

example {p : Prop} : p ∨ False ↔ p :=
  Iff.intro
    (
      fun hpf : p ∨ False =>
      Or.elim hpf
        (fun hp : p => hp)
        (fun hf : False => False.elim hf)
    )
    (fun hp : p => Or.intro_left False hp)

习题 18

零律證明：p ∧ False ↔︎ False

參考答案

example {p : Prop} : p ∧ False ↔ False :=
  Iff.intro
    (
      fun hpf : p ∧ False =>
        have hf : False := hpf.right
        hf
    )
    fun hf : False =>
      False.elim hf

习题 19

假言易位 證明：(p → q) → (¬q → ¬p)

參考答案

example {p q : Prop} : (p → q) → (¬q → ¬p) :=
  fun (hpq : p → q) (hnq : ¬q) =>
    fun hp : p =>
      hnq (hpq hp)

2.6 練習二-經典邏輯

下面的練習中，你可以使用排中律。

Lean中，排中律位於Classical命名空間下。

#check Classical.em

我們可以臨時地使用Classical命名空間，而不幹擾其它代碼。方法為open Classical in ...，例如

open Classical in
example {p : Prop} : p ∨ ¬p := em p

允許使用排中律，使得你可以分正反兩種情形分析問題。這對應Classical命名空間下的byCases定理：

#check Classical.byCases
-- Classical.byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q

即如果分正反兩種情況討論，都有結論成立，說明結論成立。

习题 20

證明：(p → q ∨ r) → ((p → q) ∨ (p → r))

參考答案

open Classical in
example {p q r : Prop} : (p → q ∨ r) → ((p → q) ∨ (p → r)) :=
  fun pqr : p → q ∨ r =>
    Or.elim (em q)
    (
      fun hq : q =>
        Or.intro_left (p → r) (fun _ : p => hq)
    )
    (
      fun hnq : ¬q =>
        Or.intro_right (p → q)
        (
          fun hp : p =>
            have qr : q ∨ r := pqr hp
            Or.elim qr
              (fun hq : q => False.elim (hnq hq))
              (fun hr : r => hr

        )
    )
  )

习题 21

證明：¬(p ∧ q) → ¬p ∨ ¬q

參考答案

open Classical in
example {p q : Prop} : ¬(p ∧ q) → ¬p ∨ ¬q :=
  fun hnpq : ¬(p ∧ q) =>
    byCases
      (
        fun hp : p =>
          byCases
            (
              fun (hq : q) =>
                have hpq : p ∧ q := And.intro hp hq
                absurd hpq hnpq
            )
            (fun (hnq : ¬q) => Or.intro_right (¬p) hnq)
      )
      (fun hnp : ¬p => Or.intro_left (¬q) hnp)

习题 22

證明：(p → q) → (¬p ∨ q)

參考答案

open Classical in
example {p q : Prop} : (p → q) → (¬p ∨ q) :=
  fun hpq : (p → q) =>
    byCases
      (
        fun hp : p =>
          have hq : q := hpq hp
          Or.intro_right (¬p) hq
      )
      (
        fun hnp : ¬p => Or.intro_left q hnp
      )

习题 23

證明：(¬q → ¬p) → (p → q)

參考答案

open Classical in
example {p q : Prop} : (¬q → ¬p) → (p → q) :=
  fun hnqnp : ¬q → ¬p =>
    fun hp : p =>
      Or.elim (em q)
        (fun hq : q => hq)
        (
          fun hnq : ¬q =>
            have hnp : ¬p := hnqnp hnq
            False.elim (hnp hp)
        )

例 4

證明：(((p → q) → p) → p)

參考答案

open Classical in
example {p q : Prop} : (((p → q) → p) → p) :=
  fun hpqp : (p → q) → p =>
    byCases
      (fun hp : p => hp)
      (
        fun hnp : ¬p =>
          have hpq : p → q := (fun hp : p => False.elim (hnp hp))
          have hp : p := hpqp hpq
          False.elim (hnp hp)
      )

也許現在告訴你有點太遲，但其實一般的命題邏輯都可以由tauto策略自動證明。如下所示，

-- example {p q r: Prop} : (p → (q → r)) ↔ (p ∧ q → r) := by tauto
-- 注意：使用tauto的前提是import Mathlib

至此，本章介紹了Lean中命題邏輯的基礎知識，希望你已經理解在Lean中如何引用定理，顯式地構造一個命題的證明，或者使用tauto策略自動完成命題邏輯的證明。