The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   Dear Florian,

If I define by hand a type list' (which mimics list (A * B)), I can get
an induction principle "list_prod" : 

[...]
Inductive list' : Type :=
| nil' : list'
| cons' : prod' -> list' -> list'

with prod' : Type :=
| pair' : A -> B -> prod'.

Scheme list_prod := Induction for list' Sort Type
with prod_list := Induction for prod' Sort Type.

  First of all I do not understand why do you insist on using mutually inductive definitions here (prod does not depend on list).

Definition list_prod' :
 forall (P : list (A * B) -> Type) (P0 : (A * B) -> Type),
   P nil ->
   (forall p : A * B, P0 p ->
     forall l : list (A * B), P l -> P (cons p l)) ->
   (forall (t : A) (t0 : B), P0 (t, t0)) ->
   forall l : list (A * B), P l
     := [...]

  Note that this induction principle follows simply from the general induction principle on lists by taking 'Q' as 'always true'. Hence if for whatever reason you want an induction principle of exactly this shape you can easily prove if for standard list/prod types with:

Require Import List.
Lemma list_prod_ind : forall (P : list (A * B) -> Type) (Q : A * B -> Type),

  P nil ->
  (forall p, Q p -> forall l, P l -> P (cons p l)) ->

  (forall a b, Q (a, b)) ->
  forall l, P l.

Proof.
  intros P Q P0 P1 Q0 l. induction l. assumption.

  apply P1. destruct a. apply Q0. assumption.
Qed.

  Cheers,

   Adam
-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================