Software foundations: stuck at exercise `binary_inverse` in the Induction chapter

Using Coq
1

Hi all, this my first time posting. I apologise in advance for any inaccuracies in my handling of the English language.

I’m a self-taught developer currently going through the exercises in Software Foundations. I’m stuck at the Induction chapter’s last exercise, binary_inverse.

The book provides two hints which unfortunately didn’t help me much.
The first is:

You may find you need to go back and change your earlier definitions to get things to work here

But, probably due to a lack of experience with formal proofs (or any kind of proof, really), I haven’t the faintest clue about the kind of reimplementation that would help.

The second provided hint is

If your definition of nat_to_bin involved any extra functions, you may need to prove a subsidiary lemma showing how such functions relate to nat_to_bin

But in my case the relation between my helper function and the nat_to_bin function is just the latter performing the initial call of the former, which I don’t really see how to take advantage of in a proof.

What I initially envisaged was trying to first prove that, for any binary number b, (incr b) = (B1 Z + b) as a first step toward making it possible to take advantage of the inductive hypothesis with the rewrite tactic in a proof by induction. But then I realised I would need to implement binary addition and it seems unlikely that the exercise would require to go to such lengths.

Could someone point me in the right direction?

Here is my implementation of nat_to_bin:

Fixpoint nat_to_bin' (b : bin) (n : nat) : bin :=
    match b, n with
    | b', O => b'
    | b', S n' => nat_to_bin' (incr b') n'
    end.

Definition nat_to_bin (n : nat) : bin :=
    nat_to_bin' Z n.
2

Hint: In nat_to_bin', accumulator b is not destructed, so the definition is equivalent to:

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

Does this remind you of a better way to define nat_to_bin?

3

Thank you Lys, your hint has been most helpful.

I had sort of automatically ruled out using incr as the outer function because my first instinct was to write a tail-recursive definition. But as it turns out, with the head-recursive definition, the proof practically writes itself. Thanks again!