The Coq mailing list

[Guillaume Brunerie <guillaume.brunerie AT gmail.com>]

Hi,

(this question is probably easy, I think I’m missing something)

I want to define recursively a dependent type [T] and a function [f] such that

T : nat -> Type

f : forall n : nat, A n -> T n (* [A : nat -> Type] has been defined earlier *)

I have [T (S n)] depending on [f n] and [T n], and [f (S n)] also depending on [f n] and [T n] (and [T (S n)] because it’s in the type of [f (S n)]).

I naively tried the following:

Fixpoint T (n : nat) : Type :=

  […]

with f (n : nat) : A n -> T n :=

  […].

 

But this didn’t work because [T] does not exists yet and Coq wants to type [f] before adding [T] to the environment.

I also tried defining [T] and [f] as one function:

Fixpoint Tf (n : nat) : {B : Type & A n -> B} :=

  match n with

    | 0 => […]

    | S n' => […]

  end.

This didn’t work either, I think this is because in the first branch of the match Coq want a function of type [A n -> B] but I just have something of type [A 0 -> B] (and there is the same problem in the second branch, is this what is called dependent pattern matching?)

Could you help me define [T] and [f]?

Thanks,

Guillaume Brunerie