让"自动"执行案例分析的惯用方法是什么?

Question

Inductive Foo : nat -> Type :=
| a : Foo 1.
(* ... *)
Goal forall m, Foo m -> m = 1.
Proof.
auto.
Fail Qed.

有没有一种简单的方法来做到这一点？

Answer 1

您可以将Hint Extern与执行案例分析的策略脚本一起使用。 例如，如果参数是变量，则此参数将使用destruct，否则将使用inversion_clear：

Inductive Foo : nat -> Type :=
| a : Foo 1.
Hint Extern 1 => match goal with
| [ H : Foo ?m |- _ ]
=> first [ is_var m; destruct H | inversion_clear H ]
end.
Goal forall m, Foo m -> m = 1.
Proof.
auto.
Qed.

Answer 2

通过编程语言基础，Coq 证明中的自动化理论与实践一章：

请注意，证明搜索策略从不执行任何重写步骤(策略rewrite，subst)，也不对任意数据结构或属性进行任何案例分析(策略destruct和inversion)，也不执行任何归纳证明(策略induction)。因此，证明搜索实际上是为了自动执行证明的各个分支的最后步骤。它无法发现证明的整体结构。

所以真的没有办法做到这一点;这个目标应该手动解决，然后添加到提示数据库(Hint blah.)。