## Stream: Coq users

### Topic: ✔ An Extra Condition in My Induction Hypothesis?

#### 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!

#### Gaëtan Gilbert (Jun 08 2022 at 13:34):

you probably shouldn't use eqn with induction

#### 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

#### 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