使用特定證據實例化存在

Question

我正在嘗試使用可以輕鬆生成的術語（在此特定示例中，從tauto）實例化存在量詞的策略。我第一次嘗試：

Ltac mytac := 
    match goal with 
    | |- (exists (_ : ?X), _) => cut X; 
          [ let t := fresh "t" in intro t ; exists t; firstorder 
           | tauto ] 
    end. 

這種戰術將在一個簡單的問題，工作就像

Lemma obv1(X : Set) : exists f : X -> X, f = f. 
    mytac. 
Qed. 

但是它不會在一個目標的工作就像

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x. 
    mytac. (* goal becomes t x = x for arbitrary t,x *) 

在這裏，我想用這種策略，相信f哪tauto發現將只是fun x => x，因此潛在的具體證明（應該是身份函數）和d不僅僅是我當前腳本中的通用t。我可以怎樣去寫這種策略？

Answer 1

您可以使用eexists來引入一個存在變量，並讓它實例化它。

這給出了以下簡單的代碼。

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x. 
    eexists; tauto. 
Qed. 

Answer 2

這是更爲常見的創建一個存在變量，讓一些戰術（eauto或tauto例如）通過統一的實例變量。

在另一方面，你也可以從字面上使用策略提供使用戰術證人方面：

Ltac mytac := 
    match goal with 
    | [ |- exists (_:?T), _ ] => 
    exists (ltac:(tauto) : T) 
    end. 

Lemma obv1(X : Set) : exists f : X -> X, f = f. 
Proof. 
    mytac. 
    auto. 
Qed. 

您需要的類型歸屬: T使戰術，在長期ltac:(tauto)有權目標（類型exists預計）。

我不確定這是否有用（通常，證人的類型不是非常有用，你想用目標的其餘部分來選擇它），但很酷，你可以做到這一點。