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,
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
(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.