Skip to content

Instantly share code, notes, and snippets.

@yforster
Created September 18, 2023 08:40
Show Gist options
  • Save yforster/6ad75c48e86525567e5fe73eba967a6f to your computer and use it in GitHub Desktop.
Save yforster/6ad75c48e86525567e5fe73eba967a6f to your computer and use it in GitHub Desktop.
(** 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