如何证明 (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)

Question

我希望使用 Coq 和 mathcomp.classical_sets 证明下面的引理。

设 A × B - 某些集合的乘积，即 {(z1, z2) | z1 Î A /\ z2 Î B} 那么 (A × B = ∅) <-> (A = ∅) ∨ (B = ∅)

我的证明如下：

From mathcomp.classical Require Import all_classical.

From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
From mathcomp Require Import ssrint interval.
From mathcomp Require Import mathcomp_extra boolp.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Context {T:Type}.
Implicit Types (A B C D:classical_sets.set T) (x:T).

Lemma zrch_ch1_p2_e6_a A B: (
  ((A `*` B) = classical_sets.set0 :> classical_sets.set (T * T))
    <-> (A = classical_sets.set0 :> classical_sets.set T) \/ (B = classical_sets.set0 :> classical_sets.set T)
)%classic.
  Proof.
    split.
    move=> H.
    rewrite /classical_sets.setM in H.
    (* Here i got stuck *)

Coq 上下文如下：

2 goals
A, B : set T
H : [set z | A z.1 /\ B z.2]%classic = classical_sets.set0
______________________________________(1/2)
A = classical_sets.set0 \/ B = classical_sets.set0
______________________________________(2/2)
A = classical_sets.set0 \/ B = classical_sets.set0 ->
(A `*` B)%classic = classical_sets.set0

我无法分解 H 来做这样的事情：

1. 应用 classic_sets.v 中的一些引理
2. 尝试使用归纳法

Answer 1

在使用经典逻辑时，通过“排除中间”对必须以创造性方式选择的公式进行推理通常很有用。

此外，指导方针应该是您正在执行数学证明，而不受用形式语言表达的限制。

这里的推理是：如果

A

或

B

为空，则笛卡尔积为空，如定理

set0M

和

setM0

所示。接下来的自然句子是：如果

A

不为空且

B

不为空，我们该怎么办？这种思维方式应该让我们思考排除中间。

classical

库中有一个定理，它的名字是

EM

（一个简短的名字，这让我觉得它应该被经常使用）。

现在

classical_sets

文件中还有另一个特殊技巧。它由定理 set0P 给出。符号

!=set0

（

=

和

set0

之间没有空格）表示

nonempty

，这又意味着集合中存在一个元素。定理

set0P

给出，如果集合不为空，则其中存在元素。如果

A

和

B

不为空，那么它们每个都有一个元素，并且这些元素对是

A

和

B

的乘积。

这是我为此证明运行的脚本（使用

coq

8.17 和

coq-mathcomp-classical

0.6.4 进行测试。请注意，我在序言中添加了

Import classical_sets.

以使文本更具可读性。

From mathcomp.classical Require Import all_classical.

From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
From mathcomp Require Import ssrint interval.
From mathcomp Require Import mathcomp_extra boolp.

Import classical_sets.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Context {T:Type}.
Implicit Types (A B C D:set T) (x:T).

Lemma zrch_ch1_p2_e6_a A B: (
  ((A `*` B) = set0 :> set (T * T))
    <-> (A = set0 :> set T) \/ (B = set0 :> set T))%classic.
Proof.
split; last first.
   by move=> [] ->; rewrite ?set0M ?setM0.
case: (EM (A = set0))=> [-> | /eqP ]; first by left.
case: (EM (B = set0)) => [-> | /eqP]; first by right.
rewrite !set0P=> -[] b Pb [] a Pa.
move=> abs.
suff : (a, b) \in set0 by rewrite inE.
by rewrite -abs inE /=.
Qed.