correct binary to natural number conversion

nat-bin.v

Require Import Omega.
Require Import Extraction.

(* Inductive binary number data type. *)
Inductive bin : Type :=
 | Z
 | A (n : bin)
 | B (n : bin).


(* Increment a binary number. *)
Fixpoint incr (m:bin) : bin :=
  match m with
  | Z => B Z
  | A n => B n
  | B n => A (incr n)
  end.

(* Some test cases. *)
Example test_incr1: (incr Z) = B Z.
Proof. reflexivity. Qed.

Example test_incr2: (incr (A (B Z))) = B (B Z).
Proof. reflexivity. Qed.

Example test_incr3: (incr (B (B (B Z)))) = (A (A (A (B Z)))).
Proof. reflexivity. Qed.

(* Convert a binary number to a natural number. *)
Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | Z => 0
  | A n => (2 * (bin_to_nat n))
  | B n => S (2 * (bin_to_nat n))
  end.

(* Convert a natural number to a binary number. *)
Fixpoint nat_to_bin (n:nat) : bin :=
  match n with
  | 0 => Z
  | S n' => incr (nat_to_bin n')
  end.

(* Some test cases. *)
Example test_bin_to_nat1: bin_to_nat (A (A (B Z))) = 4.
Proof. reflexivity. Qed.

Example test_bin_to_nat2: bin_to_nat (B (A (B Z))) = 5.
Proof. reflexivity. Qed.

Example test_nat_to_bin1: nat_to_bin 5 = (B (A (B Z))).
Proof. reflexivity. Qed.


(* An incr can be "factored" out into a succ across a bin_to_nat. *)

(* This proof is long because we have to perform induction over the
   type constructors of binary numbers. *)
Lemma succ_to_incr_eqv :
  forall n : bin,
    S (bin_to_nat n) = (bin_to_nat (incr n)).
Proof.
  intros n.
  induction n.
  - reflexivity.
  - reflexivity.
  - simpl.
    assert (H: forall n : nat, n + 0 = n). {
      auto.
    }
    rewrite <- IHn, H, H.
    destruct n.
    + reflexivity.
    + simpl. rewrite H. apply f_equal.
      assert (H1: forall a : nat, S (a + a + (a + a)) = a + a + S (a + a)). {
        auto.
      }
      rewrite <- H1. reflexivity.
    + rewrite IHn. rewrite <- IHn.
      omega.
Qed.

(* incr can be factored out of a bin_to_nat and simplified into S
   n. *)
Theorem incr_over_bin_to_nat :
  forall n : nat,
    bin_to_nat (incr (nat_to_bin n)) = S n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. rewrite <- IHn. rewrite <- succ_to_incr_eqv. reflexivity.
Qed.

(* Converting a natural number to a binary and back again results in
   the same number. *)
Theorem nat_to_bin_and_back :
  forall n : nat,
    (bin_to_nat (nat_to_bin n)) = n.
Proof.
  intros.
  induction n; simpl.
  - reflexivity.
  - rewrite incr_over_bin_to_nat. reflexivity.
Qed.


Extraction Language OCaml.
Recursive Extraction nat_to_bin bin_to_nat.