Lean4项目中simp?!指令未启用自动展开功能的问题分析

在Lean4定理证明系统中，simp系列指令是自动化证明的重要工具。最近发现了一个关于simp?!指令行为异常的问题，值得深入探讨。

问题背景

Lean4的simp指令家族包含多个变体，其中：

• simp：基本的简化指令
• simp!：在简化时自动展开定义
• simp?!：与simp?类似，但会尝试自动展开定义

用户报告了一个行为不一致的情况：在相同的条件下，simp!能够成功完成证明，而simp?!却报告"simp made no progress"（简化未取得进展）。

技术细节分析

问题的核心在于simp?!指令的实现未能正确继承simp!的自动展开行为。从技术实现角度来看：

1. simp!通过设置特定的配置标志来启用定义展开
2. simp?!本应是simp?和simp!的结合体，但实际上只继承了simp?的查询功能，没有继承自动展开的特性

影响范围

这个问题影响了以下使用场景：

• 用户希望同时获得自动展开和简化建议查询的功能
• 在交互式开发中，当需要查看简化步骤同时又需要自动展开定义时

解决方案

该问题已在Lean4的夜间构建版本中得到修复。修复方案确保了：

1. simp?!现在正确地继承了simp!的自动展开行为
2. 同时保留了查询简化步骤的功能
3. 保持了与现有代码的兼容性

最佳实践建议

对于Lean4用户，在处理类似情况时：

1. 当需要自动展开定义时，优先使用simp!
2. 如果需要查看简化步骤，使用simp?!（确保使用修复后的版本）
3. 对于关键证明步骤，可以考虑显式使用unfold指令来明确展开定义

这个问题提醒我们，在定理证明系统中，即使是看似简单的指令变体，其行为一致性也需要特别注意。理解这些工具的内部工作机制有助于更有效地使用它们来完成证明任务。