Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Prefixes of a vector


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

(*=======================================================================*)





Archive powered by MhonArc 2.6.16.

Top of Page