Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dependent pattern-matching


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page