coq - 使用 Coq 证明存在量词

Question

假设我们有一个归纳数据结构和一些谓词:

Inductive A : EClass :=
   X | Y .

Definition P (a: A) : bool :=
 match a with
   X => true
 | Y => false
 end.

然后，我制定一个定理说存在一个元素 a 使得 P a 返回 true:

Theorem test :
 exists a: A, P a.

大概有多种实现方式，我在想如何用案例分析来证明，在我看来，它的工作原理是这样的:

• 记住 A 有两种构造方式
• 一条一条地尝试每一种方式，如果我们找到满足P a 的证人，就停止。

我的 Coq 代码如下所示:

evar (a: A). (* introduce a candidate to manipulate *)
destruct a eqn: case_A. (* case analysis *)
  - (* case where a = X *) 
    exists a.
    rewrite case_A.
    done.  
  - (* case where a = Y *) 
    (* stuck *)

我的问题是，

• 我的证明策略在逻辑上有缺陷吗？
• 如果不是，我的 Coq 就是问题所在，如果我找到一个证人，我该如何向 Coq 传达我的工作已经完成？可能是我不应该 destruct？

谢谢!

Answer 1

是的，你的证明是有缺陷的!您只需要先提供证人:

Inductive A := X | Y .

Definition P (a: A) : bool := match a with X => true | Y => false end.

Theorem test : exists a: A, P a = true.
Proof. now exists X. Qed.

如果你先做案例分析，你就会陷入死胡同。