使用回溯在 Coq 中寻找存在价值

Question

我的目标如下：

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) ]).

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

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

时失败了

我的问题

我可以使用什么策略让证明搜索找到存在变量的值？我怎样才能使用 constructor 的回溯来找到使存在保持不变的值？

Answer 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 ] ].

使用回溯在 Coq 中寻找存在价值

Using backtracking to find value for existential in Coq

theorem-proving

coq

dependent-type

coq-tactic

ltac