How to prove (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)

Question

I wish to prove the lemma below using Coq and mathcomp.classical_sets.

Let A × B - product of some sets, i.e. {(z1, z2) | z1 ∈ A /\ z2 ∈ B} Then (A × B = ∅) <-> (A = ∅) ∨ (B = ∅)

My proof is presented below:

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 context presented below:

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

I can't decompose H to do something like this:

1. Apply some lemmas from classical_sets.v
2. Trying to use induction

Answer 1

When working in classical logic, it is often useful to reason by "excluded middle" on a formula that you have to choose in a creative way.

Also, a guideline should be that you are performing mathematical proofs, without the constraint of expressing it in a formal language.

Here, the reasoning goes: if either A or B is empty, then the Cartesian product is empty, as expressed by theorems set0M and setM0. The next natural sentence is : if A is not empty and B is not empty, what do we do? This way of thinking should make us think about excluded middle. There is a theorem for that in the classical library, and its name is EM (a short name, which makes me think it should be used a lot).

Now there is another particular trick in the classical_sets file. It is given by theorem set0P. the notation !=set0 (no space between the = and set0), means nonempty, which in turn means that there exists an element in the set. Theorem set0P gives that if a set is not empty, then there is an element in it. If A and B are bot not empty, then we have an element in each of them and the pair of these elements is in the product of A and B.

Here is the script I run for this proof (tested with coq 8.17 and coq-mathcomp-classical 0.6.4. Note that I added Import classical_sets. in the prelude to make the text more readable.

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.