The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

The standard way to define the append 
function in Coq is to use directly the fixpoint operator and not the
derived list_rec combinator :

Fixpoint app [X:Set;l:(list X)] : (list X)->(list X)
:= [m]Cases l of Nil => m
               | (Cons a l') => (Cons ? a (app X l' m))
   end.

The type of list_rec is :
 (X:Set; P:((list X)->Set))
        (P (Nil X))
        ->((x:X; l:(list X))(P l)->(P (Cons X x l)))
        ->(l:(list X))(P l)

In order to define app you should instantiate 
this scheme with P such that (P l)=(list X)
so takes P:=[l](list X)
the case (P (Nil X)) corresponds to the result (app (Nil X) m) which 
should be m 
the third argument explains how to compute 
    (app (Cons x l) m) [: (P (Cons x l))]
  from (app l m) [: (P l)]
so if applm represents (app l m) , the result should be 
(Cons x applm)

Finally the definition is :
        Definition app2 : (X:Set)(list X)->(list X)->(list X)
 := [X,l,m](list_rec X 
                     [l](list X) 
                     m
                     [x:X][l:(list X)][applm:(list X)](Cons ? x applm)
                     l).
It is possible to test these functions, for instance on lists of
        integers :

Require Arith.
Definition l1:=(Cons ? (1) (Cons ? (2) (Nil nat))).
Definition l2:=(Cons ? (3) (Cons ? (4) (Nil nat))).

Eval Compute in (app ? l1 l2).
Eval Compute in (app2 ? l1 l2).

I hope it answers your questions
Christine Paulin


HI!

My name is Joao
I'm a new member of the Coq Club.
I would like to know how to define new operations using the
recursive scheme _rec
I. e. If I have the next definition:
Coq < Inductive list [X:Set]:Set :=
Coq < Nil : (list X)
Coq < | Cons: X -> (list X) -> (list X).
list_ind is defined
list_rec is defined
list_rect is defined
list is defined

How I could define a function that concatenate two lists using
list_rec?

Thanks
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84