Precise search
Lean 定理精确搜索
Mathlib 数学库中包含了成千上万条引理，如何才能高效地找到需要的那一条？
仅仅通过记忆引理的名称或模糊的关键词进行搜索，往往如同大海捞针。更有效的方法是通过表达式结构进行精确的定位。这篇笔记介绍 Loogle 的使用方法。
官网介绍的翻译
关于
Loogle 搜索 Lean 和 Mathlib 中的定义与定理。
你可以在 Lean4 的 VSCode 语言扩展中通过（默认为）Ctrl-K Ctrl-S 来使用 Loogle。你也可以尝试来自 LeanSearchClient 的 #loogle 命令、CLI 版本、Loogle VS Code 扩展、lean.nvim 集成或 Zulip 机器人。
用法
Loogle 通过多种方式寻找定义和引理：
通过常量：
🔍 Real.sin
查找所有命题中以任何方式提及正弦函数的引理。
通过引理名称的子字符串：
🔍 "differ"
查找所有在其引理名称中某处包含 "differ" 的引理。
通过子表达式：
🔍 _ * ( ^ )
查找所有命题中某处包含一个乘积，且其第二个参数被提升到某个次方的引理。
模式也可以是非线性的，如：
🔍 Real.sqrt ?a * Real.sqrt ?a
如果模式有参数，它们会以任意顺序进行匹配。下面两者都会找到 List.map：
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
通过主结论：
🔍 |- tsum _ = _ * tsum _
查找所有结论（即位于所有 → 和 ∀ 右侧的子表达式）具有给定形状的引理。
和之前一样，如果模式有参数，它们会以任意顺序与引理的前提进行匹配；例如，
🔍 |- _ < _ → tsum _ < tsum _
将会找到 tsum_lt_tsum，即使前提 f i < g i 并不是最后一个。
如果你传递多个用逗号分隔的搜索过滤器，Loogle 将返回匹配所有这些过滤器的引理。搜索
🔍 Real.sin, "two", tsum, _ * , _ ^ , |- _ < _ → _
将会找到所有提及常量 Real.sin 和 tsum，引理名称中包含子字符串 "two"，类型中某处包含乘积和幂，并且有一个形如 _ < _ 的前提的引理（如果存在这样的引理的话）。元变量 (?a) 在每个过滤器中是独立分配的。
个人理解总结
Loogle 是一款专为 Lean 与 Mathlib 设计的搜索工具，可在以下环境调用：
- VS Code 官方Lean扩展：可以设置快捷键以在侧边栏中快速打开 Loogle 界面使用，使用组合键 Ctrl-K Ctrl-S打开设置界面，搜索 Loogle 为其设置快捷键。
- #loogle 命令（由 LeanSearchClient 提供）
- CLI、VS Code 扩展、lean.nvim、Zulip 机器人
用法速览
| 搜索方式 | 示例 | 说明 |
|---|---|---|
| 常量 | Real.sin |
返回所有用到 Real.sin 的定理 |
| 名称片段 | "differ" |
返回名称字符串中包含子串 differ 的定理 |
| 子表达式 | _ * (_ ^ _) |
返回类型中存在“乘方后再相乘”模式的定理 |
| 非线性模式 | Real.sqrt ?a * Real.sqrt ?a |
?a 在同一位置重复出现，可匹配平方根相乘的定理（我理解为原变量，类似与正则表达式使用的$1） |
| 主结论 | |- tsum _ = _ * tsum _ |
仅匹配结论（最右侧表达式）符合模式的定理 |
| 前提模式 | |- _ < _ → tsum _ < tsum _ |
即使前提顺序不同，也能匹配 tsum_lt_tsum |
组合过滤
, 半角逗号连接多个条件，结果为交集。示例：