The Coq mailing list

[Edsko de Vries <edsko AT edsko.net>]

Hi,

Suppose we have a definition such as

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

Then when we do a proof by induction on L, for the 'Ind' case, the induction
principle derived by Coq tells me that the property holds for the sub-L.
However, what if we need to know that the property holds for a sub-sub-L? For
example, consider

Fixpoint foo (l: L) : nat := match l with
  | Base => 0
  | Ind l' => match l' with
    | Base => 0
    | Ind l'' => foo l''
    end
  end. 

Theorem foo_zero : forall (l:L), foo l = 0.

When I try to do a normal proof by induction, the induction hypothesis is no
use in the Ind Ind case:

Proof.
induction l.
reflexivity.
induction l.
reflexivity.
simpl.

1 subgoal
l : L
IHl : foo (Ind l) = 0
IHl0 : foo l = 0 -> foo (Ind l) = 0
______________________________________(1/1)
foo l = 0

At which point we're stuck (I think?). Now, up until recently the
'induction principle' was a bit of magic to me, until I realised that it
was simply a fold (in the functional programming sense), and that so it
must be possible to define these proofs directly. Indeed, I can prove
foo_zero as follows:

Proof.
refine (fix f (l:L) : foo l = 0 := _).
elim l.
reflexivity.
intros.
elim l0.
reflexivity.
intros.
simpl.
apply f.
Qed.

Although I'm quite happy I understood this, I would still like to be able to
use the proof style of the first attempt. Is it possible? 

Thanks!

Edsko