The Coq mailing list

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

A well-known reason for not having a predefined rich induction principle
is that several statements can be provided.
For example you can use List.fold_right, as follows:

Definition fold (P : box -> Prop) : list box -> Prop := 
  List.fold_right (fun (b : box) (Pl : Prop) => P b /\ Pl) True.

Then you get a similar induction principle with a quite readable definition:

Import List (* for list notation *).

Definition box_fold_ind
    (P : box -> Prop)
    (step : forall (n : nat) (l : list box), fold P l -> P (Cons n l)) :
    forall b : box, P b :=
  fix box_fold_ind (b : box) : P b :=
    let aux := fix aux (l : list box) : fold P l := 
      match l with 
        | nil => I
        | b :: l => conj (box_fold_ind b) (aux l)
      end in
    match b with
      | Cons b l => step b l (aux l)
    end.

You can design it in interactive mode as well, using fix, without any
issue about guardedness.

It is easy to show that box_fold_ind and box_rich_ind are equivalent
(the rewrite step is performed only there).

Hope it helps a little bit.
Jean-Francois



On Fri, Feb 22, 2013 at 01:47:20AM +0100, Pierre-Marie Pédrot wrote:
> On 21/02/2013 23:04, Nuno Gaspar wrote:
> >I believe the solution will be something similar to the one on decidable
> >equality shown on the link above...but how can I adapt it to my case?
> 
> You need to write out a nicer induction principle for your type, and
> this is a well-known problem (I think this is covered in the FAQ,
> and it keeps poping out every month on Coq-Club).
> 
> Basically, what you want to obtain is something that would look like:
> 
> Lemma box_rich_ind :
>   forall P : box -> Prop,
>   (forall n l, (forall b, List.In b l -> P b) -> P (Cons n l)) ->
>   forall b, P b.
> 
> Unluckily, I know of no easy way to handle this through Ltac for
> now, except using the infamous « Fix » tactic and its lot of
> guardedness hassle even if you're only doing very natural things
> such as rewrite. You've got to go the hard way to understand what's
> going on, writing the proof-term by hand. This is an exercise of its
> own, but for the sake of explanation, here it is:
> 
> Definition box_rich_ind :
>   forall P : box -> Prop,
>   (forall n l, (forall b, List.In b l -> P b) -> P (Cons n l)) ->
>   forall b, P b :=
> fix F P Hc b :=
> match b with
> | Cons n l =>
>   let aux : forall b, List.In b l -> P b :=
>     (fix G l b (H : List.In b l) {struct l} :=
>     match l return List.In b l -> P b with
>     | nil => False_rect _
>     | cons c l =>
>       fun H => match H with
>       | or_introl Heq =>
>         let H := F P Hc c in
>         match Heq in _ = d return P c -> P d with
>         | eq_refl => fun H => H
>         end H
>       | or_intror Hn => G l b Hn
>       end
>     end H) l in
>   Hc n l aux
> end.
> 
> It is only a richer version of the nested fixpoints definitions used
> here and there to handle that sort of inductive types. The problem
> here is that you want the full induction principle, which is quite
> contrived to recover (ugly dependent matches in the term as you can
> see).
> 
> Not sure this helps,
> PMP
> 
> 

-- 
Jean-Francois Monin
LIAMA Project FORMES, CNRS  &  Universite de Grenoble 1 &
Tsinghua University