Lean常用快捷键

Lean常用快捷键

介绍

Lean 是一款强大的交互式定理证明器，广泛用于形式化数学和编程验证。掌握其快捷键可以显著提升开发效率，特别是在频繁切换证明状态和浏览代码时。本页面将详细介绍 Lean 中常用的快捷键及其应用场景，适合初学者和进阶用户参考。

基础导航快捷键

以下快捷键适用于 Lean 的默认编辑器（如 VS Code 或 Emacs 插件）：

基础导航快捷键表

快捷键	功能	说明
Ctrl + Enter	执行当前行或选中代码	在 Lean 中触发类型检查或证明推进
Alt + ↑/↓	上下移动代码块	调整证明步骤的顺序
Ctrl + .	跳转到定义	查看函数或定理的定义
Ctrl + Shift + .	查找引用	定位符号的使用位置
F12	重命名符号	重构时修改变量或定理名称

证明交互快捷键

在编写证明时，以下快捷键尤为实用：

补全建议

• Ctrl + Space：触发自动补全（如输入 rw 后补全 rewrite）。
• Tab：在补全菜单中选择建议项。

证明辅助

• Ctrl + Alt + Enter：尝试自动填充证明（如使用 simp 或 auto）。
• Ctrl + /：注释/取消注释当前行。

  
-- 示例：使用快捷键快速补全  
example : 2 + 2 = 4 := by  
  simp -- 输入 `simp` 后按 Ctrl+Enter 执行

高级编辑技巧

多光标操作

• Alt + Click：添加多个光标。
• Ctrl + D：选中当前单词并查找下一个相同项。

代码折叠

• Ctrl + Shift + [：折叠当前代码块。
• Ctrl + Shift + ]：展开代码块。

实际案例

以下是一个使用快捷键优化证明流程的示例：

  
-- 初始证明（手动输入）  
theorem add_comm (a b : Nat) : a + b = b + a := by  
  induction a  
  · simp  
  · simp [Nat.succ_add, *]  

-- 使用快捷键优化后：  
-- 1. 输入 `induction a` 后按 Ctrl+Enter 执行  
-- 2. 按 Alt+↓ 移动第二个 `simp` 到正确位置  
-- 3. 使用 Ctrl+/ 注释掉未完成的步骤

快捷键图示

flowchart TD A[开始编写证明] --> B[输入策略如 simp] B --> C{Ctrl+Enter执行} C --> D[查看目标状态] D --> E[继续编辑或补全]

数学公式支持

快捷键效率提升的量化分析： $\text{节省时间}=\sum _{i=1}^n(t_{\text{手动}}-t_{\text{快捷键}})$

总结

熟练掌握 Lean 的快捷键可以大幅减少重复操作时间，尤其适合长证明或大型项目。建议从基础导航开始练习，逐步适应高级编辑功能。