Software Foundations: Normalization Function Exercise

Using Coq
1

Hey all, I just started making my way through Software Foundations since it seems like a good resource for learning to work with proofs in a computational context, and I’m pretty darn stuck on the last part of first 5 star exercise (binary_inverse in the induction chapter).

I’ve defined the relevant functions as follows:

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

Fixpoint nat_to_bin (n:nat) : bin :=
  match n with
  | O => 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.

With the theorem to prove being:

Theorem bin_nat_bin : forall b, nat_to_bin (bin_to_nat b) = normalize b.

Issue being that due to the way I’ve defined normalize, my proof attempts inevitably “simplify” into trying to prove the equivalence of different match statements, something the book has not taught me how to do, so I suspect I’ve taken a wrong turn somewhere.

Am I missing a more straight forward way to define normalize? Is there a simpler way to prove things with the definitions I’ve got? Or am I overlooking something else? Any kind of advice would be much appreciated, since I’m too stubborn to move on in the book with this unresolved.

2

If you take the inner match from the B0 case in your normalize definition and turn it into its own function, you can prove properties about its behavior, which you can then use to prove bin_nat_bin.

3

Thanks a bunch, I suppose my instinct to define things compactly got in my way there.