The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

I'm ashamed to ask this, I'm pretty sure this was answered somewhere.

I'm trying to do a (what I thought was a) simple dependent function type nT and function of that type fT. More concretely, nT generates types [unit, Type->Prop, (Type->Prop)*(Type->Prop), ...]:

Fixpoint nT n : Type :=
  match n with
  | 0  => unit
  | 1 => Type -> Prop
  | S n => ((Type -> Prop) * nT n)%type
  end.

When I try to define the function fT, it fails:

Fail Fixpoint fT n : nT n :=
  match n with
  | 0  => tt
  | 1 => (fun T:Type=>True)
  | S n' => ((fun T:Type=>True), fT n')
  end.

Failing with message:
Recursive call to fT has principal argument equal to
"S n0" instead of one of the following variables:
"n'" "n0".

Even if I try to help Coq a bit with annotations, or even breaking the cases, it's the same: it is not considering n = S n'. The only way I found to deal with this is using Program (avoiding it to perform the substitutions!):

Obligation Tactic := idtac.

Program Fixpoint fT n : nT n :=
  match n as m return n = m -> nT m with
  | 0  => fun _ => tt
  | S n' => fun H1 =>
    match n' return n = S n' -> nT (S n') with
    | 0 => fun _ =>(fun P:Type => True)
    | S n'' => fun H2 => ((fun P:Type => True), (_ (fT n') : nT (S n'')))
    end eq_refl
  end eq_refl.
Next Obligation.
 intros; rewrite H1 in H2.
 injection H2; intro H'.
 rewrite H' in x.
 exact x.
Defined.
Next Obligation.
 auto.
Defined.

which is horrible. Anyone knows of a better way to define this?

Thanks,

Beta

P.S.: A simpler version fails in a weird way:

Program Fixpoint fT n : nT n :=
  match n return nT n with
  | 0  => tt
  | S n' =>
    match n' as m return n' = m -> nT (S m) with
    | 0 => fun _ => ((fun T:Type=>True) : nT 1)
    | S n'' => fun H2 => _ ((fun T:Type=>True), fT n')
    end eq_refl
  end.
Next Obligation.
intros.
rewrite <- H2.
simpl.
rewrite H2.
rewrite <- H2.
exact x.
Fail Defined.


Error: Error: Illegal application:
       The term "@pair" of type
        "forall (A : Type@{Coq.Init.Datatypes.23})
           (B : Type@{Coq.Init.Datatypes.24}), A -> B -> A * B"
       cannot be applied to the terms
        "Type@{Top.1610} -> Prop" : "Type@{max(Set+1, Top.1610+1)}"
        "nT n'" : "Type@{Top.1319}"
        "fun _ : Type@{Top.1610} => True" : "Type@{Top.1610} -> Prop"
        "fT n'" : "nT n'"
       The 1st term has type "Type@{max(Set+1, Top.1610+1)}"
       which should be coercible to "Type@{Coq.Init.Datatypes.23}".