The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Yes you can use use the proof style of the first attempt.
Just state a slightly stronger lemma.

Theorem bar_zero : forall (l:L), foo l = 0 /\ foo (Ind l) = 0.
induction l; info intuition.  
Qed.

Theorem foo_zero : forall (l:L), foo l = 0.
intro l; generalize (bar_zero l); info intuition.
Qed.

Jean-Francois

On Thu, Oct 11, 2007 at 03:25:34PM +0100, Edsko de Vries wrote:
> 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
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46