The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

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.

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