Created
September 18, 2023 08:40
-
-
Save yforster/6ad75c48e86525567e5fe73eba967a6f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** Implementation of the Cantor pairing and its inverse function *) | |
Require Import PeanoNat Lia. | |
(** Bijections between [nat * nat] and [nat] *) | |
(** Cantor pairing [to_nat] *) | |
Fixpoint to_nat' z := | |
match z with | |
0 => 0 | |
| S i => S i + to_nat' i | |
end. | |
Definition to_nat '(x, y) : nat := | |
y + to_nat' (y + x). | |
(** Cantor pairing inverse [of_nat] *) | |
Fixpoint of_nat (n : nat) : nat * nat := | |
match n with | |
| 0 => (0,0) | |
| S i => let '(x,y) := of_nat i in | |
match x with | |
| 0 => (S y, 0) | |
| S x => (x, S y) | |
end | |
end. | |
(** [of_nat] is the left inverse for [to_nat] *) | |
Lemma cancel_of_to p : of_nat (to_nat p) = p. | |
Proof. | |
enough (H : forall n p, to_nat p = n -> of_nat n = p) by now apply H. | |
Admitted. | |
(** [to_nat] is injective *) | |
Corollary to_nat_inj p q : to_nat p = to_nat q -> p = q. | |
Proof. | |
Admitted. | |
(** [to_nat] is the left inverse for [of_nat] *) | |
Lemma cancel_to_of n : to_nat (of_nat n) = n. | |
Proof. | |
Admitted. | |
(** [of_nat] is injective *) | |
Corollary of_nat_inj n m : of_nat n = of_nat m -> n = m. | |
Proof. | |
Admitted. | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment