使用 Coq 证明存在量词

Posted 2023-03-29

【中文标题】使用 Coq 证明存在量词

【英文标题】：Prove existential quantifier using Coq

【发布时间】：2017-09-24 13:19:30

【问题描述】：

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

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？

谢谢！

【参考方案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.

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

【参考方案2】：

这是一个粗略的框架，演示了如何编写 Coq 策略以尝试将有限类型的所有元素作为见证。

(* Typeclass to register an enumeration of elements of a type. *)
Class Enumeration (A:Type) :=
enumerate : list A.
Arguments enumerate A [Enumeration].

(* Typeclass to register decision procedures to determine whether
   a given proposition is true or false. *)
Class Decision (P:Prop) :=
decide : P + ~P.
Arguments decide P [Decision].

(* Given a Coq list l, execute tactic t on every element of
   l until we get a success. *)
Ltac try_list l t :=
match (eval hnf in l) with
| @cons _ ?hd ?tl => (t hd || try_list tl t)
end.
(* Tactic for "proof by reflection": use a decision procedure, and
   if it returns "true", then extract the proof from the result. *)
Ltac by_decision :=
match goal with
|- ?P => let res := (eval hnf in (decide P)) in
         match res with
         | left ?p => exact p
         end
end.
(* Combination to try to prove an (exists x:A, P) goal by trying
   to prove P by reflection for each element in an enumeration of A. *)
Ltac try_enumerate :=
match goal with
|- @ex ?A ?P =>
  try_list (enumerate A)
    ltac:(fun x => exists x; by_decision)
end.

(* Demonstration on your example *)
Inductive A := X | Y.
Instance A_enum : Enumeration A :=
cons X (cons Y nil).
Instance bool_eq_dec : forall x y:bool,
  Decision (x = y).
Proof.
intros. red. decide equality.
Defined.

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

Goal exists a:A, P a = true.
Proof.
try_enumerate.
Qed.