The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sun, 4 Nov 2012 13:05:09 -0500,
Arthur Azevedo de Amorim 
<arthur.aa AT gmail.com>
 a écrit :

> Thanks a lot Cédric. Is there any reason why Coq would infer one
> annotation for one match and not for the other?

anotations are infered for both match. Just that there are two
incompatible anotations performed.

I did not tried it, but replacing "Inductive fin : nat -> Set :=…" with
"Inductive fin : nat -> Type := …" may also work. In general, you
should use "Type" everywhere, so you do not end with such kind of
errors as often. "Type" is "less efficient" than "Set", because it
implies to build type universes, whereas Set does not, but the
gain in performance is most of the time neglictable.

That said, I am not sure why "match … return Set with …" is not allowed
where a "match … return Type with …" is expected.

> 
> 
> On Wed, Oct 31, 2012 at 4:13 AM, AUGER Cédric 
> <sedrikov AT gmail.com>
> wrote:
> 
> > Le Wed, 31 Oct 2012 03:04:06 -0400,
> > Arthur Azevedo de Amorim 
> > <arthur.aa AT gmail.com>
> >  a écrit :
> >
> > > Dear list,
> > >
> > > Suppose that we have the following definition of bounded nats:
> > >
> > >   Inductive fin : nat -> Set :=
> > >   | First : forall n, fin (S n)
> > >   | Next : forall n, fin n -> fin (S n).
> > >
> > > Then, I try to define a function fminus : forall n, fin (S n) ->
> > > nat in the following way (this is *not* supposed to be a nice
> > > definition)
> > >
> > > Fixpoint fminus' n (fn : fin (S n)) : nat :=
> > >   match n return fin (S n) -> nat with
> > >     | O => fun fn => O
> > >     | S n' => fun fn =>
> > >       match fn in fin n'' return
> > >         match n'' with
> > >           | O => unit
> > >           | S O => unit
> > >           | S _ => nat
> > >         end with
> > >         | First n''' =>
> > >           match n''' return
> > >             match n''' with
> > >               | O => unit
> > >               | S _ => nat
> > >             end with
> > >             | O => tt
> > >             | S _ => n
> > >           end
> > >         | Next n''' fn' =>
> > >           match n''' return fin n''' ->
> > >             match n''' with
> > >               | O => unit
> > >               | S _ => nat
> > >             end with
> > >             | O => fun _ => tt
> > >             | S _ => fun fn' => fminus fn'
> > >           end fn'
> > >       end
> > >   end fn.
> > >
> > > Coq complains, saying
> > >
> > > Error: In pattern-matching on term "fn0" the branch for
> > > constructor "Next" has type
> > >  "forall n''' : nat, fin n''' -> match n''' with
> > >                                  | 0 => unit
> > >                                  | S _ => nat
> > >                                  end" which should be
> > >  "forall n : nat, fin n -> match n with
> > >                            | 0 => unit
> > >                            | S _ => nat
> > >                            end".
> > >
> > > However, this very similar term (that doesn't do the same thing,
> > > though) does typecheck:
> >
> > You did not tried this term in this context.
> > "fminus" is not defined, and "fminus'" is not used inside your
> > fixpoint. And you didn't mistyped "fminus" instead of "fminus'"
> > since by correcting it this way, you get an obvious type checking
> > error (which is not related to dependent types).
> >
> >
> > I corrected it as:
> >
> > »             | S k => fun fn' => fminus' k fn'
> >
> > which seems to give your error back.
> >
> > Then activating display of all low level contents, I get:
> >
> > Error: In pattern-matching on term "fn0" the branch for constructor
> > "Next" has type "forall (n''' : nat) (_ : fin n'''),
> >   match n''' return Set with
> >   | O => unit
> >   | S _ => nat
> >   end" which should be
> >  "forall (n : nat) (_ : fin n),
> >   match n return Type (* Top.68 *) with
> >   | O => unit
> >   | S _ => nat
> >   end".
> >
> > »         | Next n''' fn' =>
> > »           match n''' return fin n''' ->
> > »             match n''' with
> > »               | O => unit
> > »               | S _ => nat
> > »             end : Type (*yes I know, that seems weird*) with
> > »             | O => fun _ => tt
> >
> > works.
> >
> > When you have an "<x> has type <y> while it should be <y>" error,
> > display all. Some important type information may be omitted by
> > implicit arguments or similar stuff.
> >
> > >
> > > Fixpoint fminus' n (fn : fin (S n)) : nat :=
> > >   match n return fin (S n) -> nat with
> > >     | O => fun fn => O
> > >     | S n' => fun fn =>
> > >       match fn in fin n'' return
> > >         match n'' with
> > >           | O => unit
> > >           | S O => unit
> > >           | S _ => nat
> > >         end with
> > >         | First n''' =>
> > >           match n''' return
> > >             match n''' with
> > >               | O => unit
> > >               | S _ => nat
> > >             end with
> > >             | O => tt
> > >             | S _ => n
> > >           end
> > >         | Next n''' fn' =>
> > >           match n''' return
> > >             match n''' with
> > >               | O => unit
> > >               | S _ => nat
> > >             end with
> > >             | O => tt
> > >             | S _ => n
> > >           end
> > >       end
> > >   end fn.
> > >
> > > (Notice that in the Next branch we are not abstracting over fin
> > > n''' anymore).
> > >
> > > Any thoughts on why this doesn't work?
> > >
> >
> >
> 
>