Stream: Coq users

Topic: ✔ An Extra Condition in My Induction Hypothesis?

view this post on Zulip Jiahong Lee (Jun 08 2022 at 13:30):

Hi, I'm very new and self-learning Coq. While trying to proof this exercise, I'm confused why Coq adds an extra condition in front of my IHt2' and IHp1' induction hypotheses.

To illustrate:

(* Given *)
(* Datatype for representing a binary number. *)
Inductive bin : Type :=
  | BZ              (* zero *)
  | T2 (n : bin)    (* twice n *)
  | T2P1 (n : bin). (* twice n, plus one *)

Fixpoint incr (m:bin) : bin :=
  match m with
  | BZ      => T2P1 BZ
  | T2 m'   => T2P1 m'
  | T2P1 m' => T2 (incr m')
  end.

Fixpoint bin_to_nat (m:bin) : nat :=
  match m with
  | BZ      => O
  | T2   m' => 2 * bin_to_nat m'
  | T2P1 m' => 1 + 2 * bin_to_nat m'
  end.

(* To prove this: *)
(* Theorem: Incrementing a binary number and then converting it to
    a natural number yields the same result as first converting
    it to a natural number and then incrementing.
*)
Theorem bin_to_nat_pres_incr : forall b : bin,
    bin_to_nat (incr b) = S (bin_to_nat b).
Proof.
  (* By induction on b. *)
  induction b as [| t2' IHt2' | t2p1' IHp1'] eqn:Eb.
  - (* b = BZ *)
    simpl incr. simpl bin_to_nat. reflexivity.
  - (* b = T2 t2' *)
    simpl incr. simpl bin_to_nat. reflexivity.
    (* ^----   [1] Check out IHt2'. *)

At [1] (end of the code snippet above), there is an extra b = t2' in my IHt2'. Here is a snapshot of my *goals*:

1 goal (ID 26)

- b, t2' : bin
- Eb : b = T2 t2'
- IHt2' : b = t2' -> bin_to_nat (incr t2') = S (bin_to_nat t2') (* <==== HERE *)
  ============================
  bin_to_nat (incr (T2 t2')) = S (bin_to_nat (T2 t2'))

I would expect it to be IHt2': bin_to_nat (incr t2') = S (bin_to_nat t2') from my previous experience of doing induction with natural numbers.

Questions:

  1. Is there anything wrong with my induction tactic?
  2. If so, how to get rid of the extra condition in my induction hypotheses? If not, how can I prove the third case when b = T2P1 t2pl'? My proof is almost completed but stuck at proving the extra condition. Full code until where I stuck:

Thanks!

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 13:34):

you probably shouldn't use eqn with induction

view this post on Zulip Jiahong Lee (Jun 08 2022 at 13:40):

Thanks! Didn't realise that was the issue. :dizzy:

Removing it completes the proof without changing anything! :D

view this post on Zulip Notification Bot (Jun 08 2022 at 13:40):

Jiahong Lee has marked this topic as resolved.

Last updated: Sep 30 2023 at 15:01 UTC