1

我目前正在尝试编写一种策略，该策略使用可以轻松生成的术语（在此特定示例中， from 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 *)

在这里，我想使用这种策略，相信fwhich tautofinds 将是 just fun x => x，从而替换特定证明（应该是身份函数），而不仅仅是t我当前脚本中的泛型。我该如何编写这样的策略？

4

2 回答 2

3

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期望的类型）。

我不确定这是否有用（通常见证人的类型信息量不大，您想使用目标的其余部分来选择它），但是您仍然可以这样做很酷。

于 2017-10-17T14:13:53.883 回答
2

您可以使用eexists引入一个存在变量，并让tauto实例化它。

这给出了以下简单的代码。

Lemma obv2(X : Set) : exists f : X -> X, forall x, f x = x.
  eexists; tauto.
Qed.
于 2017-10-17T13:56:45.413 回答