coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <devriese AT cs.tcd.ie>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] More dependent pattern matching
- Date: Mon, 9 Jun 2008 14:56:22 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I'm stuck again in trying to write some dependent code. I want to index a
vector:
Section vectors.
Variable (A : Set).
Inductive vec : nat -> Set :=
| vnil : vec 0
| vcons : forall n, A -> vec n -> vec (S n).
Inductive fin : nat -> Set :=
| finz : fin 1
| fins : forall n, fin n -> fin (S n).
Fixpoint vind n (i : fin n) {struct i} : vec n -> A :=
match i in fin n return vec n -> A with
| finz => fun v =>
match v in vec m return (match m with 0 => True | S _ => A end) with
| vnil => I
| vcons _ x _ => x
end
| fins m j => fun v =>
match v in vec m return (match m with 0 => True | S _ => A end) with
| vnil => I
| vcons m' _ xs => vind m j xs (* wrong *)
end
end.
Unfortunately, this code does not typecheck; the line marked as (* wrong *)
gives
Error:
In environment
A : Set
vind : forall n : nat, fin n -> vec n -> A
n : nat
i : fin n
m : nat
j : fin m
v : vec (S m)
m' : nat
a : A
xs : vec m'
The term "xs" has type "vec m'" while it is expected to have type "vec m"
It seems clear to me (but apparently not to the Coq typechecker) that m and m'
must be the same. Obviously, I can rewrite this code using inversion, but that
yields a large term which, moreover, includes an equality proof of m and m' --
which makes proofs more difficult because equality proofs are not transparent.
Is there another way?
Thanks,
Edsko
- [Coq-Club] More dependent pattern matching, Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching,
Adam Chlipala
- Re: [Coq-Club] More dependent pattern matching, Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching,
Conor McBride
- Re: [Coq-Club] More dependent pattern matching, Conor McBride
- Re: [Coq-Club] More dependent pattern matching,
Edsko de Vries
- Re: [Coq-Club] More dependent pattern matching, Conor McBride
- <Possible follow-ups>
- Re: [Coq-Club] More dependent pattern matching, rcp
- Re: [Coq-Club] More dependent pattern matching,
Adam Chlipala
Archive powered by MhonArc 2.6.16.