The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 18 Dec 2012 14:25:11 -0800,
Kenneth Roe 
<kendroe AT hotmail.com>
 a écrit :

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

I think I will get bored to reply to this question ^^.

That is not your fault, just that this question comes rather often in
the mailing list. Maybe it should be added in a FAQ or something alike.

There are many solutions.

An "unsafe one" is to replace "Theorem" with "Fixpoint".
It is sound, but guardedness will be checked at Qed. time (or at
Guarded. time if you use it). Beware Fixpoint (as well as the "fix"
tactic) easily breaks guardedness. So when using a fixpoint, quickly
destruct the recursive argument and generalize applications of the
fixpoint with structurally smaller arguments, then clear the fixpoint.

A safer solution is to define your own induction principle.

An other solution is to user "Induction Scheme" (or something like
that) which automatize a little generation of induction principle.

All these solutions do not modify your inductive type, but there is
also an alternative solution (which I often prefer):

Inductive Test : Type :=
   | Leaf : nat -> Test
   | Nodes : listTest -> Test
with listTest : Type :=
   | NilTest : listTest
   | ConsTest : Test -> listTest -> listTest.
 
Fixpoint same x := match x with
                   | Leaf x => Leaf x
                   | Nodes l => Nodes (mapsame l)
                   end
with mapsame l := match l with
                  | NilTest => NilTest
                  | ConsTest x l => ConsTest (same x) (mapsame l)
                  end.

Theorem ss : forall x, same x = x
with ssl : forall l, mapsame l = l.
Proof.
...
Proof.
...
Qed.

Note that it has the same behaviour as Fixpoint, so you need extra care
not to break guardedness. Note also that this way, you should not use
the induction tactic, but simply "case" or "destruct" on the recursive
argument.

I also encourage you to take a look at the documentation.