Stream: Coq users

Topic: ✔ Cantor pairing function and countability


view this post on Zulip Lessness (Jul 31 2022 at 17:49):

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.

view this post on Zulip Pierre Castéran (Jul 31 2022 at 19:10):

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

view this post on Zulip Pierre Castéran (Jul 31 2022 at 19:32):

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

view this post on Zulip Lessness (Jul 31 2022 at 20:28):

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.

view this post on Zulip Lessness (Jul 31 2022 at 20:30):

Big thank you anyway! :)

view this post on Zulip Notification Bot (Jul 31 2022 at 20:30):

Lessness has marked this topic as resolved.

view this post on Zulip Pierre Castéran (Aug 01 2022 at 07:08):

@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 )

view this post on Zulip Olivier Laurent (Aug 01 2022 at 14:39):

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

view this post on Zulip Olivier Laurent (Aug 01 2022 at 14:41):

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

view this post on Zulip Alexander Gryzlov (Aug 01 2022 at 17:08):

@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: Mar 29 2024 at 15:02 UTC