無法自動執行在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明確引入上下文時，Coq可能會執行一些隱式清理，但不會在僅提示DB時執行。

任何想法？

Answer 1

這裏的一個可能的解決方法是將提示添加到新的用戶定義的數據庫：

Create HintDb my_hints. 
Hint Resolve H1 H2 : my_hints. 

現在我們可以完成證明：

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

一兩件事：勒柯克的參考手冊告訴（§8.9.1）我們

可以使用命令（可選）聲明一個提示數據庫。如果提示被添加到未知數據庫，它將自動創建。

但是，如果我們省略Create HintDb my_hints.部分，eauto策略將不起作用。當提示被添加到默認的core提示數據庫中時，它看起來是一樣的。

Answer 2

問題是透明度爲sentence。

大廈安東Trunov的答案，如果你看起來非常密切，你會發現，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爲什麼這樣表現......也許它拒絕統一使用不同類型的條款（如果?X的型號爲sentence，當X ++ X的型號爲list），或者它可能是一個保留基於元的統一......我打開了一個issue on the bugtracker about this lack of documentation/bad behavior。