The Coq mailing list

[Beta Ziliani <bziliani AT famaf.unc.edu.ar>]

Hi Frédéric,

On Wed, Jul 15, 2015 at 4:08 PM, Frédéric Besson <frederic.besson AT inria.fr> wrote:

Hi,

Your code is working with 8.5beta2.

Must be something new, I'm using 8.5 commit 851539eca5016da98253308749131abae3ec7b93 (June 5).

 

Set Printing All shows the code provided by James.

Uh? This is an answer to what?

 

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}".
>