I have defined an Inductive in Coq for binary representation of natural numbers as follows:
Inductive bin : Type := | Z : bin | T : bin -> bin | M : bin -> bin.
and two recursive functions to convert between nat and bin types as:
Fixpoint nat_to_bin (n : nat) : bin := match n with | O => Z | S n' => incr (nat_to_bin n') end.
Fixpoint bin_to_nat (b : bin) : nat := match b with | Z => O | M b' => S (mult 2 (bin_to_nat b')) | T b' => mult 2 (bin_to_nat b') end.
to show that bin_to_nat is the inverse of nat_to_bin I need to prove that
T Z = Z by using these tactics that I know:
simpl reflexivity destruct rewrite replace induction please recommend some clues showing how to do this. Thank you!
The incr implementation is
Fixpoint incr (b : bin) : bin := match b with | Z => M Z | T b' => M b' | M b' => T (incr b') end.