# Software foundations: stuck at exercise \`binary\_inverse\` in the Induction chapter

**URL:** <https://discourse.rocq-prover.org/t/software-foundations-stuck-at-exercise-binary-inverse-in-the-induction-chapter/1378>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [July 4, 2021, 7:47pm UTC](https://discourse.rocq-prover.org/t/software-foundations-stuck-at-exercise-binary-inverse-in-the-induction-chapter/1378 "2021-07-04T19:47:50Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![YaVeremos](https://avatars.discourse-cdn.com/v4/letter/y/c77e96/32.png) [@YaVeremos](https://discourse.rocq-prover.org/u/YaVeremos)\
**Post date:** [July 4, 2021, 7:47pm UTC](https://discourse.rocq-prover.org/t/software-foundations-stuck-at-exercise-binary-inverse-in-the-induction-chapter/1378/1 "2021-07-04T19:47:50Z")

</div>

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](https://softwarefoundations.cis.upenn.edu/lf-current/Induction.html) 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:

```auto
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.

```

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [July 4, 2021, 11:40pm UTC](https://discourse.rocq-prover.org/t/software-foundations-stuck-at-exercise-binary-inverse-in-the-induction-chapter/1378/2 "2021-07-04T23:40:44Z")

</div>

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

```auto
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`?

---

<div class="post-metadata">

**Author:** ![YaVeremos](https://avatars.discourse-cdn.com/v4/letter/y/c77e96/32.png) [@YaVeremos](https://discourse.rocq-prover.org/u/YaVeremos)\
**Post date:** [July 6, 2021, 11:52am UTC](https://discourse.rocq-prover.org/t/software-foundations-stuck-at-exercise-binary-inverse-in-the-induction-chapter/1378/3 "2021-07-06T11:52:34Z")

</div>

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!