coq - 目标中存在下的重写等价

Question

我已经证明了等价and_distributes_over_or:

Theorem and_distributes_over_or : forall P Q R : Prop,
  P /\ (Q \/ R) <-> (P /\ Q) \/ (P /\ R).

在其他地方我有一个目标

exists x0 : A, f x0 = y /\ (x = x0 \/ In x0 xs)

(对于上下文，我正在研究 Logical Foundations ；我在 the In_map_iff exercise of the chapter on constructive logic 上。请不要告诉我练习的解决方案!)

我尝试使用 rewrite and_distributes_over_or 实现我的目标(得到 exists x0 : A, (f x0 = y/\x = x0)\/(f x0 = y/\在 x0 xs))。我收到一个错误:

Found no subterm matching "?P /\ (?P0 \/ ?P1)" in the current goal.

使用我的人脑，我可以看到在目标中似乎是该形式的一个非常明显的子项。为什么 Coq 的非人类非大脑无法在存在量词下看到它？您有什么技巧可以使这项工作成功吗？

我读过 a previous question with a similar title to this one但那是关于重写假设，而不是目标，答案似乎不适用于我的情况。

Answer 1

只需使用 setoid_rewrite 而不是 rewrite，并确保 Require Setoid.(虽然加载 List 有在这种情况下已经这样做了)。

Coq 正在寻找的模式在 Binder 下面；也就是说，它在函数体中。 Binder 并不明显，因为它是 exists 的一部分，但您的目标实际上是 ex (fun (x0:A) => f x0 = y/\(x = x0\/在 x0 xs)) 中，Coq 的符号机制将它很好地打印为 exists x0, ...。基本的 rewrite 策略不能在函数内部进行重写，但是 setoid_rewrite 可以。

另外:请注意定义 ex 及其符号 exists x, ... 不是 Coq 内置的，而是在标准库中定义的!您可以使用 Locate exists(查找符号)和 Print ex(查看定义)来检查此类内容。还有 Unset Printing Notations。 如果您不确定正在使用什么符号，请记住，有很多符号您可能认为是理所当然的，例如 /\、=，甚至 ->。