The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Edsko de Vries a écrit :
> 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? 
>   
As previous posters indicated, functional induction permits to do that 
by generating an induction principle derived from the function.

Alternatively, you could define foo and prove it has the expected 
property at the same time using dependently-typed programming. E.g, 
using the Program extension:

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

Obligations Tactic := idtac.

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

Obligations.

Solve Obligations using reflexivity.
>>

If you do not change the default obligations tactic to a dummy they are 
solved automatically.

Another way would be to define the induction principle by hand, keeping 
the original definition of foo. e.g:

<<
Require Import Coq.Program.Program.
Obligations Tactic := program_simpl.

Program Fixpoint L_ind' (P : L -> Prop)
 (pbase : P Base) (pbase2 : P (Ind Base)) (pind : forall l : L, P l -> 
P (Ind (Ind l))) (l : L) {struct l}: P l :=
 match l with
   | Base => pbase
   | Ind l' =>
     match l' with
       | Base => pbase2
       | Ind l'' => pind l'' (L_ind' P pbase pbase2 pind l'')
     end
 end.

Lemma foo_0 : forall l, foo l = 0.
Proof.
 induction l using L_ind' ; simpl ; trivial.
Qed.
>>

You can even get by without using Program or writting ugly terms in this 
case with:
<<
Fixpoint L_ind' (P : L -> Prop)
 (pbase : P Base)
 (pbase2 : P (Ind Base))
 (pind : forall l : L, P l -> P (Ind (Ind l))) (l : L) {struct l}: P l :=
 match l return P l with
   | Base => pbase
   | Ind Base => pbase2
   | Ind (Ind l') => pind l' (L_ind' P pbase pbase2 pind l')
 end.
>>

I'm not sure such an induction principle would be generaly useful in 
your case though...

Hope this helps,

--
Matthieu Sozeau
http://www.lri.fr/~sozeau