使用特定证明实例化存在

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 *)

在这里我想使用这个策略，相信 tauto 找到的 f 只是 fun x => x，因此代入具体证明（应该是身份函数），而不仅仅是我当前脚本中的通用 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.

您需要类型归因 : T 以便术语 ltac:(tauto) 具有正确的目标（exists 期望的类型）。

我不确定这是否有用（通常证人的类型不是很有用，你想用目标的其余部分来选择它），但你能做到这一点很酷尽管如此。

使用特定证明实例化存在

Instantiating an existential with a specific proof

coq

ltac