coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Prefixes of a vector
- Date: Tue, 19 Aug 2008 12:33:35 -0400
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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?
(*=======================================================================*)
Require Import Bvector.
Implicit Arguments Vcons [A n].
(*=======================================================================*)
Inductive Bounded : nat -> Set :=
| Zero : forall (n : nat), Bounded (S n)
| Succ : forall (n : nat), Bounded n -> Bounded (S n)
.
Implicit Arguments Succ [n].
(*=======================================================================*)
Fixpoint Bounded_to_nat (n : nat) (i : Bounded n) {struct i} : nat :=
match i with
| Zero _ => 0
| Succ n0 i0 => S (Bounded_to_nat n0 i0)
end
.
Implicit Arguments Bounded_to_nat [n].
(*=======================================================================*)
Definition prefix : forall (m : nat) (i : Bounded (S m)) (a : Type),
vector a m -> vector a (Bounded_to_nat i).
intro.
induction m as [| n].
(* Case m = 0 *)
remember 1 as One.
intros.
destruct i as [| p j].
(* Case i = Zero *)
simpl.
apply (Vnil a).
(* Case i = Succ j *)
assert (p = 0).
change p with (pred (S p)).
rewrite HeqOne.
simpl.
trivial.
revert j. rewrite H. intro.
inversion j.
(* Case m = S n *)
remember (S (S n)) as SSn.
intros.
destruct i as [| p j].
(* Case i = Zero *)
simpl.
apply (Vnil a).
(* Case i = Succ j *)
assert (p = (S n)).
change p with (pred (S p)).
rewrite HeqSSn.
simpl.
trivial.
revert j. rewrite H. intro.
simpl.
apply Vcons.
apply (Vhead a n X).
apply (IHn j).
apply (Vtail a n X).
Defined.
Implicit Arguments prefix [m a].
(*=======================================================================*)
Definition test_vec := Vcons 10 (Vcons 20 (Vcons 30 (Vnil nat))).
Eval compute in prefix (Zero 3) test_vec.
Eval compute in prefix (Succ (Zero 2)) test_vec.
Eval compute in prefix (Succ (Succ (Zero 1))) test_vec.
Eval compute in prefix (Succ (Succ (Succ (Zero 0)))) test_vec.
(*=======================================================================*)
- [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,
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.