How to prove that nat_to_bin combines bin_to_nat b = normalize b in Coq

Question

I am a green hand in studying Coq with the reference book softwarefoundation-induction

In the last part of this phrase, there is an exercise about proving that

change a binary to a nature number and change it back to binary is equivalence to itself.

which is the last theorem bin_nat_bin

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with 
  | Z => 0
  | B0 (m') => 2 * bin_to_nat(m')
  | B1 (m') => S (2 * bin_to_nat(m')) 
  end.

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

Fixpoint normalize (b:bin) : bin :=
  match b with
  | Z => Z
  | B0 b' =>
    match (normalize b') with
    | Z => Z
    | b'' => B0 b''
    end
  | B1 b' => B1 (normalize b')
  end.

Theorem bin_nat_bin : forall b : bin, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
    (* FILL IN HERE *) Admitted.

At first, I tried to induction b as follows.

Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  intros b. induction b as [|b'|b''].
  - simpl. reflexivity. 
  - simpl. rewrite add_0_r. simpl.

And get these

1 goal
b' : bin
IHb' : nat_to_bin (bin_to_nat b') = normalize b'
______________________________________(1/1)
nat_to_bin (bin_to_nat b' + bin_to_nat b') =
match normalize b' with
| Z => Z
| B0 n => B0 (B0 n)
| B1 n => B0 (B1 n)
end

I want to know that to proof this subgoal,

if I need to change the '+' between bin_to_nat b' into a construct function double_bin

Definition double_bin (b:bin) : bin :=
  match b with
  | Z => Z
  | m => B0 (m)
  end.

and bridge the gap between them (I don't know clearly how to do this. Please give me some tips)

or to do as the hint put it

Hint: Start by trying to prove the main statement, see where you get stuck, and see if you can find a lemma -- perhaps requiring its own inductive proof -- that will allow the main proof to make progress. We have one lemma for the B0 case (which also makes use of double_incr_bin) and another for the B1 case.

Could you please offer me some more detailed or practical measures or hints?

Thank you.

Answer 1

It's better to define normalize with double_bin and incr. We can then argue the property is hold while converting from nature number to binary, like forall m , nat_to_bin (m + m) = double_bin (nat_to_bin m).

Answer 2

As suggested by @sozzzzz, it is helpful to define some helper lemmas and definitions that can aid the proof because directly proving this theorem requires some non-trivial transformation.

Fixpoint double (n : nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Definition double_bin (b : bin) : bin :=
  match b with
  | Z => Z
  | B0 z' => B0 (B0 z')
  | B1 z' => B0 (B1 z')
  end.
  
Lemma double_plus : forall n,
  double n = n + n.
Proof.
  intros n. induction n as [ | n' H ].
  - reflexivity.
  - simpl. rewrite -> H. rewrite <- plus_n_Sm. reflexivity.
Qed.

Theorem bin_to_nat_pres_incr : forall b : bin,
  bin_to_nat (incr b) = S (bin_to_nat b).
Proof.
  induction b; auto.
  simpl. repeat rewrite <- plus_n_O.
  rewrite IHb.
  rewrite plus_Sn_m.
  f_equal. 
  (* Require Import Arith. *)
  apply Nat.add_comm.
Qed.

Theorem nat_bin_nat : forall n,
  bin_to_nat (nat_to_bin n) = n.
Proof.
  intros n. induction n as [ | n' H].
  - reflexivity.
  - simpl.
    rewrite bin_to_nat_pres_incr. auto.
Qed.

Lemma double_incr_bin : forall b : bin,
    double_bin (incr b) = incr (incr (double_bin b)).
Proof.
  destruct b; auto.
Qed.

Lemma double_bin_exchange: forall n : nat,
  nat_to_bin (double n) = double_bin (nat_to_bin n).
Proof.
  intros n. induction n as [| n' H].
  - reflexivity.
  - simpl. rewrite -> double_incr_bin. rewrite -> H. reflexivity.
Qed.

Lemma incr_double: forall b : bin,
  incr (double_bin b) = B1 b.
Proof.
  destruct b; auto.
Qed.

Theorem bin_nat_bin : forall b : bin, nat_to_bin (bin_to_nat b) = normalize b.
Proof.
  intros.
  induction b.
  - auto.
  - simpl. rewrite <- IHb.
    rewrite <- plus_n_O.
    rewrite <- double_plus.
    rewrite double_bin_exchange.
    unfold double_bin.
    reflexivity.
  - simpl. rewrite <- plus_n_O.
    rewrite <- IHb.
    rewrite <- double_plus.
    rewrite <- incr_double.
    rewrite double_bin_exchange.
    reflexivity.
Qed.