Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prefixes of a vector

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prefixes of a vector


chronological Thread 
  • 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))).





Archive powered by MhonArc 2.6.16.

Top of Page