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
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 : nat ⇒ S x + y) n.
Lemma sumToN1 : ∀ n : nat, n ≤ sumToN n.
Lemma sumToN2 : ∀ b a : nat, a ≤ b → sumToN a ≤ sumToN 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 d → a + b = c + d.
Lemma cPairInj1 : ∀ a b c d : nat, cPair a b = cPair c d → a = c.
Lemma cPairInj2 : ∀ a b c d : nat, cPair a b = cPair c d → b = d.
End CPair_Injectivity.
Section CPair_projections.
Let searchXY (a : nat) :=
boundedSearch (fun a y : nat ⇒ ltBool 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 a ≤ b → searchXY 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, a ≤ cPair a b.
Lemma cPairLe1A : ∀ a : nat, cPairPi1 a ≤ a.
Lemma cPairLe2 : ∀ a b : nat, b ≤ cPair a b.
Lemma cPairLe2A : ∀ a : nat, cPairPi2 a ≤ a.
Lemma cPairLe3 :
∀ a b c d : nat, a ≤ b → c ≤ d → cPair a c ≤ cPair 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.
Require Import Coq.Lists.List.
Require Import extEqualNat.
Require Import primRec.
Definition sumToN (n : nat) :=
nat_rec (fun _ ⇒ nat) 0 (fun x y : nat ⇒ S x + y) n.
Lemma sumToN1 : ∀ n : nat, n ≤ sumToN n.
Lemma sumToN2 : ∀ b a : nat, a ≤ b → sumToN a ≤ sumToN 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 d → a + b = c + d.
Lemma cPairInj1 : ∀ a b c d : nat, cPair a b = cPair c d → a = c.
Lemma cPairInj2 : ∀ a b c d : nat, cPair a b = cPair c d → b = d.
End CPair_Injectivity.
Section CPair_projections.
Let searchXY (a : nat) :=
boundedSearch (fun a y : nat ⇒ ltBool 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 a ≤ b → searchXY 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, a ≤ cPair a b.
Lemma cPairLe1A : ∀ a : nat, cPairPi1 a ≤ a.
Lemma cPairLe2 : ∀ a b : nat, b ≤ cPair a b.
Lemma cPairLe2A : ∀ a : nat, cPairPi2 a ≤ a.
Lemma cPairLe3 :
∀ a b c d : nat, a ≤ b → c ≤ d → cPair a c ≤ cPair 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