The Coq mailing list

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

> On 15 Jul 2015, at 21:13, Beta Ziliani 
> <bziliani AT famaf.unc.edu.ar>
>  wrote:
> 
> 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?
Here is the script:

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

Print nT.
Set Printing All.
Print nT.
and the output (coq8.5beta2):

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

Argument scope is [nat_scope]
nT = 
fix nT (n : nat) : Type :=
  match n return Type with
  | O => unit
  | S n0 =>
      match n0 return Type with
      | O => forall _ : Type, Prop
      | S _ => prod (forall _ : Type, Prop) (nT n0)
      end
  end
     : forall _ : nat, Type

Argument scope is [nat_scope]




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