特定の証明で実在をインスタンス化する

Question

私は現在、容易に生成できる用語（この具体例では、tauto）を使用して存在量限定子をインスタンス化する手法を作成しようとしています。私の最初の試み：

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

それは私が使用したい

ここ

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

のような目標では動作しませんが、この戦術は

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

のような単純な問題に取り組みますこの手法は、fがtautoであることを確信しているだけで、fun x => xになります。したがって、特定の証明（識別関数である必要があります）に私の現在のスクリプトのgeneric tだけではありません。どのように私はそのような戦術を書くことに行くことができますか？

Answer 1

eexistsを使用して、存在変数を導入し、tautoをインスタンス化することができます。

これは、次の簡単なコードを与えます。

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. 

戦術・イン・用語が権利を有するltac:(tauto)ようにするには、型帰属: Tが必要目標（existsが期待するタイプ）。

これはすべて役に立ちます（通常、証人のタイプはあまり有益ではなく、残りの目標を使用して選択したいと考えています）が、これにもかかわらずこれを行うことは可能です。