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:

- Is there anything wrong with my
`induction`

tactic? - 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!

you probably shouldn't use eqn with induction

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

Removing it completes the proof without changing anything! :D

Jiahong Lee has marked this topic as resolved.

Last updated: Sep 30 2023 at 15:01 UTC