name: loogle-search description: 通过类型签名模式在Mathlib中搜索引理
Loogle 搜索 - Mathlib 类型签名搜索
通过类型签名模式在Mathlib中搜索引理。
使用时机
- 当您知道类型形状但不知道名称时查找引理
- 发现某个类型可用的引理（例如，所有
Nontrivial ↔ _引理） - 类型导向的证明搜索
命令
# 通过模式搜索（如果服务器运行，则使用服务器，否则直接）
loogle-search "Nontrivial _ ↔ _"
loogle-search "(?a → ?b) → List ?a → List ?b"
loogle-search "IsCyclic, center"
# JSON输出
loogle-search "List.map" --json
# 启动服务器以快速查询（在内存中保持索引）
loogle-server &
查询语法
| 模式 | 含义 |
|---|---|
_ |
任何单个类型 |
?a, ?b |
类型变量（相同变量 = 相同类型） |
Foo, Bar |
必须同时提到 Foo 和 Bar |
Foo.bar |
精确名称匹配 |
示例
# 查找与Nontrivial和基数相关的引理
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"
# 查找类似map的函数
loogle-search "(?a → ?b) → List ?a → List ?b"
# → List.map, List.pmap, ...
# 查找关于循环群和中心的所有内容
loogle-search "IsCyclic, center"
# → commutative_of_cyclic_center_quotient, ...
# 查找Fintype.card引理
loogle-search "Fintype.card"
性能
- 服务器运行时: 每次查询约100-200毫秒
- 冷启动（无服务器）: 每次查询约10秒（加载343MB索引）
设置
Loogle必须先构建：
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache # 或使用 --write-index
与证明集成
在Lean证明中卡住时：
- 识别需要的类型形状
- 查询Loogle以找到引理名称
- 在证明中应用该引理
-- 目标：从1 < Fintype.card G得到Nontrivial G
-- 查询：loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"
-- 找到：Fintype.one_lt_card_iff_nontrivial
exact Fintype.one_lt_card_iff_nontrivial.mpr h