induction exercise hint · Miscellaneous

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

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

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.

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

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! =)

Stream: Miscellaneous

Topic: induction exercise hint