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.


Section Vadd.

  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).

End Vadd.

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: forall i, 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 vector A n 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 sig P.


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 option A 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 (option A)

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.