The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT cnam.fr>]

Hi,

Indeed standard induction scheme are relatively weak compared to more
general ones like well founded induction (see theories/Wellfounded/*.v). 
However they are easier to use. I suggest you use the new "Function"
feature instead of Fixpoint. It gives you among other things a useful
(but still in the style of L_ind) induction scheme from the function
definition.


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

Function foo (l: L) : nat := match l with
  | Base => 0
  | Ind l' => match l' with
    | Base => 0
    | Ind l'' => foo l''
    end
  end. 
(* See the message for a list of things defined here. For example Check 
foo_ind *)

Theorem foo_zero : forall (l:L), foo l = 0.
Proof.
  intros l.
  functional induction (foo l). (* this makes actually use of foo_ind, 
automatically built by Function *)
  reflexivity.
  reflexivity.
  assumption.
Qed.
  


Le Thu, 11 Oct 2007 15:25:34 +0100, Edsko de Vries 
<edsko AT edsko.net>
 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? 
> 
> 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