coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Dependent pattern-matching
- Date: Wed, 31 Oct 2012 03:04:06 -0400
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:
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?
--
Arthur Azevedo de Amorim
- [Coq-Club] Dependent pattern-matching, Arthur Azevedo de Amorim, 10/31/2012
- Re: [Coq-Club] Dependent pattern-matching, AUGER Cédric, 10/31/2012
- Re: [Coq-Club] Dependent pattern-matching, Adam Chlipala, 10/31/2012
Archive powered by MHonArc 2.6.18.