Hello!
I'm working my way through the Logic Foundations on my own, and I got stumped in part c
of binary_inverse
.
I came up with the following definition for normalize
:
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 Z
.
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 normalize
? =)
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.
for normalize_normalize
you just need to simplify IHb
(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 rewrite normalizeB0
Nice! Another thing I didn't realize: that one could state a lemma using match
in the original goal. Thanks again! =)
Last updated: Jun 01 2023 at 11:01 UTC