## Stream: Miscellaneous

### Topic: induction exercise hint

#### Thales MG (May 17 2021 at 20:08):

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`? =)

#### Laurent Théry (May 17 2021 at 20:37):

your first definition of `normalize` looks good to me. Can you be more precise what problems you have in the proofs with it?

#### Thales MG (May 17 2021 at 21:09):

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?! *)
``````

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

#### Laurent Théry (May 17 2021 at 21:32):

for `normalize_normalize` you just need to simplify `IHb` (`simpl in IHb`)

#### Thales MG (May 17 2021 at 23:44):

@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?

#### Thales MG (May 18 2021 at 00:10):

(BTW, indeed it seems that `simpl in` was the missing piece. With that, I managed to finally finish the exercise.)

#### Laurent Théry (May 18 2021 at 00:14):

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`

#### Thales MG (May 18 2021 at 10:10):

Nice! Another thing I didn't realize: that one could state a lemma using `match` in the original goal. Thanks again! =)

Last updated: Dec 07 2023 at 09:01 UTC