The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/31/2012 03:04 AM, Arthur Azevedo de Amorim wrote:
> 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)
>    

Now I'm curious, though it looks like someone solved your concrete 
problem: why do you want to write a function like this, or like whatever 
is the real inspiration for the example?

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