Inductive bin :=
| zero : bin
| twice : bin -> bin
| twice_and_one : bin -> bin.

Fixpoint incr (b:bin) :=
match b with
| zero => twice_and_one zero
| twice b' => twice_and_one b'
| twice_and_one b' => twice (incr b')
end.

Fixpoint bin_to_nat (b:bin) : nat :=
match b with
| zero => 0
| twice b' => 2 * bin_to_nat b'
| twice_and_one b' => S (2* bin_to_nat b')
end.

Example test_bin_incr1 : bin_to_nat (zero) = 0.
Proof. reflexivity. Qed.

Example test_bin_incr2 : bin_to_nat (incr zero) = 1.
Proof. reflexivity. Qed.

Example test_bin_incr3 : bin_to_nat (incr (incr zero)) = 2.
Proof. reflexivity. Qed.

Example test_bin_incr4 : bin_to_nat (incr (incr (incr zero))) = 3.
Proof. reflexivity. Qed.

Example test_bin_incr5 : bin_to_nat (incr (twice_and_one (twice_and_one (twice_and_one zero)))) = 8.
Proof. reflexivity. Qed.

Fixpoint nat_to_bin (n:nat) :=
match n with
| 0 => zero
| S n' => incr (nat_to_bin n')
end.

Lemma incr_increments : forall b:bin, bin_to_nat (incr b) = S (bin_to_nat b).
Proof.
  induction b.
  - reflexivity.
  - reflexivity.
  - simpl.
    rewrite IHb.
    rewrite <- plus_n_O.
    rewrite <- plus_n_O.
    simpl.
    rewrite <- plus_n_Sm.
    reflexivity.
Qed.

Theorem nat_to_bin_to_nat : forall n:nat, bin_to_nat (nat_to_bin n) = n.
Proof.
  induction n.
  - reflexivity.
  - simpl.
    rewrite incr_increments.
    rewrite IHn.
    reflexivity.
Qed.

Fact bin_to_nat_to_bin_notwork : ~ forall b:bin, nat_to_bin (bin_to_nat b) = b.
Proof.
  intros h.
  assert (nat_to_bin (bin_to_nat (twice zero)) = zero).
  { reflexivity. }
  assert (nat_to_bin (bin_to_nat (twice zero)) = twice zero).
  { rewrite h. reflexivity. }
  congruence.
Qed.

Fixpoint normalize (b:bin) : bin :=
match b with
| zero => zero
| twice b' =>
  match normalize b' with
  | zero => zero
  | b'' => twice b''
  end
| twice_and_one b' => twice_and_one (normalize b')
end.

Lemma move_incr_out : forall b:bin, incr (normalize b) = normalize (incr b).
Proof.
  induction b.
  - reflexivity.
  - simpl.
    destruct (normalize b).
    + reflexivity.
    + reflexivity.
    + reflexivity.
  - simpl.
    rewrite <- IHb.
    destruct (normalize b).
    + reflexivity.
    + reflexivity.
    + reflexivity.
Qed.

Lemma move_twice_out : forall n:nat, nat_to_bin (2 * n) = normalize (twice (nat_to_bin n)).
Proof.
  intros n.
  induction n.
  - reflexivity.
  - assert (H : nat_to_bin (2 * S n) = incr (incr (nat_to_bin (2 * n)))).
    simpl.
    rewrite <- plus_n_O.
    rewrite <- plus_n_Sm.
    simpl.
    reflexivity.
    rewrite H.
    rewrite IHn.
    rewrite move_incr_out.
    rewrite move_incr_out.
    reflexivity.
Qed.

Theorem normalize_id : forall b:bin, normalize b = normalize (normalize b).
Proof.
  induction b.
  - reflexivity.
  - simpl. destruct (normalize b).
    + reflexivity.
    + simpl.
      rewrite IHb.
      simpl.
    Admitted.

Theorem bin_to_nat_to_bin_norm : forall b:bin, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  intros b.
  induction b.
  - reflexivity.
  - simpl.
    rewrite <- plus_n_O.
    assert (H:bin_to_nat b + bin_to_nat b = 2 * bin_to_nat b).
    { simpl. rewrite <- plus_n_O. reflexivity. }
    rewrite H.
    rewrite move_twice_out.
    simpl.
    rewrite IHb.
    rewrite <- normalize_id.
    reflexivity.
  - simpl.
    rewrite <- plus_n_O.
    assert (H:bin_to_nat b + bin_to_nat b = 2 * bin_to_nat b).
    { simpl. rewrite <- plus_n_O. reflexivity. }
    rewrite H.
    rewrite move_twice_out.
    simpl.
    rewrite IHb.
    rewrite <- normalize_id.
    destruct (normalize b).
    + reflexivity.
    + reflexivity.
    + reflexivity.
Qed.