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策略自动完成命题逻辑的证明。