I started working through the Software Foundations series as a way to learn Coq. I have previously studied logic and I’m not new to functional programming either.
Along the way, I’ve been experimenting with my own code and proofs beyond the official exercises. But I’ve hit a brick wall with one my attempts and wanted to see if someone could provide guidance on how to do what I’m trying to do.
In the Induction chapter, there’s a series of proofs about converting between unary and binary number representations. The final proof is to show that your normalize function is equivalent to turning a binary number into a unary one and back.
I followed all the directions for writing the other functions until that point and ended up with a straightforward proof that only needed one lemma (instead of the two the book said were likely required).
But after I was done, I wanted to find a way to prove that my normalize actually did what I intended, specifically that it removed all leading zeros from all binary number inputs. I then wanted to use that to prove that normalize was now uniquely specified: that any function that obeyed the properties I’ve proved about normalize must give the same outputs as my normalize when given the same inputs.
I am pretty sure I need the proof about the absence of leading zeros to prove that normalize is uniquely specified because it seems that there could be some alternative normalization scheme where you always had exactly one leading zero. (Or exactly one leading zero whenever the number was prime for that matter.)
I haven’t been able to figure out how to get the first proof to work, and so I haven’t even attempted the second one.
Can anyone provide some help on how to do this? Right now, I don’t know if the issue is that I’m not good enough with using tactics or if I’ve gone about trying to do this proof in a bad way that is making this harder than it has to be.
Here’s what I’ve tried as a starting point:
Fixpoint bin_tail (b : bin) : bin :=
match b with
| Z => Z
| B0 Z => B0 Z
| B1 Z => B1 Z
| B0 x => bin_tail x
| B1 x => bin_tail x
end.
Definition is_denorm (b : bin) : bool :=
match bin_tail b with
| B0 Z => true
| _ => false
end.
Lemma tail_norms : forall b, normalize (bin_tail b) = bin_tail (normalize b).
Proof. Admitted.
Lemma norm_norms : forall b, is_denorm (normalize b) = false.
Proof. Admitted.
I tried a different approach using the nat_to_bin function:
Example nat_never_B0Z : forall n, not (nat_to_bin n = (B0 Z)).
Proof. Admitted.
None of these got me anywhere. Any help would be appreciate.