I'm working my way through the Logic Foundations on my own, and I got stumped in part
I came up with the following definition for
Fixpoint normalize (b : bin) : bin := match b with | Z => Z | B1 b' => B1 (normalize b') | B0 b' => match (normalize b') with | Z => Z | b'' => B0 b'' end end.
... but I'm afraid I've got a bad definition for this, because very often I end up having to prove things of this form:
match incr (...) with | Z => Z
... which seems like a dead end, sinc the result of
incr cannot never be
I've tried an alternative formulation:
Fixpoint is_zero (b : bin) : bool := match b with | Z => true | B1 _ => false | B0 b' => is_zero b' end. Fixpoint normalize (b : bin) : bin := match b with | Z => Z | B1 b' => B1 (normalize b') | B0 b' => match (is_zero b') with | true => Z | false => B0 b' end end.
But using this I end up with either contractions in my context or having to prove them. Since these first two chapters do not teach tactics like
inversion, it feels like using those future tactics would be cheating.
As a hint, can anyone who have successfully completed the exercise give a hint on the correct form of
your first definition of
normalize looks good to me. Can you be more precise what problems you have in the proofs with it?
One example is trying to prove the following lemma (which I used to successfully prove
binary_inverse_c after marking it
Admitted. :see_no_evil: ):
Lemma normalize_normalize : forall (b : bin), normalize (normalize b) = normalize b. Proof. induction b as [| b IHb | b IHb]. - reflexivity. - simpl. destruct (normalize b). + reflexivity. + simpl. rewrite <- IHb. simpl. (* stuck?! *) Admitted.
I end up with a goal of the form:
1 subgoal (ID 149) b, b0 : bin IHb : normalize (B0 b0) = B0 b0 ============================ match match normalize b0 with | Z => Z | B0 n => B0 (B0 n) | B1 n => B0 (B1 n) end with | Z => Z | B0 n => B0 (B0 n) | B1 n => B0 (B1 n) end = B0 match normalize b0 with | Z => Z | B0 n => B0 (B0 n) | B1 n => B0 (B1 n) end
... which seems contradictory, since the LHS could, in principle, yield a
Z, while the RHS cannot. I believe the difficulty seems to arise from the fact that there is no relation between
b0 (which came from the
destruct) and the original
b from the induction.
Something similar arises when trying to prove the following (I also used this in the final theorem):
Lemma double_bin : forall (n : nat), nat_to_bin (double n) = normalize (B0 (nat_to_bin n)). Proof. induction n as [| n IHn]. - reflexivity. - simpl. rewrite normalize_incr_comm. rewrite normalize_nat_to_bin_id. rewrite IHn. simpl. Admitted.
normalize_normalize you just need to simplify
simpl in IHb)
@Laurent Théry Indeed, that trick did it! Thanks for showing me that usage! :beers:
Maybe with this I can advance the other stuck lemmas.
But I searched the first two chapters and I could not find any mentions of
simpl in. Which makes me wonder... Does that mean that this exercise really needs "things from the future" (It seems the first mention of
simpl in is in
Tactics.v), or perhaps I messed up some detail?
(BTW, indeed it seems that
simpl in was the missing piece. With that, I managed to finally finish the exercise.)
An alternative way (not using
simpl in _) is to realize that
simpl is doing too much when you apply it to
normalize (B0 (B0 b0)). It is eating two
B0 whule you would like it to eat only the top one. For this, you can prove an intermediate theorem
Lemma normalizeB0 x : normalize (B0 x) = match (normalize x) with | Z => Z | b => B0 b end.
whose proof is easy and now instead of
simpl you just use
Nice! Another thing I didn't realize: that one could state a lemma using
match in the original goal. Thanks again! =)
Last updated: Aug 14 2022 at 11:02 UTC