Ben*_*son 3 theorem-proving coq dependent-type
我已经证明是等效的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)
（有关背景，我通过工作逻辑基础 ;我上了In_map_iff建设性的逻辑章的练习，请不要告诉我解决了运动虽然。！）
我试图用rewrite and_distributes_over_or自己的目标来获得exists x0 : A, (f x0 = y /\ x = x0) \/ (f x0 = y /\ In x0 xs)。我收到一个错误：
Found no subterm matching "?P /\ (?P0 \/ ?P1)" in the current goal.
用我的大脑，我可以看到目标中该形式的一个非常明显的子术语。为什么带有非人类非大脑功能的Coq不能在存在量词下看到它？你有什么技巧可以使这项工作吗？
我读过一个与该标题相似的上一个问题，但这是关于用假设而不是目标进行改写，并且答案似乎不适用于我的情况。
只需使用setoid_rewrite代替rewrite，并确保Require Setoid.（尽管List在这种情况下，加载已经完成了）。
Coq所寻找的图案在活页夹下面；也就是说，它在函数的主体中。活页夹不是很明显，因为它是的一部分exists，但是您的目标实际上是ex (fun (x0:A) => f x0 = y /\ (x = x0 \/ In x0 xs))，Coq的表示法将它很好地打印为exists x0, ...。基本rewrite策略不能在函数内部进行重写，但是setoid_rewrite可以。
另外：请注意，该定义ex及其符号exists x, ...不是Coq内置的，而是在标准库中定义的！您可以使用Locate exists（查找符号）和Print ex（查看定义）检查此类事物。还有Unset Printing Notations.，如果你不知道什么样的注释都在使用，但请记住，有很多你可能觉得理所当然，像符号的/\，=甚至->。