Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dependent pattern-matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dependent pattern-matching


Chronological Thread 
  • From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Dependent pattern-matching
  • Date: Sun, 4 Nov 2012 13:06:45 -0500

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



Archive powered by MHonArc 2.6.18.

Top of Page