通过提供一个例子来证明存在

Question

如果我有一个形式为的定理

Theorem my_thm (n: nat -> nat): exists t: nat, n t = 0.
Admitted.

如果我想为my_func 0 = 0这样的函数证明它，我如何告诉coq确实存在这样的t，因为my_func 0=0？

这并没有一个深刻的目标，但理解存在证明在coq中是如何工作的。

Answer 1

您可以添加一个参数，此处为P，它将断言此属性成立，并在稍后的定理中使用exists策略。例如(我正在使用ssreflect，但我想你会明白的(：

Theorem my_thm (n: nat -> nat) (P : n 0 = 0) : exists u, n u = 0.
Proof.
exists 0.
exact: P.
Qed.

当然，您也可以更改定理体以更好地满足您的需求。