代码之家 › 专栏 › 技术社区 › Carl Patenaude Poulin

让“auto”执行案例分析的惯用方法是什么?

coq-tactic coq

Carl Patenaude Poulin · 技术社区 · 7 年前

Inductive Foo : nat -> Type :=
  | a : Foo 1.

(* ... *)

Goal forall m, Foo m -> m = 1.
Proof.
  auto.
Fail Qed.

有没有一种简单的方法可以做到这一点?

2 回复 | 直到 7 年前

Jason Gross 7 年前

您可以使用 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.

Carl Patenaude Poulin 7 年前

通过 编程语言基础 章 Theory and Practice of Automation in Coq Proofs :

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

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

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

7 年前