The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

Your code is working with 8.5beta2.
Set Printing All shows the code provided by James.

Print produces:
nT = 
fix nT (n : nat) : Type :=
  match n with
  | 0 => unit
  | 1 => Type -> Prop
  | S (S _ as n0) => ((Type -> Prop) * nT n0)%type
  end
     : nat -> Type

Best,

—
Frédéric





> On 15 Jul 2015, at 20:39, Beta Ziliani 
> <beta AT mpi-sws.org>
>  wrote:
> 
> 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}".
>