如何让Coq中CPDT的crush自动展开定义def？

问题背景 #

以下是简化后的示例代码，核心需求是让自定义的crush'策略自动展开def定义，同时不能将def设为Notation（否则它作为假设时会被crush自动拆分）：

(* 简化版crush，仅用于示例 *)
Ltac crush' := autorewrite with core; eauto.

Definition P := False.
Definition Q := (False /\ False).
Definition def := P /\ Q.

Axiom solve_P : P = True.
Axiom solve_Q : Q = True.
Hint Rewrite solve_P solve_Q.

(* 尝试过的无效提示 *)
Hint Unfold def.
Hint Transparent def.
Hint Extern 1 def => unfold def.

Axiom def_hint : P -> Q -> def.
Hint Resolve def_hint.

Lemma test : def.
Proof.
  crush'. (* 失败：无法自动展开def *)
  unfold def; crush'. (* 成功，但想避免显式unfold *)
  Undo.
  (* 手动断言更繁琐 *)
  assert P by crush'.
  assert Q by crush'.
  crush'. (* 成功 *)
Qed.

核心原因分析 #

你猜测的执行顺序问题完全正确：

1. 原crush'的执行流程是先autorewrite，再eauto
2. 当目标为def时，autorewrite无法处理该符号；eauto阶段触发展开def的提示后，目标变为P /\ Q，但此时crush'已经结束，不会再执行autorewrite将P/Q替换为True，导致eauto无法解决False /\ False（即使有solve_P/solve_Q的重写提示）
3. 另外，Hint Resolve def_hint需要先证明P和Q，但原流程中autorewrite没机会处理P/Q，所以这条提示也无法生效

解决方案 #

调整crush'的逻辑，让它能在展开def后重新触发重写和自动化策略，以下是两种可行方案：

方案1：循环执行策略直到目标解决 #

将crush'改为循环执行autorewrite、eauto和展开操作，确保展开后的目标能被重写处理：

Ltac crush' := repeat (autorewrite with core; eauto; try unfold def).

• repeat会重复执行括号内的策略，直到无法再修改目标或目标被解决
• try unfold def确保只有当def存在时才尝试展开，避免无意义操作

方案2：精准匹配目标触发展开 #

针对目标为def的情况优先展开，再执行重写和自动化：

Ltac crush' :=
  repeat match goal with
         | [ |- def ] => unfold def
         | _ => autorewrite with core; eauto
         end.

• 用match goal精准捕获目标为def的场景，展开后进入下一轮循环
• 循环中autorewrite会处理P/Q，eauto解决最终的True /\ True

验证 #

替换原crush'后，直接执行即可通过证明：

Lemma test : def.
Proof. crush'. Qed.

补充说明 #

• 保留def为Definition而非Notation，确保它作为假设时不会被crush自动拆分
• 两种方案都不需要修改原有提示，只需调整crush'的执行逻辑

内容的提问来源于stack exchange，提问作者R. Bosman