0

我处于以下形式的目标的情况：

exists x : T1, f x = y.

哪里y : T2和f : T1 -> T2。诀窍是我已经定义了它们的构造函数T1并T2以这样的方式对应，所以对于人类来说，很容易看出什么值x将使相等成立。

但是，我有大量案例，并且希望我的脚本健壮，所以我想自动找到这样一个x.

我如何使用证明搜索来找到这样的值x？

现在我有这样的东西（借用 CPDT 的粉碎策略）：

Ltac postpone :=
 match goal with
  | [ |- ?X] => let H := fresh "Arg" in evar (H : X); apply H
  end
(unshelve eexists; [(constructor; postpone) | (crush ; fail) ]).

即我为 创建了一个evar x，将其搁置，使用构造函数求解，用evas填充构造函数生成的所有子目标，然后使用证明搜索来确定相等性。

但是，这给出了：Error: Tactic failure.我的意图是，如果constructor选择了错误的构造函数，crush将无法解决目标，因此fail会触发回溯。但这似乎没有发生，它在第一次命中时就失败了fail。

我的问题

我可以使用哪些策略让证明搜索找到存在变量的值？如何使用constructor's 回溯来找到使存在存在的价值？

4

1 回答 1

1

我认为您需要的只是unshelve eexists; [ econstructor | solve [ crush ] ]-solve [ ]在第一个目标中触发回溯。这是一个有效的示例。它包括一些从 T1 构造函数的参数创建的延迟目标。

Inductive T1 := T1A | T1B (x:unit) (H: x = x) | T1C (A:Type) (x:A) (H: x = x).
Inductive T2 := T2A | T2B | T2C.

Definition f (x:T1) : T2 :=
  match x with
  | T1A => T2A
  | T1B _ _ => T2B
  | T1C _ _ _ => T2C
  end.

Ltac crush := auto.

Goal exists x, f x = T2C.
Proof.
  unshelve eexists;
    [ econstructor | solve [ crush ] ].
于 2018-07-30T18:14:30.120 回答