# Library CoLoR.Util.Vector.VecUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-02
• Frederic Blanqui, 2005-01-27 and later
• Adam Koprowski and Hans Zantema, 2007-03-26
• Joerg Endrullis, 2008-06-19
• Pierre-Yves Strub, 2009-04-09
• Wang Qian & Zhang Lianyi, 2009-05-06

# Extension of the Coq library Vector

Set Implicit Arguments.

Notation vector := Vector.t.
Notation Vnil := Vector.nil.
Notation Vcons := Vector.cons.
Notation Vhead := Vector.hd.
Notation Vtail := Vector.tl.
Notation Vconst := Vector.const.

Notations for vectors.

Module VectorNotations.
Notation " [ ] " := Vnil : vector_scope.
Notation " [ x ] " := (Vcons x Vnil) : vector_scope.
Notation " [ x ; .. ; y ] " := (Vcons x .. (Vcons y Vnil) ..)
: vector_scope.
End VectorNotations.

Tactic for destructuring equalities on vectors.

Ltac Veqtac := repeat
match goal with
| H : Vcons ?x ?v = Vcons ?x ?w |- _ =>
let h := fresh in
(injection H; intro h; ded (inj_existT eq_nat_dec h);
clear h; clear H)
| H : Vcons ?x ?v = Vcons ?y ?w |- _ =>
let h1 := fresh in let h2 := fresh in
(injection H; intros h1 h2; ded (inj_existT eq_nat_dec h1);
clear h1; clear H)
end.

## Elementary identities.

Section Velementary.

Variable A : Type. Notation vec := (vector A).

Definition Vid n : vector A n -> vector A n :=
match n with
| O => fun _ => Vnil
| _ => fun v => Vcons (Vhead v) (Vtail v)
end.

Lemma Vid_eq : forall n (v : vector A n), v = Vid v.

Lemma VSn_eq : forall n (v : vector A (S n)), v = Vcons (Vhead v) (Vtail v).

Definition Vhead_tail n (v : vector A (S n)) := (Vhead v, Vtail v).

Lemma Vcons_eq_intro : forall a1 a2 n (v1 v2 : vector A n),
a1 = a2 -> v1 = v2 -> Vcons a1 v1 = Vcons a2 v2.

Lemma Vcons_eq_elim : forall a1 a2 n (v1 v2 : vector A n),
Vcons a1 v1 = Vcons a2 v2 -> a1 = a2 /\ v1 = v2.

Lemma Vcons_eq : forall a1 a2 n (v1 v2 : vector A n),
Vcons a1 v1 = Vcons a2 v2 <-> a1 = a2 /\ v1 = v2.

Lemma Vtail_eq : forall a n (v1 v2 : vector A n),
v1 = v2 -> Vcons a v1 = Vcons a v2.

End Velementary.

Tactic for destructing non empty vectors.

Ltac VSntac y := let h := fresh in gen (VSn_eq y); intro h; try rewrite h.

## First element of a vector with default value if empty.

Definition Vfirst A default n (v : vector A n) : A :=
match v with
| Vnil => default
| Vcons x _ => x
end.

## Type casting function on vectors.

Section Vcast.

Variable A : Type.

Definition Vcast m (v : vector A m) n (mn : m = n) : vector A n :=
match mn in _ = p return vector A p with
| eq_refl => v
end.

Lemma Vcast_cons n (v : vector A n) x p (hS : S n = S p) :
Vcast (Vcons x v) hS = Vcons x (Vcast v (eq_add_S hS)).

Lemma Vcast_refl n (v : vector A n) : forall H : n=n, Vcast v H = v.

Lemma Vcast_eq_elim : forall n (v1 v2 : vector A n) m (h : n = m),
Vcast v1 h = Vcast v2 h -> v1 = v2.

Lemma Vcast_cast_eq :
forall n (v : vector A n) m (h1 : n=m) p (h2 : m=p) (h3 : n=p),
Vcast (Vcast v h1) h2 = Vcast v h3.

Lemma Vcast_cast : forall n (v : vector A n) m (h1 : n=m) p (h2 : m=p),
Vcast (Vcast v h1) h2 = Vcast v (trans_eq h1 h2).

Lemma Vcast_eq_intror : forall n1 (v1 : vector A n1) n0 (h1 : n1=n0)
n2 (v2 : vector A n2) (h2 : n2=n0) (h : n1=n2),
Vcast v1 h = v2 -> Vcast v1 h1 = Vcast v2 h2.

Lemma Vcast_eq_intro : forall n (v1 v2 : vector A n) p (e : n=p),
v1 = v2 -> Vcast v1 e = Vcast v2 e.

Lemma Vcast_eq : forall n (v1 v2 : vector A n) p (e : n=p),
Vcast v1 e = Vcast v2 e <-> v1 = v2.

Lemma Vcast_pi : forall n (v : vector A n) p (h1 : n=p) (h2 : n=p),
Vcast v h1 = Vcast v h2.

Lemma Vcast_lr : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h12 : n1=n2) (h21 : n2=n1), Vcast v1 h12 = v2 -> v1 = Vcast v2 h21.

Lemma Vcast_rl : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h12 : n1=n2) (h21 : n2=n1), v1 = Vcast v2 h21 -> Vcast v1 h12 = v2.

Lemma Vcast_introrl : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h21 : n2=n1), Vcast v1 (sym_eq h21) = v2 -> v1 = Vcast v2 h21.

Lemma Vcast_elimlr : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h12 : n1=n2), Vcast v1 h12 = v2 -> v1 = Vcast v2 (sym_eq h12).

End Vcast.

## Lemma and tactic for replacing an empty vector by Vnil.

Definition VO_eq A (v : vector A O) : v = Vnil
:= match v with Vnil => eq_refl _ end.

Ltac VOtac := repeat
match goal with
| v : vector _ O |- _ => assert (v = Vnil); [apply VO_eq | subst v]
end.

## N-th element of a vector.

Section Vnth.

Variable A : Type.

Program Fixpoint Vnth n (v : vector A n) : forall i, i < n -> A :=
match v with
| Vnil => fun i ip => !
| Vcons x v' => fun i =>
match i with
| 0 => fun _ => x
| S j => fun H => Vnth v' (i:=j) _
end
end.
Solve Obligations with program_simplify; auto with *.

Lemma Vhead_nth : forall n (v : vector A (S n)), Vhead v = Vnth v (lt_O_Sn n).

Lemma Vnth_eq : forall n (v : vector A n) i1 (h1 : i1<n) i2 (h2 : i2<n),
i1 = i2 -> Vnth v h1 = Vnth v h2.

Lemma Vnth_tail : forall n (v : vector A (S n)) i (h : i < n),
Vnth (Vtail v) h = Vnth v (lt_n_S h).

Lemma Vnth_cons_head : forall x n (v : vector A n) k (h : k < S n),
k = 0 -> Vnth (Vcons x v) h = x.

Lemma Vnth_cons_tail_aux : forall n i, i < S n -> i > 0 -> i-1 < n.

Lemma Vnth_cons_tail : forall x n (v : vector A n) i (h1:i<S n) (h2:i>0),
Vnth (Vcons x v) h1 = Vnth v (Vnth_cons_tail_aux h1 h2).

Lemma Vnth_cons : forall x n (v : vector A n) i (h1:i<S n),
Vnth (Vcons x v) h1 = match lt_ge_dec 0 i with
| left h2 => Vnth v (Vnth_cons_tail_aux h1 h2)
| _ => x
end.

Lemma Vnth_const : forall n (a : A) i (ip : i < n), Vnth (Vconst a n) ip = a.

Lemma Vnth_cast_aux : forall n n' k, n = n' -> k < n' -> k < n.

Lemma Vnth_cast : forall n (v : vector A n) n' (e : n = n') k (h : k < n'),
Vnth (Vcast v e) h = Vnth v (Vnth_cast_aux e h).

Lemma Veq_nth : forall n (v v' : vector A n),
(forall i (ip : i < n), Vnth v ip = Vnth v' ip) -> v = v'.

End Vnth.

Notation "v '[@' p ']'" := (Vnth v p) (at level 0) : vec_scope.

## Add an element at the end of a vector.

Variable A : Type.

Fixpoint Vadd n (v : vector A n) (x : A) : vector A (S n) :=
match v with
| Vnil => Vcons x Vnil
| Vcons a v' => Vcons a (Vadd v' x)
end.

Lemma Vnth_addl : forall k n (v : vector A n) a (H1 : k < S n) (H2 : k < n),
Vnth (Vadd v a) H1 = Vnth v H2.

Lemma Vnth_addr : forall k n (v : vector A n) a (H1 : k < S n) (H2 : k = n),
Vnth (Vadd v a) H1 = a.

Lemma Vnth_add_aux : forall i n, i < S n -> i <> n -> i < n.

Lemma Vnth_add : forall n (v : vector A n) x i (h : i < S n),
Vnth (Vadd v x) h =
match eq_nat_dec i n with
| left _ => x
| right n => Vnth v (Vnth_add_aux h n)
end.

Lemma Vadd_cons : forall x n (v : vector A (S n)),
Vadd v x = Vcons (Vhead v) (Vadd (Vtail v) x).

## Replace the i-th element of a vector by some value.

Section Vreplace.

Variable A : Type.

Program Fixpoint Vreplace n (v : vector A n) i (ip : i < n) (a : A)
: vector A n :=
match v with
| Vnil => !
| Vcons h v' =>
match i with
| 0 => Vcons a v'
| S i' => Vcons h (Vreplace v' (i:=i') _ a)
end
end.
Solve Obligations with program_simplify ; auto with *.

Lemma Vreplace_tail : forall n i (ip : S i < S n) (v : vector A (S n)) a,
Vreplace v ip a = Vcons (Vhead v) (Vreplace (Vtail v) (lt_S_n ip) a).

Lemma Vnth_replace : forall n i (ip ip' : i < n) (v : vector A n) (a : A),
Vnth (Vreplace v ip a) ip' = a.

Lemma Vnth_replace_neq : forall n i (ip : i < n) j (jp : j < n)
(v : vector A n) (a : A), i <> j -> Vnth (Vreplace v ip a) jp = Vnth v jp.

Lemma Vreplace_pi : forall n (v : vector A n) i1 i2 (h1 : i1 < n)
(h2 : i2 < n) x, i1 = i2 -> Vreplace v h1 x = Vreplace v h2 x.

Lemma Vreplace_eq_elim : forall n (v : vector A n) i (h : i < n) x x',
Vreplace v h x = Vreplace v h x' -> x = x'.

Lemma Vreplace_nth_eq : forall n (v : vector A n) i (h : i < n),
Vreplace v h (Vnth v h) = v.

End Vreplace.

## Concatenation of two vectors.

Section Vapp.

Variable A : Type.

Fixpoint Vapp n1 n2 (v1 : vector A n1) (v2 : vector A n2)
: vector A (n1+n2) :=
match v1 with
| Vnil => v2
| Vcons a v' => Vcons a (Vapp v' v2)
end.

Lemma Vapp_cons : forall a n1 n2 (v1 : vector A n1) (v2 : vector A n2),
Vapp (Vcons a v1) v2 = Vcons a (Vapp v1 v2).

Lemma Vapp_nil_eq : forall n (v : vector A n) (w : vector A 0) (h : n=n+0),
Vapp v w = Vcast v h.

Lemma Vapp_nil : forall n (v : vector A n) (w : vector A 0),
Vapp v w = Vcast v (plus_n_O n).

Lemma Vapp_rcast_eq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p2
(h1 : n2=p2) (h2 : n1+n2=n1+p2),
Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) h2.

Lemma Vapp_rcast : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p2
(h1 : n2=p2),
Vapp v1 (Vcast v2 h1) = Vcast (Vapp v1 v2) (plus_reg_l_inv n1 h1).

Lemma Vapp_lcast_eq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p1
(h1 : n1=p1) (h2 : n1+n2=p1+n2),
Vapp (Vcast v1 h1) v2 = Vcast (Vapp v1 v2) h2.

Lemma Vapp_lcast : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) p1
(h1 : n1=p1),
Vapp (Vcast v1 h1) v2 = Vcast (Vapp v1 v2) (plus_reg_r_inv n2 h1).

Lemma Vapp_assoc_eq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
n3 (v3 : vector A n3) (h : n1+(n2+n3) = (n1+n2)+n3),
Vapp (Vapp v1 v2) v3 = Vcast (Vapp v1 (Vapp v2 v3)) h.

Lemma Vapp_assoc : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
n3 (v3 : vector A n3),
Vapp (Vapp v1 v2) v3 = Vcast (Vapp v1 (Vapp v2 v3)) (plus_assoc n1 n2 n3).

Lemma Vapp_eq_intro : forall n1 (v1 v1' : vector A n1) n2
(v2 v2' : vector A n2), v1 = v1' -> v2 = v2' -> Vapp v1 v2 = Vapp v1' v2'.

Lemma Vapp_eq : forall n1 (v1 v1' : vector A n1) n2 (v2 v2' : vector A n2),
Vapp v1 v2 = Vapp v1' v2' <-> v1 = v1' /\ v2 = v2'.

Lemma Vnth_app_aux : forall n1 n2 i, i < n1+n2 -> n1 <= i -> i - n1 < n2.

Lemma Vnth_app : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
i (h : i < n1+n2), Vnth (Vapp v1 v2) h =
match le_gt_dec n1 i with
| left p => Vnth v2 (Vnth_app_aux h p)
| right p => Vnth v1 p
end.

Lemma Vnth_app_cons : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h : n1 < n1 + S n2) x, Vnth (Vapp v1 (Vcons x v2)) h = x.

Lemma Vnth_app_cons_neq : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2) k
(h : k < n1 + S n2) x x',
k <> n1 -> Vnth (Vapp v1 (Vcons x v2)) h = Vnth (Vapp v1 (Vcons x' v2)) h.

Lemma Vapp_cast_aux : forall n1 n2 n2', n2 = n2' -> n1+n2 = n1+n2'.

Lemma Vapp_cast : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
n2' (e : n2 = n2'),
Vapp v1 (Vcast v2 e) = Vcast (Vapp v1 v2) (Vapp_cast_aux n1 e).

Lemma Vadd_app_aux : forall p q, p + S q = S (p+q).

Lemma Vadd_app : forall p (v : vector A p) q (w : vector A q) x,
Vadd (Vapp v w) x = Vcast (Vapp v (Vadd w x)) (Vadd_app_aux p q).

End Vapp.

## Breaking a vector into two sub-vectors.

Section Vbreak.

Variable A : Type.

Fixpoint Vbreak n1 n2 : vector A (n1+n2) -> vector A n1 * vector A n2 :=
match n1 with
| O => fun v => (Vnil, v)
| S p1 => fun v =>
let w := Vbreak p1 n2 (Vtail v) in (Vcons (Vhead v) (fst w), snd w)
end.

Lemma Vbreak_app : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2),
Vbreak (Vapp v1 v2) = (v1, v2).

Lemma Vbreak_eq_app : forall n1 n2 (v : vector A (n1+n2)),
v = Vapp (fst (Vbreak v)) (snd (Vbreak v)).

Lemma Vbreak_eq_app_cast : forall n n1 n2 (H : n1+n2=n) (v : vector A n),
v = Vcast (Vapp (fst (Vbreak (Vcast v (sym_equal H))))
(snd (Vbreak (Vcast v (sym_equal H))))) H.

End Vbreak.

## Membership predicate on vectors.

Section Vin.

Variable A : Type.

Fixpoint Vin (x : A) n (v : vector A n) : Prop :=
match v with
| Vnil => False
| Vcons y w => y = x \/ Vin x w
end.

Lemma Vin_head : forall n (v : vector A (S n)), Vin (Vhead v) v.

Lemma Vin_tail : forall n x (v : vector A (S n)), Vin x (Vtail v) -> Vin x v.

Lemma Vnth_in : forall n (v : vector A n) k (h : k<n), Vin (Vnth v h) v.

Lemma Vin_nth : forall n (v : vector A n) a, Vin a v ->
exists i, exists ip : i < n, Vnth v ip = a.

Lemma Vin_cast_intro : forall m n (H : m=n) (v : vector A m) x,
Vin x v -> Vin x (Vcast v H).

Lemma Vin_cast_elim : forall m n (H : m=n) (v : vector A m) x,
Vin x (Vcast v H) -> Vin x v.

Lemma Vin_cast : forall m n (H : m=n) (v : vector A m) x,
Vin x (Vcast v H) <-> Vin x v.

Lemma Vin_appl : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2),
Vin x v1 -> Vin x (Vapp v1 v2).

Lemma Vin_appr : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2),
Vin x v2 -> Vin x (Vapp v1 v2).

Lemma Vin_app_cons : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2),
Vin x (Vapp v1 (Vcons x v2)).

Lemma Vin_app : forall x n1 (v1 : vector A n1) n2 (v2 : vector A n2),
Vin x (Vapp v1 v2) -> Vin x v1 \/ Vin x v2.

Lemma Vin_elim : forall x n (v : vector A n), Vin x v ->
exists n1 (v1 : vector A n1) n2 (v2 : vector A n2) (H : n1 + S n2 = n),
v = Vcast (Vapp v1 (Vcons x v2)) H.

Variable eq_dec : forall x y : A, {x=y}+{~x=y}.

Lemma Vin_dec : forall x n (xs : vector A n), {Vin x xs}+{~Vin x xs}.

End Vin.

## Sub-vector.

Given a vector v of size n, two natural numbers i and k and a proof h that i+k<=n, then Vsub v h is the sub-vector of v of size k made of the elements v_i, ..., v_{i+k-1}.

Section Vsub.

Variable A : Type.

Lemma Vsub_aux1 : forall i k' n : nat, i + S k' <= n -> i < n.

Lemma Vsub_aux2: forall i k' n : nat, i + S k' <= n -> S i + k' <= n.

Fixpoint Vsub n (v : vector A n) i k : i+k<=n -> vector A k :=
match k as k return i+k<=n -> vector A k with
| 0 => fun _ => Vnil
| S k' => fun h =>
Vcons (Vnth v (Vsub_aux1 h)) (Vsub v (S i) k' (Vsub_aux2 h))
end.

Lemma Vsub_nil_aux : forall i k (h:i+k<=0) (e : 0=k),
Vsub Vnil h = Vcast Vnil e.

Lemma Vsub_nil_aux1 : forall i k, i+k <= 0 -> 0=k.

Lemma Vsub_nil : forall i k (h:i+k<=0),
Vsub Vnil h = Vcast Vnil (Vsub_nil_aux1 h).

Lemma Vsub_eq_nil k n (v : vector A n) i (h : i+k <= n) (hk : k = 0) :
Vsub v h = Vcast Vnil (eq_sym hk).

Lemma Vnth_sub_aux : forall n i k j, i+k<=n -> j<k -> i+j<n.

Lemma Vnth_sub : forall k n (v : vector A n) i (h : i+k<=n) j (p : j<k),
Vnth (Vsub v h) p = Vnth v (Vnth_sub_aux h p).

Lemma Vsub_cons_aux : forall n i k, S i + k <= S n -> i + k <= n.

Lemma Vsub_cons : forall x i k n (v : vector A n) (h : S i + k <= S n),
Vsub (Vcons x v) h = Vsub v (Vsub_cons_aux h).

Lemma Vsub_pi : forall n (v : vector A n) i k (h h' : i+k<=n),
Vsub v h = Vsub v h'.

Lemma Vsub_cast_aux : forall n (v : vector A n) n' (e : n=n') i k
(h : i+k<=n') (h' : i+k<=n), Vsub (Vcast v e) h = Vsub v h'.

Lemma Vsub_cast_aux1 : forall n n' i k, n=n' -> i+k<=n' -> i+k<=n.

Lemma Vsub_cast : forall n (v : vector A n) n' (e : n=n') i k (h : i+k<=n')
(h' : i+k<=n), Vsub (Vcast v e) h = Vsub v (Vsub_cast_aux1 e h).

Lemma Vcast_sub_aux1 : forall n i k j, i + k <= n -> k = j -> i + j <= n.

Lemma Vcast_sub : forall n (v : vector A n) i k (h : i + k <= n) j
(e : k = j), Vcast (Vsub v h) e = Vsub v (Vcast_sub_aux1 h e).

Lemma Vcons_nth_aux1 : forall n i k, i < n -> S i+k <= n -> i+S k <= n.

Lemma Vcons_nth : forall n (v : vector A n) i k (h1 : i<n)
(h2 : S i + k <= n),
Vcons (Vnth v h1) (Vsub v h2) = Vsub v (Vcons_nth_aux1 h1 h2).

Lemma Vsub_cons_intro_aux : forall n (v : vector A n) i k (h : i+k<=n)
(h1 : i<n) (h2 : S i + pred k <= n) (e : S (pred k) = k),
Vsub v h = Vcast (Vcons (Vnth v h1) (Vsub v h2)) e.

Lemma Vsub_cons_intro_aux1 : forall n i k, i+k<=n -> k>0 -> i<n.

Lemma Vsub_cons_intro_aux2 : forall n i k, i+k<=n -> k>0 -> S i+pred k <= n.

Lemma Vsub_cons_intro_aux3 : forall k, k>0 -> S(pred k) = k.

Lemma Vsub_cons_intro : forall n (v : vector A n) i k (h : i+k<=n) (p : k>0),
Vsub v h = Vcast (Vcons (Vnth v (Vsub_cons_intro_aux1 h p))
(Vsub v (Vsub_cons_intro_aux2 h p))) (Vsub_cons_intro_aux3 p).

Lemma Veq_app_aux : forall n (v : vector A n) i
(h1 : 0 + i <= n) (h2 : i + (n - i) <= n) (e : i + (n - i) = n),
v = Vcast (Vapp (Vsub v h1) (Vsub v h2)) e.

Lemma Veq_app_aux1 : forall n i, i <= n -> 0 + i <= n.

Lemma Veq_app_aux2 : forall n i, i <= n -> i + (n - i) <= n.

Lemma Veq_app_aux3 : forall n i, i <= n -> i + (n - i) = n.

Lemma Veq_app : forall n (v : vector A n) i (h : i<=n),
v = Vcast (Vapp (Vsub v (Veq_app_aux1 h)) (Vsub v (Veq_app_aux2 h)))
(Veq_app_aux3 h).

Lemma Veq_app_cons_aux : forall n (v : vector A n) i (h1 : 0 + i <= n)
(h2 : i < n) (h3 : S i + (n - S i) <= n) (e : i + S (n - S i) = n),
v = Vcast (Vapp (Vsub v h1) (Vcons (Vnth v h2) (Vsub v h3))) e.

Lemma Veq_app_cons_aux1 : forall n i, i < n -> 0 + i <= n.

Lemma Veq_app_cons_aux2 : forall n i, i < n -> S i + (n - S i) <= n.

Lemma Veq_app_cons_aux3 : forall n i, i < n -> i + S (n - S i) = n.

Lemma Veq_app_cons : forall n (v : vector A n) i (h : i<n),
v = Vcast (Vapp (Vsub v (Veq_app_cons_aux1 h))
(Vcons (Vnth v h) (Vsub v (Veq_app_cons_aux2 h))))
(Veq_app_cons_aux3 h).

Lemma Veq_sub_aux : forall n (v v' : vector A n) i (h1 : 0+i<=n)
(h2 : i+(n-i)<=n),
Vsub v h1 = Vsub v' h1 -> Vsub v h2 = Vsub v' h2 -> v = v'.

Lemma Veq_sub : forall n (v v' : vector A n) i (h : i<=n),
Vsub v (Veq_app_aux1 h) = Vsub v' (Veq_app_aux1 h) ->
Vsub v (Veq_app_aux2 h) = Vsub v' (Veq_app_aux2 h) -> v = v'.

Lemma Veq_sub_cons_aux : forall n (v v' : vector A n) i (h1 : 0+i<=n)
(h2 : i<n) (h3 : S i+(n-S i)<=n), Vsub v h1 = Vsub v' h1 ->
Vnth v h2 = Vnth v' h2 -> Vsub v h3 = Vsub v' h3 -> v = v'.

Lemma Veq_sub_cons : forall n (v v' : vector A n) i (h : i<n),
Vsub v (Veq_app_cons_aux1 h) = Vsub v' (Veq_app_cons_aux1 h) ->
Vnth v h = Vnth v' h ->
Vsub v (Veq_app_cons_aux2 h) = Vsub v' (Veq_app_cons_aux2 h) -> v = v'.

Lemma Vsub_replace_l : forall n (v : vector A n) i (h : i<n) x j k
(p : j+k<=n), j+k <= i -> Vsub (Vreplace v h x) p = Vsub v p.

Lemma Vsub_replace_r : forall n (v : vector A n) i (h : i<n) x j k
(p : j+k<=n), j > i -> Vsub (Vreplace v h x) p = Vsub v p.

Lemma Vsub_app_l_aux : forall n1 n2 i, i <= n1 -> 0 + i <= n1 + n2.

Lemma Vsub_app_l : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h : 0+n1<=n1+n2), Vsub (Vapp v1 v2) h = v1.

Lemma Vsub_id : forall n (v : vector A n) (h:0+n<=n), Vsub v h = v.

Lemma Vsub_app_r : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2)
(h : n1+n2<=n1+n2), Vsub (Vapp v1 v2) h = v2.

End Vsub.

## Function removing the last element of a non-empty vector.

Section Vremove_last.

Variable A : Type.

Lemma Vremove_last_aux : forall n, 0 + n <= S n.

Definition Vremove_last A n (v : vector A (S n)) : vector A n :=
Vsub v (Vremove_last_aux n).

Lemma Vnth_remove_last_intro : forall n (v : vector A (S n)) i
(h1 : i<n) (h2 : i<S n), Vnth v h2 = Vnth (Vremove_last v) h1.

Lemma Vnth_remove_last : forall n (v : vector A (S n)) i
(h : i<n), Vnth (Vremove_last v) h = Vnth v (lt_S h).

Lemma Vremove_last_add : forall n (v : vector A n) x,
Vremove_last (Vadd v x) = v.

End Vremove_last.

## Last element of a vector with default value if empty.

Section Vlast.

Variable A : Type.

Fixpoint Vlast default n (v : vector A n) : A :=
match v with
| Vnil => default
| Vcons x v' => Vlast x v'
end.

Lemma Vlast_eq : forall x y n (v : vector A (S n)), Vlast x v = Vlast y v.

Lemma Vlast_nth : forall n (v : vector A (S n)) x (h : n < S n),
Vlast x v = Vnth v h.

Lemma Vlast_tail : forall n (v : vector A (S n)),
Vlast (Vhead v) (Vtail v) = Vlast (Vhead v) v.

Lemma VSn_add_default : forall x n (v : vector A (S n)),
v = Vadd (Vremove_last v) (Vlast x v).

Lemma VSn_add : forall n (v : vector A (S n)),
v = Vadd (Vremove_last v) (Vlast (Vhead v) v).

End Vlast.

## Function applying a function f on every element of a vector.

Section Vmap.

Variables (A B : Type) (f : A->B).

Fixpoint Vmap n (v : vector A n) : vector B n :=
match v with
| Vnil => Vnil
| Vcons a v' => Vcons (f a) (Vmap v')
end.

Lemma Vnth_map : forall n (v : vector A n) i (H : i < n),
Vnth (Vmap v) H = f (Vnth v H).

Lemma Vin_map : forall x n (v : vector A n),
Vin x (Vmap v) -> exists y, Vin y v /\ x = f y.

Lemma Vin_map_intro : forall x n (v : vector A n),
Vin x v -> Vin (f x) (Vmap v).

Lemma Vmap_app : forall n1 n2 (v1 : vector A n1) (v2 : vector A n2),
Vmap (Vapp v1 v2) = Vapp (Vmap v1) (Vmap v2).

Lemma Vmap_cast : forall m n (H : m=n) (v : vector A m),
Vmap (Vcast v H) = Vcast (Vmap v) H.

Lemma Vmap_tail : forall n (v : vector A (S n)),
Vmap (Vtail v) = Vtail (Vmap v).

Lemma Vmap_eq_nth : forall n (v1 : vector A n) (v2 : vector B n),
(forall i (h : i<n), f (Vnth v1 h) = Vnth v2 h) -> Vmap v1 = v2.

End Vmap.

Lemma Vmap_map : forall A B C (f:A->B) (g:B->C) n
(v : vector A n), Vmap g (Vmap f v) = Vmap (fun x : A => g (f x)) v.

## Predicate saying that every element of a vector satisfies some

predicate P.

Section Vforall.

Variables (A : Type) (P : A -> Prop).

Fixpoint Vforall n (v : vector A n) { struct v } : Prop :=
match v with
| Vnil => True
| Vcons a w => P a /\ Vforall w
end.

Lemma Vforall_intro : forall n (v : vector A n),
(forall x, Vin x v -> P x) -> Vforall v.

Lemma Vforall_nth_intro : forall n (v : vector A n),
(forall i (ip : i < n), P (Vnth v ip)) -> Vforall v.

Lemma Vforall_in : forall x n (v : vector A n), Vforall v -> Vin x v -> P x.

Lemma Vforall_eq : forall n (v : vector A n),
Vforall v <-> (forall x, Vin x v -> P x).

Lemma Vforall_nth : forall n (v : vector A n) i (ip : i < n),
Vforall v -> P (Vnth v ip).

Lemma Vforall_incl : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2),
(forall x, Vin x v1 -> Vin x v2) -> Vforall v2 -> Vforall v1.

Lemma Vforall_cast : forall n v p (h : n=p),
Vforall (Vcast v h) <-> Vforall v.

Lemma Vforall_app : forall p (v : vector A p) q (w : vector A q),
Vforall (Vapp v w) <-> Vforall v /\ Vforall w.

Decidability of Vforall.

Variable P_dec : forall x, {P x}+{~P x}.

Lemma Vforall_dec : forall n (v : vector A n), {Vforall v}+{~Vforall v}.

Variables (f : A -> bool) (f_ok : forall x, f x = true <-> P x).

Fixpoint bVforall n (v : vector A n) : bool :=
match v with
| Vnil => true
| Vcons a w => f a && bVforall w
end.

Lemma bVforall_ok : forall n (v : vector A n),
bVforall v = true <-> Vforall v.

End Vforall.

Lemma Vforall_impl : forall A (P Q : A -> Prop) n (v : vector A n),
Vforall P v -> (forall x, Vin x v -> P x -> Q x) -> Vforall Q v.

Lemma Vforall_map_elim : forall A B (f: A->B) (P : B->Prop) n (v : vector A n),
Vforall P (Vmap f v) -> Vforall (fun a : A => P (f a)) v.

Lemma Vforall_map_intro : forall A B (f: A->B) (P : B->Prop) n (v : vector A n),
Vforall (fun a : A => P (f a)) v -> Vforall P (Vmap f v).

## Equality of Vmap's.

Lemma Vmap_eq : forall (A B : Type) (f g : A->B) n (v : vector A n),
Vforall (fun a => f a = g a) v -> Vmap f v = Vmap g v.

Lemma Vmap_eq_ext : forall (A B : Type) (f g : A->B),
(forall a, f a = g a) ->
forall n (v : vector A n), Vmap f v = Vmap g v.

Lemma Vmap_id : forall (A : Type) n (v : vector A n),
Vmap (fun x => x) v = v.

Lemma Vmap_eq_id : forall (A : Type) (f : A->A) n (v : vector A n),
Vforall (fun a => f a = a) v -> Vmap f v = v.

Lemma Vmap_eq_ext_id : forall (A : Type) (f : A->A), (forall a, f a = a) ->
forall n (v : vector A n), Vmap f v = v.

## Predicate saying that the elements of two vectors are pairwise

in relation.

Section Vforall2.

Variables (A B : Type) (R : A -> B -> Prop).

Fixpoint Vforall2_aux n1 n2 (v1 : vector A n1) (v2 : vector B n2) : Prop :=
match v1, v2 with
| Vnil, Vnil => True
| Vcons a v, Vcons b w => R a b /\ Vforall2_aux v w
| _, _ => False
end.

Definition Vforall2 n (v1 : vector A n) (v2 : vector B n) :=
Vforall2_aux v1 v2.

Lemma Vforall2_tail : forall n (v1 : vector A (S n)) (v2 : vector B (S n)),
Vforall2 v1 v2 -> Vforall2 (Vtail v1) (Vtail v2).

Lemma Vforall2_elim_nth : forall n (v1 : vector A n) (v2 : vector B n) i
(ip : i < n), Vforall2 v1 v2 -> R (Vnth v1 ip) (Vnth v2 ip).

Lemma Vforall2_intro_nth : forall n (v1 : vector A n) (v2 : vector B n),
(forall i (ip : i < n), R (Vnth v1 ip) (Vnth v2 ip)) -> Vforall2 v1 v2.

Lemma Vforall2_cons_eq : forall u v n (us : vector A n) (vs : vector B n),
Vforall2 (Vcons u us) (Vcons v vs) <-> R u v /\ Vforall2 us vs.

Lemma Vforall2_cons_elim : forall n (u : vector A n) (v : vector B n) x y,
Vforall2 (Vcons x u) (Vcons y v) -> Vforall2 u v.

Lemma Vforall2_app_elim_l n1 (v1 : vector A n1) (v1' : vector B n1)
n2 (v2 : vector A n2) (v2' : vector B n2) :
Vforall2 (Vapp v1 v2) (Vapp v1' v2') -> Vforall2 v1 v1'.

Lemma Vforall2_app_elim_r n1 (v1 : vector A n1) (v1' : vector B n1)
n2 (v2 : vector A n2) (v2' : vector B n2) :
Vforall2 (Vapp v1 v2) (Vapp v1' v2') -> Vforall2 v2 v2'.

Lemma Vforall2_cast n (u : vector A n) (v : vector B n) n' (h h' : n=n') :
Vforall2 (Vcast u h) (Vcast v h') <-> Vforall2 u v.

Lemma Vforall2_sub : forall n (v1 : vector A n) (v2 : vector B n)
p q (h : p+q<=n), Vforall2 v1 v2 -> Vforall2 (Vsub v1 h) (Vsub v2 h).

Decidability of Vforall2.

Variable R_dec : forall x y, {R x y}+{~R x y}.

Lemma Vforall2_aux_dec : forall n1 (v1 : vector A n1) n2 (v2 : vector B n2),
{Vforall2_aux v1 v2} + {~Vforall2_aux v1 v2}.

Lemma Vforall2_dec n (v : vector A n) (w : vector B n) :
{Vforall2 v w}+{~Vforall2 v w}.

Variables (f : A -> B -> bool) (f_ok : forall x y, f x y = true <-> R x y).

Fixpoint bVforall2_aux n1 n2 (v1 : vector A n1) (v2 : vector B n2) : bool :=
match v1, v2 with
| Vnil, Vnil => true
| Vcons x xs, Vcons y ys => f x y && bVforall2_aux xs ys
| _, _ => false
end.

Lemma bVforall2_aux_ok : forall n1 (v1 : vector A n1) n2 (v2 : vector B n2),
bVforall2_aux v1 v2 = true <-> Vforall2_aux v1 v2.

Definition bVforall2 n (v1 : vector A n) (v2 : vector B n) :=
bVforall2_aux v1 v2.

Lemma bVforall2_ok : forall n (v1 : vector A n) (v2 : vector B n),
bVforall2 v1 v2 = true <-> Vforall2 v1 v2.

End Vforall2.

Properties of Vforall2 wrt relations.

Section Vforall2_rel.

Variables (A : Type) (R : relation A).

Global Instance Vforall2_refl :
Reflexive R -> forall n, Reflexive (Vforall2 (n:=n) R).

Global Instance Vforall2_trans :
Transitive R -> forall n, Transitive (Vforall2 (n:=n) R).

Global Instance Vforall2_sym :
Symmetric R -> forall n, Symmetric (Vforall2 (n:=n) R).

Global Instance Vforall2_equiv :
Equivalence R -> forall n, Equivalence (Vforall2 (n:=n) R).

End Vforall2_rel.

Section Vforall2_aux_Proper.

Variables (A : Type) (R : relation A) (B : Type) (S : relation B)
(F : A -> B -> Prop) (F_R : Proper (R ==> S ==> iff) F).

Global Instance Vforall2_aux_Proper n1 n2 :
Proper (Vforall2 R ==> Vforall2 S ==> iff)
(Vforall2_aux F (n1:=n1) (n2:=n2)).

End Vforall2_aux_Proper.

Properties of Vforall2 wrt Vmap.

Section Vforall2_map.

Variables (A : Type) (R : relation A) (B : Type) (S : relation B)
(f g : A -> B).

Lemma Vforall2_map_intro : forall n (v : vector A n),
Vforall (fun x => S (f x) (g x)) v -> Vforall2 S (Vmap f v) (Vmap g v).

End Vforall2_map.

## Predicate saying that some element of a vector satisfies some

predicate P.

Section Vexists.

Variables (A : Type) (P : A->Prop).

Fixpoint Vexists n (v : vector A n) : Prop :=
match v with
| Vnil => False
| Vcons a v' => P a \/ Vexists v'
end.

Lemma Vexists_eq : forall n (v : vector A n),
Vexists v <-> exists x, Vin x v /\ P x.

Variable f : A->bool.

Fixpoint bVexists n (v : vector A n) : bool :=
match v with
| Vnil => false
| Vcons a v' => f a || bVexists v'
end.

Lemma bVexists_ok_Vin : forall n (v : vector A n),
(forall x, Vin x v -> (f x = true <-> P x)) ->
(bVexists v = true <-> Vexists v).

Variable f_ok : forall x, f x = true <-> P x.

Lemma bVexists_ok : forall n (v : vector A n),
bVexists v = true <-> Vexists v.

End Vexists.

## Build a vector of size n from a function gen:foralli,i<n->A.

Section Vbuild.

Variable A : Type.

Program Fixpoint Vbuild_spec (n : nat) (gen : forall i, i < n -> A) :
{ v : vector A n | forall i (ip : i < n), Vnth v ip = gen i ip } :=
match n with
| 0 => Vnil
| S p =>
let gen' := fun i ip => gen (S i) _ in
Vcons (gen 0 _) (@Vbuild_spec p gen')
end.

Solve Obligations with coq_omega.

Definition Vbuild n gen : vector A n := proj1_sig (Vbuild_spec gen).

Lemma Vbuild_nth : forall n gen i (ip : i < n),
Vnth (Vbuild gen) ip = gen i ip.

Lemma Vbuild_in : forall n gen x, Vin x (Vbuild gen) ->
exists i, exists ip : i < n, x = gen i ip.

Lemma Vbuild_head : forall n (gen : forall i, i < S n -> A),
Vhead (Vbuild gen) = gen 0 (lt_O_Sn n).

Lemma Vbuild_tail n (gen : forall i, i < S n -> A) :
Vtail (Vbuild gen) = Vbuild (fun i ip => gen (S i) (lt_n_S ip)).

Lemma Vin_build : forall n (gen : forall i, i < n -> A) x,
(exists i (ip : i < n), x = gen i ip) -> Vin x (Vbuild gen).

End Vbuild.

## Iterators on vectors.

Vfold_left f a b1 .. bn = f .. (f (f a b1) b2) .. bn.

Section Vfold_left.

Variables (A B : Type) (f : A->B->A).

Fixpoint Vfold_left n (a:A) (v : vector B n) : A :=
match v with
| Vnil => a
| Vcons b w => Vfold_left (f a b) w
end.

Global Instance Vfold_left_Vforall2 n (R : rel A) (S : rel B) :
Proper (R ==> S ==> R) f
-> Proper (R ==> Vforall2 S ==> R) (Vfold_left (n:=n)).

End Vfold_left.

Vfold_right f a1 .. an b = f a1 (f a2 .. (f an b) .. ).

Fixpoint Vfold_right (A B : Type) (f : A->B->B) n (v : vector A n) (b:B) : B :=
match v with
| Vnil => b
| Vcons a w => f a (Vfold_right f w b)
end.

Vfold_left_rev f a b1 .. bn = f .. (f (f a bn) bn-1) .. b1.

Section Vfold_left_rev.

Variables (A B : Type) (f : A->B->A).

Fixpoint Vfold_left_rev n (a:A) (v : vector B n) : A :=
match v with
| Vnil => a
| Vcons b w => f (Vfold_left_rev a w) b
end.

Variables (R : relation A) (S : relation B) (f_S : Proper (R ==> S ==> R) f).

Global Instance Vfold_left_rev_Vforall2 n :
Proper (R ==> Vforall2 S ==> R) (Vfold_left_rev (n:=n)).

End Vfold_left_rev.

Section FoldOpt2.

Variable aT bT cT : Type.
Variable x : cT.
Variable F : aT -> bT -> cT -> option cT.

Fixpoint Vfold2 nA nB (vA : vector aT nA) (vB : vector bT nB) :=
match vA, vB with
| Vnil, Vnil => Some x
| Vcons xA sA, Vcons xB sB =>
match Vfold2 sA sB with
| Some v => F xA xB v
| None => None
end
| Vnil, Vcons _ _ => None
| Vcons _ _, Vnil => None
end.

End FoldOpt2.

## Convert a vector into a list of the same length.

Section vec_of_list.

Variable A : Type.

Fixpoint vec_of_list (l : list A) : vector A (length l) :=
match l with
| nil => Vnil
| cons x m => Vcons x (vec_of_list m)
end.

Lemma vec_of_list_cons : forall a l,
vec_of_list (a :: l) = Vcons a (vec_of_list l).

Fixpoint list_of_vec n (v : vector A n) : list A :=
match v with
| Vnil => nil
| Vcons x v => x :: list_of_vec v
end.

Lemma in_list_of_vec : forall n (v : vector A n) x,
In x (list_of_vec v) -> Vin x v.

Lemma list_of_vec_in : forall n (v : vector A n) x,
Vin x v -> In x (list_of_vec v).

Lemma Vin_vec_of_list : forall l x, In x l <-> Vin x (vec_of_list l).

Lemma Vnth_vec_of_list : forall l d i (Hi : i < length l),
Vnth (vec_of_list l) Hi = nth i l d.

Lemma vec_of_list_exact : forall i l (Hi : i < length(l)),
element_at l i = Some (Vnth (vec_of_list l) Hi).

Lemma list_of_vec_exact : forall i n (v : vector A n) (Hi : i < n),
element_at (list_of_vec v) i = Some (Vnth v Hi).

End vec_of_list.

Equivalence between Vforall and lforall.

Lemma lforall_Vforall : forall (A : Type) (l : list A) (p : A -> Prop),
lforall p l -> Vforall p (vec_of_list l).

Lemma Vforall_lforall : forall (A : Type) n (v : vector A n)
(p : A -> Prop), Vforall p v -> lforall p (list_of_vec v).

## Convert a list intro a vector of options of fixed length.

Fixpoint vec_opt_of_list A m (l : list A) : vector (option A) m :=
match m with
| 0 => Vnil
| S m' =>
match l with
| nil => Vconst None (S m')
| cons x l' => Vcons (Some x) (vec_opt_of_list m' l')
end
end.

Lemma Vnth_vec_opt_of_list A : forall i m (l : list A) (im : i < m)
(il : i < length l), Vnth (vec_opt_of_list m l) im = Some (ith il).

## Leibniz equality on vectorAn is decidable if Leibniz

equality on A is decidable.

Section eq_dec.

Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

Lemma eq_vec_dec : forall n (v1 v2 : vector A n), {v1=v2}+{~v1=v2}.

End eq_dec.

## Boolean function for testing the equality of two vectors.

Section beq.

Variables (A : Type) (beq : A -> A -> bool)
(beq_ok : forall x y, beq x y = true <-> x = y).

Fixpoint beq_vec n (v : vector A n) p (w : vector A p) :=
match v, w with
| Vnil, Vnil => true
| Vcons x v', Vcons y w' => beq x y && beq_vec v' w'
| _, _ => false
end.

Lemma beq_vec_refl : forall n (v : vector A n), beq_vec v v = true.

Lemma beq_vec_ok_length : forall n (v : vector A n) p (w : vector A p),
beq_vec v w = true -> n = p.

Lemma beq_vec_ok1_cast : forall n (v : vector A n) p (w : vector A p)
(leq : n = p), beq_vec v w = true -> Vcast v leq = w.

Lemma beq_vec_ok1 n (v w : vector A n) : beq_vec v w = true -> v = w.

Lemma beq_vec_ok2 : forall n (v w : vector A n), v = w -> beq_vec v w = true.

Lemma beq_vec_ok : forall n (v w : vector A n), beq_vec v w = true <-> v = w.

End beq.

Section beq_in.

Variables (A : Type) (beq : A -> A -> bool).

Lemma beq_vec_ok_in1 : forall n (v : vector A n)
(hyp : forall x, Vin x v -> forall y, beq x y = true <-> x = y)
p (w : vector A p) (h : beq_vec beq v w = true),
Vcast v (beq_vec_ok_length A beq h) = w.

Lemma beq_vec_ok_in2 : forall n (v : vector A n)
(hyp : forall x, Vin x v -> forall y, beq x y = true <-> x = y) w,
v = w -> beq_vec beq v w = true.

End beq_in.

## Function applying a function f on the first element of a

non-empty vector, or some default value if the vector is empty.

Section map_first.

Variables (A B : Type) (default : B) (f : A->B).

Definition Vmap_first n (v : vector A n) : B :=
match v with
| Vcons a _ => f a
| _ => default
end.

Lemma Vmap_first_cast : forall n (v : vector A n) n' (h : n=n'),
Vmap_first (Vcast v h) = Vmap_first v.

End map_first.

## Binary map function on vectors.

Section Vmap2.

Variables (A B C : Type) (f: A->B->C).

Fixpoint Vmap2 n : vector A n -> vector B n -> vector C n :=
match n with
| O => fun _ _ => Vnil
| _ => fun v1 v2 =>
Vcons (f (Vhead v1) (Vhead v2)) (Vmap2 (Vtail v1) (Vtail v2))
end.

Lemma Vnth_map2 : forall n (vl : vector A n) (vr : vector B n) i (ip : i < n),
Vnth (Vmap2 vl vr) ip = f (Vnth vl ip) (Vnth vr ip).

Variables (R : relation A) (S : relation B) (T : relation C)
(f_mor : Proper (R ==> S ==> T) f).

Global Instance Vmap2_proper n :
Proper (Vforall2 R ==> Vforall2 S ==> Vforall2 T) (Vmap2 (n:=n)).

End Vmap2.

## Vectors of sigP.

Section Vsig.

Variables (A : Type) (P : A -> Prop).

Fixpoint Vsig_of_forall n (v : vector A n) :
Vforall P v -> vector (sig P) n :=
match v in vector _ n return Vforall P v -> vector (sig P) n with
| Vnil => fun _ => Vnil
| Vcons a w => fun H =>
Vcons (exist (proj1 H)) (Vsig_of_forall w (proj2 H))
end.

Fixpoint Vforall_of_sig (A : Type) (P : A -> Prop) n (v : vector (sig P) n) :
Vforall P (Vmap (@proj1_sig A P) v) :=
match v in vector _ n return Vforall P (Vmap (@proj1_sig A P) v) with
| Vnil => I
| Vcons a w => conj (@proj2_sig A P a) (Vforall_of_sig w)
end.

Lemma Vmap_proj1_sig : forall n (v : vector A n)
(Hv : Vforall P v), v = Vmap (@proj1_sig A P) (Vsig_of_forall _ Hv).

End Vsig.

## Build a vector of optionA of size n from the elements (if

they exist) of an arbitrary vector xs of size p whose positions are given by a vector ks of natural numbers of size n.

Section Vopt_filter.

Variable (A : Type).

Fixpoint Vopt_filter n (ks : vector nat n) p (xs : vector A p) :=
match ks in vector _ n return vector (option A) n with
| Vnil => Vnil
| Vcons k ks' =>
Vcons (match lt_dec k p with left h => Some (Vnth xs h) | _ => None end)
(Vopt_filter ks' xs)
end.

Lemma Vnth_opt_filter :
forall p (xs : vector A p) n (ks : vector nat n) i (hi : i<n),
Vnth (Vopt_filter ks xs) hi =
match lt_dec (Vnth ks hi) p with
| left h => Some (Vnth xs h)
| _ => None
end.

Lemma Vnth_opt_filter_Some_elim :
forall p (xs : vector A p) n (ks : vector nat n) i (hi : i<n) x,
Vnth (Vopt_filter ks xs) hi = Some x ->
exists h : Vnth ks hi < p, x = Vnth xs h.

Lemma Vnth_opt_filter_Some_intro : forall p (xs : vector A p)
n (ks : vector nat n) i (hi : i<n) (h : Vnth ks hi < p),
Vnth (Vopt_filter ks xs) hi = Some (Vnth xs h).

Lemma Vopt_filter_cast p (xs : vector A p) p' (h : p = p') :
forall n (ks : vector nat n),
Vopt_filter ks (Vcast xs h) = Vopt_filter ks xs.

Lemma Vopt_filter_app p (xs : vector A p) q (ys : vector A q) x :
forall n (ks : vector nat n) i (hi : i < n),
Vnth (Vopt_filter ks xs) hi = Some x ->
Vnth (Vopt_filter ks (Vapp xs ys)) hi = Some x.

Global Instance Vopt_filter_proper R n (ks : vector nat n) p :
Proper (Vforall2 R ==> Vforall2 (opt_r R)) (Vopt_filter ks (p:=p)).

End Vopt_filter.

Relation between Vopt_filter and Vmap.

Section Vopt_filter_map.

Variables (A B : Type) (f : A -> B).

Definition fopt x :=
match x with
| Some v => Some (f v)
| None => None
end.

Lemma Vopt_filter_map : forall p (xs : vector A p) n (ks : vector nat n),
Vopt_filter ks (Vmap f xs) = Vmap fopt (Vopt_filter ks xs).

End Vopt_filter_map.

Properties of sorted filters.

Definition sorted n (ks : vector nat n) :=
forall i (hi : i < n) j (hj : j < n), i < j -> Vnth ks hi < Vnth ks hj.

Lemma sorted_cons_elim n k (ks : vector nat n) :
sorted (Vcons k ks) -> sorted ks.

Lemma Vnth_opt_filter_sorted_None A p (ts : vector A p) :
forall n (ks : vector nat n), sorted ks ->
forall i (hi : i < n), Vnth (Vopt_filter ks ts) hi = None ->
forall j (hj : j < n), i < j -> Vnth (Vopt_filter ks ts) hj = None.

## Extension of a relation on A to a relation on vector(optionA)

so that Vforall2_opt (n:=n) R us vs if there are k <= n, xs, ys : vector A k such that us = Vapp (Vmap Some xs) (Vconst None (n-k)), vs = Vapp (Vmap Some ys) (Vconst None (n-k)) and Vforall2 R xs ys.

Definition Vforall2_opt {n A} (R : relation A) :
relation (vector (option A) n) :=
fun us vs => exists i (h : i <= n),
Vforall2 (opt R) (Vsub us (Veq_app_aux1 h)) (Vsub vs (Veq_app_aux1 h))
/\ Vforall2 (opt_r empty_rel) (Vsub us (Veq_app_aux2 h))
(Vsub vs (Veq_app_aux2 h)).

Lemma Vforall2_opt_filter A p (ts us : vector A p) (R : relation A) :
forall n (ks : vector nat n), sorted ks ->
(forall i (ip : i < p), Vin i ks -> R (Vnth ts ip) (Vnth us ip)) ->
Vforall2_opt R (Vopt_filter ks ts) (Vopt_filter ks us).

## First position of an element in a vector.

Section first_position.

Variables (A : Type) (P : A -> Prop) (P_dec : forall y : A, {P y}+{~P y}).

Fixpoint Vfirst_position_aux k n (ys : vector A n) :=
match ys with
| Vnil => None
| Vcons y ys' =>
match P_dec y with
| left _ => Some k
| _ => Vfirst_position_aux (S k) ys'
end
end.

Definition Vfirst_position := Vfirst_position_aux 0.

Lemma Vfirst_position_aux_lt : forall n (ys : vector A n) k i,
Vfirst_position_aux k ys = Some i -> i < k+n.

Lemma Vfirst_position_lt : forall n (ys : vector A n) i,
Vfirst_position ys = Some i -> i < n.

Lemma Vfirst_position_aux_ge : forall n (ys : vector A n) k i,
Vfirst_position_aux k ys = Some i -> i >= k.

Lemma Vfirst_position_aux_nth : forall n (ys : vector A n) k i j (hj : j<n),
Vfirst_position_aux k ys = Some i -> P (Vnth ys hj) -> i <= k+j.

Lemma Vfirst_position_nth : forall n (ys : vector A n) i j (hj : j<n),
Vfirst_position ys = Some i -> P (Vnth ys hj) -> i <= j.

Lemma Vnth_first_position_aux : forall n (ys : vector A n) k i (hi : i-k < n),
Vfirst_position_aux k ys = Some i -> P (Vnth ys hi).

Lemma Vnth_first_position : forall n (ys : vector A n) i (hi : i<n),
Vfirst_position ys = Some i -> P (Vnth ys hi).

End first_position.

Section first_position_eq.

Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}) (x : A).

Lemma Vfirst_position_aux_in : forall n (ys : vector A n) k i,
Vfirst_position_aux (eq_dec x) k ys = Some i -> Vin x ys.

Lemma Vfirst_position_in : forall n (ys : vector A n) i,
Vfirst_position (eq_dec x) ys = Some i -> Vin x ys.

Lemma Vin_first_position_aux : forall n (ys : vector A n) k,
Vin x ys -> exists i, Vfirst_position_aux (eq_dec x) k ys = Some i.

Lemma Vin_first_position : forall n (ys : vector A n),
Vin x ys -> exists i, Vfirst_position (eq_dec x) ys = Some i.

End first_position_eq.