coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT hcoop.net>
- To: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Prefixes of a vector
- Date: Tue, 19 Aug 2008 12:53:18 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Samuel E. Moelius III wrote:
For some time, I have been trying to write this function.
Definition prefix : forall (m : nat) (i : Bounded (S m))
(a : Type), vector a m -> vector a (Bounded_to_nat i).
The intuition is: the argument i picks out one of the (m + 1)
possible prefixes of a vector of length m.
Recently, I blundered my way into what appears below. My question
(which is subjective) is: is there a simpler way to write this
function?
I recommend never using the vector type family from the Coq standard library. That kind of type family works out much better as a recursive definition than as an inductive definition in Coq. Here's the way I would do it:
Section vector.
Variable T : Type.
Fixpoint vector (n : nat) : Type :=
match n with
| O => unit
| S n' => T * vector n'
end%type.
Fixpoint index (n : nat) : Type :=
match n with
| O => Empty_set
| S n' => option (index n')
end.
Fixpoint indexToNat (n : nat) : index n -> nat :=
match n return (index n -> nat) with
| O => fun emp => match emp with end
| S n' => fun idx =>
match idx with
| None => O
| Some idx' => S (indexToNat n' idx')
end
end.
Fixpoint prefix (n : nat) {struct n} : vector n -> forall idx : index (S n), vector (indexToNat (S n) idx) :=
match n return (vector n -> forall idx : index (S n), vector (indexToNat (S n) idx)) with
| O => fun _ idx =>
match idx return (vector (indexToNat 1 idx)) with
| None => tt
| Some emp => match emp with end
end
| S n' => fun vec idx =>
match idx return (vector (indexToNat (S (S n')) idx)) with
| None => tt
| Some idx' => (fst vec, prefix n' (snd vec) idx')
end
end.
End vector.
Definition test_vec : vector nat 3 := (10, (20, (30, tt))).
Eval compute in prefix _ _ test_vec None.
Eval compute in prefix _ _ test_vec (Some None).
Eval compute in prefix _ _ test_vec (Some (Some None)).
Eval compute in prefix _ _ test_vec (Some (Some (Some None))).
- [Coq-Club] Prefixes of a vector, Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector,
Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector, Pierre Casteran
- Re: [Coq-Club] Prefixes of a vector,
Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector,
Venanzio Capretta
- Re: [Coq-Club] Prefixes of a vector,
Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector,
Venanzio Capretta
- Re: [Coq-Club] Prefixes of a vector,
Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector,
Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector,
Samuel E. Moelius III
- Re: [Coq-Club] Prefixes of a vector,
Conor McBride
- Re: [Coq-Club] Prefixes of a vector, Matthieu Sozeau
- Re: [Coq-Club] Prefixes of a vector,
Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector,
Venanzio Capretta
- Re: [Coq-Club] Prefixes of a vector,
Adam Chlipala
- Re: [Coq-Club] Prefixes of a vector, Adam Chlipala
Archive powered by MhonArc 2.6.16.