编辑“︁Lean命题基础”︁

= Lean命题基础 =

'''Lean命题基础'''是学习Lean定理证明器的核心起点，它涵盖了命题逻辑的基本构造、语法规则和证明方法。本节将系统介绍如何在Lean中表示和操作命题，包括逻辑联结词、真值、以及简单证明的构建方式。

== 命题逻辑简介 ==

命题逻辑（Propositional Logic）是数学逻辑的基础分支，研究由原子命题（不可再分的陈述句）通过逻辑联结词（如∧、∨、→、¬）组合而成的复合命题。在Lean中，命题被表示为类型，其证明则是该类型的项。

=== 核心概念 ===
* '''命题'''：可判断真假的陈述（如"2是偶数"）。
* '''真值'''：命题的取值（True/False）。
* '''逻辑联结词'''：
  * 合取（<math>\land</math>）：`P ∧ Q`
  * 析取（<math>\lor</math>）：`P ∨ Q`
  * 蕴含（<math>\to</math>）：`P → Q`
  * 否定（<math>\neg</math>）：`¬P`

== Lean中的命题表示 ==

在Lean中，命题是`Prop`类型的对象。以下示例展示如何声明命题并使用联结词：

<syntaxhighlight lang="lean">
-- 声明两个命题变量
variables (P Q : Prop)

-- 复合命题示例
#check P ∧ Q      -- 合取
#check P ∨ Q      -- 析取
#check P → Q      -- 蕴含
#check ¬P         -- 否定
</syntaxhighlight>

输出：
```
P ∧ Q : Prop
P ∨ Q : Prop
P → Q : Prop
¬P : Prop
</syntaxhighlight>

== 基本证明方法 ==

Lean使用'''构造性逻辑'''，证明即给出对应命题的具体构造。以下是常见命题的证明示例：

=== 合取证明 ===
<syntaxhighlight lang="lean">
example (hP : P) (hQ : Q) : P ∧ Q :=
⟨hP, hQ⟩  -- 使用尖括号构造合取证明
</syntaxhighlight>

=== 析取证明 ===
<syntaxhighlight lang="lean">
example (hP : P) : P ∨ Q :=
or.inl hP  -- 选择左分支证明
</syntaxhighlight>

=== 蕴含证明 ===
<syntaxhighlight lang="lean">
example : P → P :=
λ hP => hP  -- 使用lambda表达式处理假设
</syntaxhighlight>

== 真值表与逻辑等价 ==

通过真值表可验证命题的等价性。例如<math>P → Q</math>等价于<math>\neg P \lor Q</math>：

<mermaid>
flowchart LR
    A[P] -->|true| B[Q]
    A -->|false| C[¬P ∨ Q = true]
</mermaid>

数学表示：
<math>
P \to Q \equiv \neg P \lor Q
</math>

== 实际案例：登录系统验证 ==

假设需要验证一个登录系统的逻辑规则："如果用户已认证''且''令牌有效，则允许访问"。用Lean表示为：

<syntaxhighlight lang="lean">
variables (authenticated valid_token : Prop)
theorem access_rule (h1 : authenticated) (h2 : valid_token) : access_granted :=
⟨h1, h2⟩  -- 构造合取证明
</syntaxhighlight>

== 常见错误与调试 ==

1. '''类型不匹配'''：确保所有子命题类型为`Prop`
   <syntaxhighlight lang="lean">
   -- 错误示例
   example (n : Nat) : n → n := λ x => x  -- Nat不是命题！
   </syntaxhighlight>

2. '''未消解假设'''：所有假设必须被使用
   <syntaxhighlight lang="lean">
   -- 错误示例
   example (hP : P) : Q := sorry  -- 未使用hP
   </syntaxhighlight>

== 进阶概念 ==

* '''经典逻辑'''：通过`open Classical`使用排中律
* '''命题等价性'''：用`↔`表示双向蕴含
  <syntaxhighlight lang="lean">
  example : P ∧ Q ↔ Q ∧ P :=
  ⟨λ h => ⟨h.right, h.left⟩, λ h => ⟨h.right, h.left⟩⟩
  </syntaxhighlight>

== 练习 ==

尝试证明以下命题：
<syntaxhighlight lang="lean">
example : P → ¬¬P :=
λ hP => λ hnP => hnP hP
</syntaxhighlight>

提示：否定¬P在Lean中定义为`P → False`。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean命题逻辑]]