David's proposal:

The challenge is about functions in Coq with a variable number of  
arguments.  Yes, it is possible!

1) Write a function which takes as a first argument a positive  
integer n and then n arguments, and returns the sum of those n  
arguments.  Here are examples of application:

Coq < Eval simpl in add 5 14 11 4 1 5.
      = 35

Coq < Eval simpl in add 3 5 10 11.
      = 26

Coq < Eval simpl in add 0.
      = 0

You must NOT use the features of Coq to change its syntax.  The  
expressive power of the Coq type system is more than enough for  
writing this function.

2) The most daring of you (Nicolas ?) can do better and write a fold  
function which allows to define generically functions such as the  
above one.  Here are some examples:

Coq < Eval simpl in fold 0 plus 5 14 11 4 1 5.
      = 35

Coq < Eval simpl in fold True (fun P n => n>0 /\ P) 3 7 0 6.
      = 7 > 0 /\ 0 > 0 /\ 6 > 0 /\ True

Coq < Eval simpl in fold False (fun P Q => Q \/ P) 3 (1=0) True  
(forall A:Prop, A->A).
      = 1 = 0 \/ True \/ (forall A : Prop, A -> A) \/ False

--

Nicolas' answer:

Require Import List.
Require Import Arith.

(* First challenge *)

Fixpoint type_nat (n:nat) {struct n} : Set :=
  match n with
    | 0 => nat
    | S n' => nat -> (type_nat n')
  end.

Definition add_nat (n: nat) (a: nat) (sum: type_nat n) : type_nat (n).
  induction n.
  intros.
  simpl in sum.
  simpl.
  exact (plus a sum).
  simpl; intros.
  exact (IHn a (sum H)).
Defined.

(*

Fixpoint add_nat  (n: nat) (a: nat) (sum: type_nat n) : type_nat (n) :=
 match n with
  | 0 => plus sum a
  | S n' => fun s => add_nat n' a (sum s)
 end.

*)

Definition add (n: nat) : type_nat n.
  induction n.
  exact 0.
  simpl.
  intro s.
  exact (add_nat n s IHn).
Defined.


(*

Fixpoint add  (n: nat): type_nat n :=
 match n with
  | 0 => 0
  | S n' => fun s => add_nat n' s (add n')
 end.

*)


Eval simpl in add 5 14 11 4 1 5.
  
Eval simpl in add 3 5 10 11.

Eval simpl in add 0. 


(* Second challenge *)

Fixpoint type (n: nat) (A: Type) (B: Type) {struct n} : Type :=
  match n with
    | 0 => A
    | S n' => B -> (type n' A B)
  end.


Definition fold'' (n: nat) (A B: Type) (b: B) (f: A -> B -> A) (sum: type n A B) : type n A B.
  induction n.
  intros.
  simpl in sum.
  simpl.
  exact (f sum b).
  simpl; intros.
  eapply IHn.
  eapply b.
  apply f.
  eapply sum.
  apply X.
Defined.

Definition fold' (n: nat) (A B: Type) (f: A -> B -> A) (default: A): type n A B.
  induction n.
  simpl; intros.
  apply default.
  simpl; intros.
  eapply fold''.
  apply X.
  apply f.
  eapply IHn.
  apply f.
  apply default.
Defined.

Definition fold (A B: Type) (default: A) (f: A -> B -> A) (n: nat) : type n A B :=
  fold' n A B f default.

Implicit Arguments fold.

Eval simpl in fold 0 plus 5 14 11 4 1 5. 

Eval simpl in fold True (fun P n => n>0 /\ P) 3 7 0 6. 

Eval simpl in fold False (fun P Q => Q \/ P) 3 (1=0) True  (forall A:Prop, A->A).

--

David's solution:

 Set Implicit Arguments.

Section Fold.

Variables A B : Type.

Variable a : A.

Variable f : A->B->A.

Fixpoint T (n:nat) : Type :=
   match n with
     O => A
   |(S n') => B->(T n')
   end.

Fixpoint fold' (n:nat)(y:B) : T n -> T n :=
   match n return (T n -> T n) with
     0 => fun x => f x y
   | S n' => fun g y' => fold' n' y (g y')
   end.

Fixpoint fold (n:nat) : T n :=
   match n return (T n) with
     0 => a
   | S n' => fun x => fold' n' x (fold n')
   end.

End Fold.

Definition add :=
   fold 0 plus.

Eval simpl in add 5 14 11 4 1 5.

Eval simpl in fold 0 plus 5 14 11 4 1 5.

Eval simpl in fold False (fun P Q => Q \/ P) 3 (1=0) False (forall  
A:Prop, A->A).

Eval simpl in fold True (fun P n => n>0 /\ P) 3 7 3 6.