The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

The example was not very motivated actually. I was trying to solve an exercise, came up with a solution and wondered if I could solve it in any other way. After some attempts, I hit that weird error and wanted to know what it meant.

On Wed, Oct 31, 2012 at 7:53 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

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.
   

--
Arthur Azevedo de Amorim