The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

See Section 3.8 of CPDT <http://adam.chlipala.net/cpdt/>.

On 12/18/2012 05:25 PM, Kenneth Roe wrote:

Below is a simple theorem I would like to prove with induction.  I have copied code up to the point where I would like to where I would like to use an inductive hypothesis.  However, Coq does not give me an inductive hypothesis.  What do I need to do to get things working?

                 - Ken

Inductive Test : Type :=
  | Leaf : nat -> Test
  | Nodes : list Test -> Test.

Fixpoint same x := match x with
                   | Leaf x => Leaf x
                   | Nodes l => Nodes (map same l)
                   end.

Theorem ss : forall x, same x = x.
Proof.
    induction x.
    unfold same. reflexivity.