coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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: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?
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.
Arthur Azevedo de Amorim
- Re: [Coq-Club] Dependent pattern-matching, Arthur Azevedo de Amorim, 11/04/2012
- Re: [Coq-Club] Dependent pattern-matching, AUGER Cédric, 11/04/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Dependent pattern-matching, Arthur Azevedo de Amorim, 11/04/2012
Archive powered by MHonArc 2.6.18.