The Coq mailing list

[Florian Hatat <florian.hatat AT univ-savoie.fr>]

Dear all,

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

Variable A : Type.
Variable B : Type.

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.


Could I get something similar to this "list_prod" principle, but for
regular lists/pairs of Coq (i.e., which are not mutually inductive)?

Simply replacing "list'" with "list (A * B)" and "prod'" with "A * B" in
the term "list_prod" doesn't work, Coq complains that the recursive call
to F0 is ill-formed. Here is the term, if you want to try:

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
      :=
      fun P P0 f f0 f1 =>

        fix F (l : list (A * B)) : P l :=
        match l as l0 return (P l0) with
          | nil => f
          | cons p l0 => f0 p (F0 p) l0 (F l0)
        end

        with F0 (p : A * B) : P0 p :=
        match p as p0 return (P0 p0) with
          | (t, t0) => f1 t t0
        end

        for F.


Thank you for your help,
-- 
Florian Hatat,
http://www.lama.univ-savoie.fr/~hatat/