I'm trying to prove that product of countable types A and B is countable type too, using Cantor's pairing function. I'm following the Wikipedia article about it and I got stuck while proving theorem `Cantor_pairing_inv_thm`

.

Do you have hints how to better prove this part? Should I keep trying to make Wikipedia's approach work, or there's some better way?

Big thank you!

```
Require Import Nat Arith Lia.
Set Implicit Arguments.
Definition Cantor_pairing x y := ((x + y + 1) * (x + y)) / 2 + y.
Definition Cantor_pairing_inv (z: nat): nat * nat.
Proof.
set ((sqrt (8 * z + 1) - 1) / 2) as w. set (div (w * w + w) 2) as t. set (z - t) as y. set (w - y) as x.
exact (x, y).
Defined.
Theorem Cantor_pairing_inv_thm z x y: Cantor_pairing x y = z -> (x, y) = Cantor_pairing_inv z.
Proof.
intros. unfold Cantor_pairing in H. remember (x + y) as w. remember ((w + 1) * w / 2) as t.
assert (2 * t = w * w + w).
{ rewrite Heqt. clear Heqt Heqw. induction w; auto.
replace ((S w + 1) * S w) with ((w + 1) * w + (w + 1) * 2) by ring.
rewrite Nat.div_add. ring_simplify. rewrite IHw. ring. lia. }
assert (w = (sqrt (8 * z + 1) - 1) / 2).
{ admit. }
assert (y = z - t) by lia. assert (x = w - y) by lia.
unfold Cantor_pairing_inv. rewrite <- H1, <- H0. replace (2 * t) with (t * 2) by ring.
rewrite Nat.div_mul; try lia. f_equal; lia.
Admitted.
Definition injective A B (f: A -> B) := forall x y, f x = f y -> x = y.
Definition countable A := exists (f: A -> nat), injective f.
Theorem countable_mult A B: countable A -> countable B -> countable (A * B).
Proof.
intros. destruct H as [f H], H0 as [f0 H0].
exists (fun p => match p with (x, y) => Cantor_pairing (f x) (f0 y) end).
intros [x1 y1] [x2 y2] H1.
assert ((f x1, f0 y1) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x2, f0 y2) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x1, f0 y1) = (f x2, f0 y2)) by congruence.
inversion H4. apply H in H6. apply H0 in H7. congruence.
Qed.
```

Hi,

Cantor pairing function and its associated projections are the object of a file, part of Russel O'Connor's work on Gödel first incompleteness theorem. It's now maintained by coq-community, as a part of the hydra-battles project https://github.com/coq-community/hydra-battles

The file is https://github.com/coq-community/hydra-battles/blob/master/theories/ordinals/Ackermann/cPair.v

If you are interested by its content, some small editing would be necessary, in order to remove links to a lot of files (e.g. on primitive recursive functions) of the project and make this file self-contained.

You may look also at MathComp's formalization of choice and countable types

https://math-comp.github.io/htmldoc_1_14_0/mathcomp.ssreflect.choice.html

If you need help to make cPair.v autonomous, please tell me.

I managed to prove it using Wikipedia's approach, using theorems from Standard Library.

```
Require Import Nat Arith Lia.
Set Implicit Arguments.
Definition Cantor_pairing x y := ((x + y + 1) * (x + y)) / 2 + y.
Definition Cantor_pairing_inv (z: nat): nat * nat.
Proof.
set ((sqrt (8 * z + 1) - 1) / 2) as w. set (div (w * w + w) 2) as t. set (z - t) as y. set (w - y) as x.
exact (x, y).
Defined.
Theorem Cantor_pairing_inv_thm z x y: Cantor_pairing x y = z -> (x, y) = Cantor_pairing_inv z.
Proof.
intros. unfold Cantor_pairing in H. remember (x + y) as w. remember ((w + 1) * w / 2) as t.
assert (2 * t = w * w + w).
{ rewrite Heqt. clear Heqt Heqw. induction w; auto.
replace ((S w + 1) * S w) with ((w + 1) * w + (w + 1) * 2) by ring.
rewrite Nat.div_add. ring_simplify. rewrite IHw. ring. lia. }
assert ((2 * w + 1) * (2 * w + 1) <= 8 * z + 1) by lia.
assert (8 * z + 1 < (2 * S w + 1) * (2 * S w + 1)) by lia.
assert (2 * w + 1 <= sqrt (8 * z + 1)).
{ apply Nat.sqrt_le_square in H1. auto. }
assert (sqrt (8 * z + 1) < 2 * S w + 1).
{ apply Nat.sqrt_lt_square in H2. auto. }
assert (2 * w <= sqrt (8 * z + 1) - 1 < 2 * S w) by lia.
assert (w <= (sqrt (8 * z + 1) - 1) / 2).
{ apply Nat.div_le_lower_bound; lia. }
assert ((sqrt (8 * z + 1) - 1) / 2 < S w).
{ apply Nat.div_lt_upper_bound; lia. }
assert (w = (sqrt (8 * z + 1) - 1) / 2) by lia.
assert (y = z - t) by lia. assert (x = w - y) by lia.
unfold Cantor_pairing_inv. rewrite <- H8, <- H0. replace (2 * t) with (t * 2) by ring.
rewrite Nat.div_mul; try lia. f_equal; lia.
Qed.
Definition injective A B (f: A -> B) := forall x y, f x = f y -> x = y.
Definition countable A := exists (f: A -> nat), injective f.
Theorem countable_mult A B: countable A -> countable B -> countable (A * B).
Proof.
intros. destruct H as [f H], H0 as [f0 H0].
exists (fun p => match p with (x, y) => Cantor_pairing (f x) (f0 y) end).
intros [x1 y1] [x2 y2] H1.
assert ((f x1, f0 y1) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x2, f0 y2) = Cantor_pairing_inv (Cantor_pairing (f x2) (f0 y2))).
{ apply Cantor_pairing_inv_thm. auto. }
assert ((f x1, f0 y1) = (f x2, f0 y2)) by congruence.
inversion H4. apply H in H6. apply H0 in H7. congruence.
Qed.
```

Big thank you anyway! :)

Lessness has marked this topic as resolved.

@Lessness

Oops, I forgot to give a (maybe) useful information:

Gödel's proof mechanization (by Russel O'Connor) is maintained on Coq-community: https://github.com/coq-community/goedel

Note also a nice Gödel-like theorem, which I didn't have time to fully mechanize: "The termination of Goodstein sequences and hydra battles cannot be proven in Peano arithmetic" (see the paper by Kirby and Paris https://faculty.baruch.cuny.edu/lkirby/accessible_independence_results.pdf )

You can find results on Cantor pairing in the standard library: https://coq.inria.fr/library/Coq.Arith.Cantor.html

with some discussion and links: https://github.com/coq/coq/pull/14008

@Gert Smolka has a chapter on Cantor's pairing in his book: https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf#chapter.7

Last updated: Sep 28 2023 at 10:01 UTC