如何指导auto在证明搜索过程中简化目标？解决let表达式阻碍问题

安全阿岳

2026-6-25

Coq中let表达式阻碍证明搜索的解决方法

问题背景

最小复现示例：

Goal let x := True in x.

该目标可通过simpl. auto.解决，但单独调用auto.无效。实际复杂场景中，可zeta约简的let表达式会卡住auto本可推进的中间步骤，且auto无法中途暂停插入化简操作。需要非冗余的处理方式，避免全局粗暴应用simpl。

用intuition替代auto：intuition会自动处理简单化简（包括这类let的zeta约简），直接调用intuition.即可解决示例目标，复杂场景中也能自动处理此类阻碍并完成后续证明搜索。
自定义轻量化简+证明搜索的组合tactic：创建仅做必要化简的组合策略，避免过度化简：
```
Ltac auto_simpl := simpl only []. auto.
```
simpl only []仅执行zeta约简（移除冗余let绑定），不会改动其他表达式，之后调用auto即可正常推进证明。
精准的局部hint策略：若需在证明搜索中自动处理特定let结构，可添加针对性extern hint，而非全局策略：
```
Hint Extern 0 (let _ := _ in _) => simpl : my_hints.
```
后续调用auto with my_hints.时，仅会处理匹配到的顶层let表达式，不会全局触发simpl。
手动局部展开（适用于明确结构的场景）：如果清楚let绑定的具体内容，可直接用destruct或unfold展开：
```
destruct (let x := True in x). auto.
```
这种方式更适合对目标结构完全明确的场景。