如何设计Coq战术：调用无证明项决策过程时判定目标得证？

Ltac 实现 #

直接用 change 修改目标结论为 True，再用 exact I 完成证明即可，这和你提到的 change_concl 效果一致（change True 默认修改结论）：

Ltac decide_and_prove :=
  (* 这里插入调用你的决策过程的逻辑，假设返回"是"时执行后续步骤 *)
  change True;
  exact I.

Ltac2 实现 #

Ltac2 没有直接对应 change_concl 的顶层命令，但可以通过 Tactic.change 或 Goal.modify 来修改目标结论，再完成证明：

Ltac2 decide_and_prove () :=
  (* 插入你的决策过程调用逻辑，确认返回"是"后执行 *)
  Tactic.change (Constr.of_constr True);
  Tactic.exact (Constr.of_constr I).

或者用更底层的目标修改方式：

Ltac2 decide_and_prove () :=
  let true_constr := Constr.of_constr True in
  Goal.modify (fun g => Goal.set_concl g true_constr);
  Tactic.exact (Constr.of_constr I).

注意事项 #

这种方法的核心前提是你的决策过程绝对可靠——它必须准确判定原目标在逻辑上成立。如果决策过程出错，这种方式会构造出无效的证明（相当于跳过了原目标的实际推导）。只要决策过程可信，这个方案完全可行。

内容的提问来源于stack exchange，提问作者Henrique Guerra