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: Oct 12 2024 at 11:01 UTC