coq - 无法自动化在 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.

这显然是正确的，因为只要某些句子有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

问题是句子的透明度。

根据 Anton Trunov 的回答，如果仔细观察，您会注意到 Print HintDb core 和 Create HintDb foo 之间的区别。 Print HintDb foo. 就是Print HintDb core 说的

Unfoldable variable definitions: none
Unfoldable constant definitions: none

同时 创建 HintDb foo。打印 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.

此外，即使没有这个，如果我们明确地为 X 变量指定展开类型，eauto 也能正常工作:

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

我不完全确定为什么 Coq 会这样......也许它拒绝将 evar 与不同类型的术语统一(如果 ?X 的类型为 sentence 当 X++ X 的类型为 list 时)，或者它可能是基于元的统一的保留...我打开了一个 issue on the bugtracker about this lack of documentation / bad behavior .