The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

Would this do the job?
Best,
Damien


Inductive L :=
| nil: Type -> L
| cons: forall A, (A -> L) -> L.

Fixpoint F (l: L) :=
  match l with
    | nil A => A
    | cons A f => forall a, F (f a)
  end.

Definition l := cons nat (fun a => cons nat (fun b => nil (a=b))).
Compute F l.



Le 17 avril 2012 10:06, Paolo Herms 
<paolo.herms AT cea.fr>
 a écrit :
> Thank you for your answer.
> However, my problem is more complex.
> In your example the number of arguments (inductive datatype nat) provides
> enough information to define the type of a function with a variable number 
> of
> arguments, as every argument has the the same type:
>
> Fixpoint T A B (n:nat) : Type :=
>  match n with
>    | O => A
>    | S n' => B -> T A B n'
>  end.
>
> T A B 3 = B -> B -> B -> A
>
> We can even generalise this to functions with a variable number of arguments
> with different but non-dependent types, using the inductive datatype list:
>
> Fixpoint T A (L : list Type) : Type :=
>  match L with
>    | nil => A
>    | B::L' => B -> T A L'
>  end%list.
>
> T D [A;B;C] = A -> B -> C -> D
>
> Now, I can't think of an inductive datatype that represents a list of
> dependent products I'd need to construct a type like
> forall (a:A) (b: B a) (c: C a b), (D a b c)
>
> Any ideas?
> --
> Paolo Herms
> PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
> Paris, France
>
>
> On Tuesday 17 April 2012 11:34:09 Sylvain Heraud wrote:
>> You can look at this exercice:
>>
>> http://staff.aist.go.jp/reynald.affeldt/coqcafe/ccc1.txt
>>
>> But you have to put the number of argument in f ! (f 1 a) (f 2 a b) (f 3 a
>> b c) ...
>>
>> Sylvain
>>
>> On Tue, Apr 17, 2012 at 10:09, Paolo Herms 
>>Â <paolo.herms AT cea.fr>
>>  wrote:
>> > Hello,
>> > any ideas of how to generalise this sequence, ie. define Tn?
>> >
>> > Definition T0
>> >
>> >  (A: Type)
>> >  (f: option (A))
>> >
>> >  :=
>> >
>> >  { x : (A) | f  = Some x }.
>> >
>> > Definition T1
>> >
>> >  (A: Type)
>> >  (B: forall (a:A), Type)
>> >  (f: forall (a:A), option (B a))
>> >  (a:A) :=
>> >  { x : (B a) | f a  = Some x }.
>> >
>> > Definition T2
>> >
>> >  (A: Type)
>> >  (B: forall (a:A), Type)
>> >  (C: forall (a:A) (b: B a), Type)
>> >  (f: forall (a:A) (b: B a), option (C a b))
>> >  (a:A) (b: B a) :=
>> >  { x : (C a b) | f a b  = Some x }.
>> >
>> > Definition T3
>> >
>> >  (A: Type)
>> >  (B: forall (a:A), Type)
>> >  (C: forall (a:A) (b: B a), Type)
>> >  (D: forall (a:A) (b: B a) (c: C a b), Type)
>> >  (f: forall (a:A) (b: B a) (c: C a b), option (D a b c))
>> >  (a:A) (b: B a) (c: C a b) :=
>> >  { x : (D a b c) | f a b c  = Some x }.
>> >
>> > Thanks in advance,
>> > --
>> > Paolo Herms
>> > PhD Student - CEA Software Safety Lab. / Inria ProVal project-team
>> > Paris, France