The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

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