A bijection nat <-> nat * nat

Encoding.v

(*
   Encoding.v: A bijection nat <-> nat * nat

   Definition of a bijection between nat and nat * nat. With this, we
   can encode several objects using natural numbers.

*)

Require Import Coq.Arith.Div2.
Require Import Coq.Arith.EqNat.
Require Import Compare_dec.
Require Import Recdef.
Require Import Omega.

(* Triangular numbers *)
Fixpoint triangle (n : nat) :=
  match n with
    | 0 => 0
    | S n' => n + triangle n'
  end.

Lemma triangle_1 : forall n, n > 0 -> triangle n >= 1.
Proof.
  intros n H.
  destruct n as [|n]; simpl; try abstract omega.
Qed.

Lemma triangle_grows : forall n, n > 1 -> triangle n > n.
Proof.
  intros n H.
  destruct n as [|[|n]]; simpl; try abstract omega.
Qed.

Lemma ge_split : forall n m, n >= m -> exists n', n = n' + m.
Proof.
  induction n.
  - intros m H.
    destruct m as [|m]; try abstract omega.
    exists 0. trivial.
  - intros m H.
    destruct m as [|m].
    + exists (S n). abstract omega.
    + assert (Hnm : n >= m) by omega.
      destruct (IHn m Hnm) as [n' Hn'].
      exists n'. abstract omega.
Qed.

Lemma triangle_monotone : forall n m,
  n >= m -> triangle n >= triangle m.
Proof.
  intros n m H.
  induction n.
  - assert (m = 0) by abstract omega. subst. auto.
  - assert (H' : S n = m \/ n >= m) by abstract omega.
    destruct H' as [H' | H']. subst. omega.
    simpl. specialize (IHn H'). omega.
Qed.

Lemma triangle_monotone_strict : forall n m,
  n > m -> triangle n > triangle m.
Proof.
  intros n m H.
  induction n. inversion H.
  assert (H' : n > m \/ n = m) by omega.
  destruct H' as [H' | H'].
  - specialize (IHn H'). simpl. omega.
  - subst. simpl. omega.
Qed.

(*
   The actual encoding. Graphically, we traverse nat * nat by going
   along the diagonals:

           0  1  2  3  4  5  6 n
        +----------------------
      0 |  0  1  3  6 10 15 21
      1 |  2  4  7 11 16 22
      2 |  5  8 12 17 23
      3 |  9 13 18 24
      4 | 14 19 25
      5 | 20 26
      6 | 27
      m

   which can be expressed in terms of triangular numbers: given a pair
   (n, m), its assigned number will be given by its position along its
   diagonal plus the size of the biggest triangle that can fit before
   it. There is also an explicit formula, given by (n + m)(n + m +
   1)/2 + m.

*)

Definition pair_nat (n m : nat) : nat :=
  m + triangle (m + n).

Lemma pair_nat_Snm : forall n m,
  S (pair_nat (S n) m) = pair_nat n (S m).
Proof.
  intros n m. unfold pair_nat.
  replace (m + S n) with (S m + n); try omega.
Qed.

Lemma pair_nat_0m: forall m,
  S (pair_nat 0 m) = pair_nat (S m) 0.
Proof.
  intros m. unfold pair_nat. simpl.
  replace (m + 0) with m; try omega.
Qed.

(* To define the inverse, we iterate a step function from the starting
   point (0, 0). *)

Definition next_pair (p : nat * nat) : nat * nat :=
  let (n, m) := p in
    match n with
      | 0 => (S m, 0)
      | S n => (n, S m)
    end.

Definition get_nm k := nat_iter k next_pair (0, 0).

Lemma pair_nat_next_pair : forall p,
  pair_nat (fst (next_pair p)) (snd (next_pair p)) =
  S (pair_nat (fst p) (snd p)).
Proof.
  intros [[|n] m]; simpl;
  auto using pair_nat_0m, pair_nat_Snm.
Qed.

(* First inverse lemma *)
Lemma pair_nat_get_nm : forall k,
  let p := get_nm k in
  pair_nat (fst p) (snd p) = k.
Proof.
  unfold get_nm.
  induction k as [|k]; simpl; trivial.
  rewrite pair_nat_next_pair.
  congruence.
Qed.

Lemma nat_iter_next_pair_move : forall k n m,
  nat_iter k next_pair (k + n, m) = (n, k + m).
Proof.
  intros k n.
  induction k as [|k]. trivial.
  intros m.
  rewrite nat_iter_succ_r. simpl.
  rewrite IHk. f_equal.
  omega.
Qed.

Lemma get_nm_triangle : forall n,
  nat_iter (triangle n) next_pair (0, 0) = (n, 0).
Proof.
  induction n as [|n]. trivial.
  simpl.
  rewrite nat_iter_plus.
  rewrite IHn.
  replace (n, 0) with (n + 0, 0); try (f_equal; omega).
  rewrite nat_iter_next_pair_move. simpl.
  f_equal. omega.
Qed.

(* The other inverse lemma *)
Lemma get_nm_pair_nat : forall n m,
  get_nm (pair_nat n m) = (n, m).
Proof.
  intros n m. unfold get_nm, pair_nat.
  rewrite nat_iter_plus.
  rewrite get_nm_triangle.
  rewrite nat_iter_next_pair_move.
  f_equal. omega.
Qed.

(* A more convenient way of using the above *)

Definition fst_nat (p : nat) : nat :=
  fst (get_nm p).

Definition snd_nat (p : nat) : nat :=
  snd (get_nm p).

Lemma pair_nat_proj : forall p, pair_nat (fst_nat p) (snd_nat p) = p.
Proof.
  intros p. unfold fst_nat, snd_nat.
  apply pair_nat_get_nm.
Qed.
Hint Resolve pair_nat_proj.
Hint Rewrite pair_nat_proj : pairs.

Lemma fst_pair_nat : forall n m, fst_nat (pair_nat n m) = n.
Proof.
  intros n m. unfold fst_nat.
  rewrite get_nm_pair_nat. trivial.
Qed.

Lemma snd_pair_nat : forall n m, snd_nat (pair_nat n m) = m.
Proof.
  intros n m. unfold snd_nat.
  rewrite get_nm_pair_nat. trivial.
Qed.

(* In order to be able to use this encoding and define functions with
   it, we need to be able to recurse on the pair components. We do
   this by showing that projections almost always give back a strictly
   smaller number, which we can use to perform well-founded
   recursion. *)

Lemma snd_nat_lt : forall p, p > 0 ->
  snd_nat p < p.
Proof.
  intros p H.
  induction p as [|p]. inversion H.
  unfold snd_nat, get_nm in *. simpl.
  destruct p as [|p]. simpl. omega.
  assert (H' : S p > 0). omega.
  specialize (IHp H'). clear H H'.
  destruct (nat_iter (S p) next_pair (0, 0)) eqn: ?.
  destruct n as [|n]; simpl. omega.
  simpl in IHp. omega.
Qed.

Lemma fst_nat_lt : forall p, p > 1 ->
  fst_nat p < p.
Proof.
  intros p H.
  induction p as [|p]. inversion H.
  destruct p as [|p]. omega.
  destruct p as [|p]. compute. omega.
  assert (H' : S (S p) > 1). omega.
  specialize (IHp H'). clear H H'.
  replace (fst_nat (S (S (S p)))) with (fst (next_pair (get_nm (S (S p))))).
  - assert (snd_nat (S (S p)) < S (S p)). apply snd_nat_lt. omega.
    unfold fst_nat, snd_nat in *.
    destruct (get_nm (S (S p))) eqn: ?.
    simpl in *.
    destruct n as [|n]; simpl; omega.
  - clear IHp.
    unfold fst_nat. f_equal.
Qed.

Lemma pair_nat_lt_m : forall n m, m > 0 ->
  m < pair_nat n m.
Proof.
  intros n m H.
  destruct m as [|m]. inversion H. clear H.
  unfold pair_nat. simpl. omega.
Qed.

Lemma pair_nat_lt_n : forall n m, n > 1 ->
  n < pair_nat n m.
Proof.
  intros n m H.
  destruct n as [|[|n]]; try omega. clear H.
  unfold pair_nat.
  replace (m + S (S n)) with (S (S n) + m); try omega.
  simpl. omega.
Qed.