Lean3命题逻辑证明移植至Lean4的方法及相关文档查询

一、目标代码的Lean4移植版本 #

你的Lean3定理可以直接修改为以下Lean4代码：

theorem my_theorem : P ∧ Q → Q ∧ P :=
fun h : P ∧ Q =>
  have hP : P := And.left h
  have hQ : Q := And.right h
  show Q ∧ P from And.intro hQ hP

关键变化点：

• 逻辑连接词从小写and改为大写And（遵循Lean4类型构造器的命名规范）
• assume替换为fun（Lean4统一用fun定义匿名函数，也可使用λ）
• 你也可以进一步简化成更紧凑的版本：

theorem my_theorem : P ∧ Q → Q ∧ P :=
fun h => And.intro h.right h.left

二、Lean3到Lean4移植的相关文档 #

• Lean官方迁移指南：Lean4仓库内置的doc/migration.md文档，详细覆盖了语法、tactic、标准库API的核心差异与替换规则
• Lean4官方手册的「Lean 3 Compatibility」章节：讲解了Lean4提供的Lean3兼容层用法，以及常见的代码适配技巧
• 社区迁移笔记：Lean Zulip社区和GitHub上有用户整理的实战迁移清单，包含常见的语法替换（如from关键字使用微调、tactic名称变更等）

内容的提问来源于stack exchange，提问作者Henry H.