Cantor_ex.v

(** 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.