The Coq mailing list

[Chantal KELLER <chantal.keller AT wanadoo.fr>]

Hi Florian,

In list_prod', F0 does not need to be mutually recursive with F. You can
define it as follows:


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 =>

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

        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.


Chantal.




Florian Hatat a écrit :
> 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,

-- 
Chantal KELLER
chantal.keller AT wanadoo.fr