无法自动化在Coq中手动工作的引理

Question

（似乎my previous question有太多不相关的信息，所以我试图抽象出细节。我不确定它仍然是同一个问题，但如果相同的解决方案适用于两者，我会删除另一个问题。）

我试图推断一些自定义列表和谓词：

Inductive alphabet := A.

Definition sentence : Type := list alphabet.

Variable pred1 : sentence -> Prop.

Variable pred2 : sentence -> Prop.

Variable conclusion : Prop.

现在，有以下假设，

Hypothesis H1 : forall (X : sentence),
pred1 X -> pred2 (X ++ X).

Hypothesis H2 : forall X,
pred2 X -> conclusion.

我想证明

Example manual : pred1 [A] -> conclusion.

这显然是正确的，因为conclusion跟随每当一些sentence有pred2，并且任何pred1的sentence意味着sentence的重复有pred2。手写的证明就是

intro. eapply H2. apply H1. exact H. Qed. 

请注意，证明只使用intro，apply，eapply和exact。这意味着证明应该允许直接自动化，只要H1和H2在上下文中可用。例如，半自动版本

Example semiauto : pred1 [A] -> conclusion.
pose proof H1. pose proof H2. eauto. Qed.

完全按照您的预期工作。现在，让我们尝试一个带有提示的全自动版本：

Hint Resolve H1 H2. 

Example auto : pred1 [A] -> conclusion.
eauto.
intro. 
eauto. 
eapply H2. 
eauto. 
apply H1. 
eauto. Qed.

这很奇怪。 eauto不仅在开始时失败，而且在除了最后一步之外的每一步都失败了。为什么会这样？

一些猜测：H1的结果包括形式X ++ X，这可能导致统一问题。也许Coq在明确引入上下文时会使用H1执行一些隐式清理，但是当它只是在提示DB中时。

有任何想法吗？

Answer 1

问题是sentence的透明度。

以安东·特鲁诺夫的答案为基础，如果你仔细观察，你会发现Print HintDb core和Create HintDb foo. Print HintDb foo.之间的区别在于Print HintDb core说

Unfoldable variable definitions: none
Unfoldable constant definitions: none

而Create HintDb foo. Print HintDb foo.说

Unfoldable variable definitions: all
Unfoldable constant definitions: all

我构建了以下简化版本的示例：

Require Import Coq.Lists.List.
Import ListNotations.
Definition sentence := list nat.
Variable pred1 : sentence -> Prop.
Variable pred2 : sentence -> Prop.
Hypothesis H1 : forall (X : sentence),
    pred1 X -> pred2 (X ++ X).
Create HintDb foo.
Hint Resolve H1 : foo.
Hint Resolve H1 : bar.
Hint Resolve H1.
Example ex1 : pred1 [0] -> exists X, pred2 X.
  eexists.
  debug eauto.

在这里，我们有eauto和eauto with bar（和eauto with bar nocore，从eauto的考虑中移除核心数据库）都失败了，但eauto with foo（和eauto with foo nocore）成功。这表明问题是透明度。有点玩耍导致我发现如果我们写的话，eauto会起作用

Hint Transparent sentence.

另外，即使没有这个，如果我们明确地给eauto变量展开类型，X工作正常：

Example ex2 : pred1 [0] -> exists X : list nat, pred2 X.

我不完全确定为什么Coq表现得这样......也许它拒绝用不同类型的术语统一evars（如果?X在sentence有类型X ++ X时有list类型），或者它可能是基于meta的延迟统一......我打开了一个issue on the bugtracker about this lack of documentation / bad behavior。

Answer 2

这里可能的解决方法是将提示添加到新的用户定义数据库：

Create HintDb my_hints.
Hint Resolve H1 H2 : my_hints.

现在我们可以完成证明：

Example auto : pred1 [A] -> conclusion.
  eauto with my_hints. Qed.

还有一件事：Coq的参考手册告诉我们（§8.9.1）我们

可以选择使用命令Create HintDb声明提示数据库。如果将提示添加到未知数据库，则会自动创建该提示。

但是，如果我们省略Create HintDb my_hints.部分，eauto战术将不起作用。当提示被添加到默认的core提示数据库时，看起来一样。