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
IHp1' induction hypotheses.
(* 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. (* ^----  Check out IHt2'. *)
At  (end of the code snippet above), there is an extra
b = t2' in my
IHt2'. Here is a snapshot of my
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.
b = T2P1 t2pl'? My proof is almost completed but stuck at proving the extra condition. Full code until where I stuck:
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