The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hey,

The Function/functional induction very nicely solved the problem. I was
wondering if there is a similar thing I can use in this minor variation:

Inductive L : Set :=
  | Base : L
  | Ind : L -> L.

Inductive Foo : L -> nat -> Prop :=
  | FooBase : Foo Base 0
  | FooIndBase : Foo (Ind Base) 0
  | FooIndInd : forall (l: L), Foo l 0 -> Foo (Ind (Ind l)) 0.

Theorem foo : forall (l:L), Foo l 0.

Again, normal proof by induction is no use:

Proof.
induction l.
apply FooBase.
induction l.
apply FooIndBase.
apply FooIndInd.
1 subgoal
l : L
IHl : Foo (Ind l) 0
IHl0 : Foo l 0 -> Foo (Ind l) 0
______________________________________(1/1)
Foo l 0

But when I do the recursion manually, the proof works:

Proof.
refine(fix f (l:L) : Foo l 0 := _).
elim l.
apply FooBase.
intros.
elim l0.
apply FooIndBase.
intros.
apply FooIndInd.
apply f.
Qed.

Of course I just use this style (using the refine to give me access to the
recursive calls to the proof), but it just seems to me there should be an
easier way.

Edsko