Library pairing.cPair

The Cantor pairing function proved correct.

This code is part of Russell O'Connor's formalisation of Goedel's Incompleteness Theorem in Coq, released into the Public Domain.

http://r6.ca/Goedel/goedel1.html
Require Import Arith.
Require Import Coq.Lists.List.
Require Import extEqualNat.
Require Import primRec.

Definition sumToN (n : nat) :=
  nat_rec (fun _nat) 0 (fun x y : natS x + y) n.

Lemma sumToN1 : ∀ n : nat, nsumToN n.

Lemma sumToN2 : ∀ b a : nat, absumToN asumToN b.

Definition cPair (a b : nat) := a + sumToN (a + b).

Section CPair_Injectivity.

Remark cPairInjHelp :
 ∀ a b c d : nat, cPair a b = cPair c da + b = c + d.

Lemma cPairInj1 : ∀ a b c d : nat, cPair a b = cPair c da = c.

Lemma cPairInj2 : ∀ a b c d : nat, cPair a b = cPair c db = d.

End CPair_Injectivity.

Section CPair_projections.

Let searchXY (a : nat) :=
  boundedSearch (fun a y : natltBool a (sumToN (S y))) a.

Definition cPairPi1 (a : nat) := a - sumToN (searchXY a).
Definition cPairPi2 (a : nat) := searchXY a - cPairPi1 a.

Lemma cPairProjectionsHelp :
 ∀ a b : nat, b < sumToN (S a) → sumToN absearchXY b = a.

Lemma cPairProjections : ∀ a : nat, cPair (cPairPi1 a) (cPairPi2 a) = a.

Lemma cPairProjections1 : ∀ a b : nat, cPairPi1 (cPair a b) = a.

Lemma cPairProjections2 : ∀ a b : nat, cPairPi2 (cPair a b) = b.

End CPair_projections.

Section CPair_Order.

Lemma cPairLe1 : ∀ a b : nat, acPair a b.

Lemma cPairLe1A : ∀ a : nat, cPairPi1 aa.

Lemma cPairLe2 : ∀ a b : nat, bcPair a b.

Lemma cPairLe2A : ∀ a : nat, cPairPi2 aa.

Lemma cPairLe3 :
 ∀ a b c d : nat, abcdcPair a ccPair b d.

Lemma cPairLt1 : ∀ a b : nat, a < cPair a (S b).

Lemma cPairLt2 : ∀ a b : nat, b < cPair (S a) b.

End CPair_Order.

This page has been generated by coqdoc