The Coq mailing list

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

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?
>