(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Vector.ma: Fixed length polymorphic vectors, and routine operations on     *)
(*            them.                                                           *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

include "basics/lists/list.ma".
include "basics/bool.ma".
include "basics/types.ma".

include "ASM/Util.ma".

include "arithmetics/nat.ma".

include "utilities/extranat.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* The datatype.                                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

inductive Vector (A: Type[0]): nat → Type[0] ≝
  VEmpty: Vector A O
| VCons: ∀n: nat. A → Vector A n → Vector A (S n).

lemma Vector_O:
  ∀A: Type[0].
  ∀v: Vector A 0.
    v ≃ VEmpty A.
 #A #v
 generalize in match (refl … 0);
 cases v in ⊢ (??%? → ?%%??); //
 #n #hd #tl #absurd
 destruct(absurd)
qed.

lemma Vector_Sn:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A (S n).
    ∃hd: A. ∃tl: Vector A n.
      v ≃ VCons A n hd tl.
  #A #n #v
  generalize in match (refl … (S n));
  cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
  [1:
    #absurd destruct(absurd)
  |2:
    #m #hd #tl #eq
    <(injective_S … eq)
    %{hd} %{tl} %
  ]
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Syntax.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

notation "hvbox(hd break ::: tl)"
  right associative with precedence 57
  for @{ 'vcons $hd $tl }.

notation "[[ list0 x sep ; ]]"
  non associative with precedence 90
  for ${fold right @'vnil rec acc @{'vcons $x $acc}}.

interpretation "Vector vnil" 'vnil = (VEmpty ?).
interpretation "Vector vcons" 'vcons hd tl = (VCons ? ? hd tl).

notation "hvbox(l break !!! break n)"
  non associative with precedence 90
  for @{ 'get_index_v $l $n }.

lemma dependent_rewrite_vectors:
  ∀A:Type[0].
  ∀n, m: nat.
  ∀v1: Vector A n.
  ∀v2: Vector A m.
  ∀P: ∀m. Vector A m → Prop.
    n = m → v1 ≃ v2 → P n v1 → P m v2.
  #A #n #m #v1 #v2 #P #eq #jmeq
  destruct #assm assumption
qed.

lemma jmeq_cons_vector_monotone:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v: Vector A m.
  ∀q: Vector A n.
  ∀prf: m = n.
  ∀hd: A.
    v ≃ q → hd:::v ≃ hd:::q.
  #A #m #n #v #q #prf #hd #E
  @(dependent_rewrite_vectors A … E)
  try assumption %
qed.

lemma Vector_singl_elim : ∀A.∀P : Vector A 1 → Prop.∀v.
  (∀a.v = [[ a ]] → P [[ a ]]) → P v.
#A #P #v
elim (Vector_Sn … v) #a * #tl >(Vector_O … tl) #EQ >EQ #H @H % qed.

lemma Vector_pair_elim : ∀A.∀P : Vector A 2 → Prop.∀v.
  (∀a,b.v = [[ a ; b ]] → P [[ a ; b ]]) → P v.
#A #P #v
elim (Vector_Sn … v) #a * #tl @(Vector_singl_elim … tl) #b #EQ1 #EQ2 destruct
#H @H %
qed.

lemma Vector_triple_elim : ∀A.∀P : Vector A 3 → Prop.∀v.
  (∀a,b,c.v = [[ a ; b ; c ]] → P [[ a ; b ; c ]]) → P v.
#A #P #v
elim (Vector_Sn … v) #a * #tl @(Vector_pair_elim … tl) #b #c #EQ1 #EQ2 destruct
#H @H %
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lookup.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

let rec get_index_v (A: Type[0]) (n: nat)
                   (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝
  (match m with
    [ O ⇒
      match v return λx.λ_. O < x → A with
        [ VEmpty ⇒ λabsd1: O < O. ?
        | VCons p hd tl ⇒ λprf1: O < S p. hd
        ]
    | S o ⇒
      (match v return λx.λ_. S o < x → A with
        [ VEmpty ⇒ λprf: S o < O. ?
        | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ?
        ])
    ]) lt.
    [ cases (not_le_Sn_O O)
      normalize in absd1;
      # H
      cases (H absd1)
    | cases (not_le_Sn_O (S o))
      normalize in prf;
      # H
      cases (H prf)
    | normalize
      normalize in prf;
      @ le_S_S_to_le
      assumption
    ]
qed.

definition get_index' ≝
  λA: Type[0].
  λn, m: nat.
  λb: Vector A (S (n + m)).
    get_index_v A (S (n + m)) b n ?.
  normalize
  @le_S_S
  cases m //
qed.

let rec get_index_weak_v (A: Type[0]) (n: nat)
                         (v: Vector A n) (m: nat) on m ≝
  match m with
    [ O ⇒
      match v with
        [ VEmpty ⇒ None A
        | VCons p hd tl ⇒ Some A hd
        ]
    | S o ⇒
      match v with
        [ VEmpty ⇒ None A
        | VCons p hd tl ⇒ get_index_weak_v A p tl o
        ]
    ].
    
interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n).

let rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝
  (match m with
    [ O ⇒
      match v return λx.λ_. O < x → Vector A x with
        [ VEmpty ⇒ λabsd1: O < O. [[ ]]
        | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl)
        ]
    | S o ⇒
      (match v return λx.λ_. S o < x → Vector A x with
        [ VEmpty ⇒ λprf: S o < O. [[ ]]
        | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?)
        ])
    ]) lt.
    normalize in prf ⊢ %;
    /2/;
qed.

let rec set_index_weak (A: Type[0]) (n: nat)
                       (v: Vector A n) (m: nat) (a: A) on m ≝
  match m with
    [ O ⇒
      match v with
        [ VEmpty ⇒ None (Vector A n)
        | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl))
        ]
    | S o ⇒
      match v with
        [ VEmpty ⇒ None (Vector A n)
        | VCons p hd tl ⇒
            let settail ≝ set_index_weak A p tl o a in
              match settail with
                [ None ⇒ None (Vector A n)
                | Some j ⇒ Some (Vector A n) (? (VCons A p hd j))
                ]
        ]
    ].
    //.
qed.

let rec drop (A: Type[0]) (n: nat)
             (v: Vector A n) (m: nat) on m ≝
  match m with
    [ O ⇒ Some (Vector A n) v
    | S o ⇒
      match v with
        [ VEmpty ⇒ None (Vector A n)
        | VCons p hd tl ⇒ ? (drop A p tl o)
        ]
    ].
    //.
qed.

definition head' : ∀A:Type[0]. ∀n:nat. Vector A (S n) → A ≝
λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | _ ⇒ A ] with
[ VEmpty ⇒ I | VCons _ hd _ ⇒ hd ].

definition tail : ∀A:Type[0]. ∀n:nat. Vector A (S n) → Vector A n ≝
λA,n,v. match v return λx.λ_. match x with [ O ⇒ True | S m ⇒ Vector A m ] with
[ VEmpty ⇒ I | VCons m hd tl ⇒ tl ].

lemma tail_head' : ∀A,n,v.v = head' A n v ::: tail … v.
#A #n #v elim (Vector_Sn … v) #hd * #tl #EQ >EQ % qed.

let rec vsplit' (A: Type[0]) (m, n: nat) on m: Vector A (plus m n) → (Vector A m) × (Vector A n) ≝
 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with
  [ O ⇒ λv. 〈[[ ]], v〉
  | S m' ⇒ λv. let 〈l,r〉 ≝ vsplit' A m' n (tail ?? v) in 〈head' ?? v:::l, r〉
  ].
(* Prevent undesirable unfolding. *)
let rec vsplit (A: Type[0]) (m, n: nat) (v:Vector A (plus m n)) on v : (Vector A m) × (Vector A n) ≝
 vsplit' A m n v.

lemma vsplit_zero:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = vsplit A 0 m v.
  #A #m #v
  cases v try %
  #n #hd #tl %
qed.

definition head: ∀A: Type[0]. ∀n: nat. Vector A (S n) → A × (Vector A n) ≝
  λA: Type[0].
  λn: nat.
  λv: Vector A (S n).
  match v return λl. λ_: Vector A l. l = S n → A × (Vector A n) with
  [ VEmpty ⇒ λK. ⊥
  | VCons o he tl ⇒ λK. 〈he, (tl⌈Vector A o ↦ Vector A n⌉)〉
  ] (? : S ? = S ?).
  //
  destruct
qed.

definition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝
 λA: Type[0].
 λv: Vector A (S 0).
   fst … (head … v).
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Folds and builds.                                                          *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
let rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
  match v with
    [ VEmpty ⇒ x
    | VCons n hd tl ⇒ f hd (fold_right A B n f x tl)
    ].

let rec fold_right_i (A: Type[0]) (B: nat → Type[0]) (n: nat)
                     (f: ∀n. A → B n → B (S n)) (x: B 0) (v: Vector A n) on v ≝
  match v with
    [ VEmpty ⇒ x
    | VCons n hd tl ⇒ f ? hd (fold_right_i A B n f x tl)
    ].

let rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0])
                      (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat)
                      (v: Vector A n) (q: Vector B n) on v : C n ≝
  (match v return λx.λ_. x = n → C n with
    [ VEmpty ⇒
      match q return λx.λ_. O = x → C x with
        [ VEmpty ⇒ λprf: O = O. c
        | VCons o hd tl ⇒ λabsd. ⊥
        ]
    | VCons o hd tl ⇒ 
      match q return λx.λ_. S o = x → C x with
        [ VEmpty ⇒ λabsd: S o = O. ⊥
        | VCons p hd' tl' ⇒ λprf: S o = S p.
           (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉
        ]
    ]) (refl ? n).
  [1,2:
    destruct
  |3,4:
    lapply (injective_S … prf)
    //
  ]
qed.
  
let rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
  match v with
    [ VEmpty ⇒ x
    | VCons n hd tl ⇒ fold_left A B n f (f x hd) tl
    ].
    
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Maps and zips.                                                             *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

let rec map (A: Type[0]) (B: Type[0]) (n: nat)
             (f: A → B) (v: Vector A n) on v ≝
  match v with
    [ VEmpty ⇒ [[ ]]
    | VCons n hd tl ⇒ (f hd) ::: (map A B n f tl)
    ].

let rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat)
             (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝
  (match v return (λx.λr. x = n → Vector C x) with
    [ VEmpty ⇒ λ_. [[ ]]
    | VCons n hd tl ⇒
      match q return (λy.λr. S n = y → Vector C (S n)) with
        [ VEmpty ⇒ ?
        | VCons m hd' tl' ⇒
            λe: S n = S m.
              (f hd hd') ::: (zip_with A B C n f tl ?)
        ]
    ])
    (refl ? n).
  [ #e
    destruct(e);
  | lapply (injective_S … e)
    # H
    > H
    @ tl'
  ]
qed.

definition zip ≝
  λA, B: Type[0].
  λn: nat.
  λv: Vector A n.
  λq: Vector B n.
    zip_with A B (A × B) n (mk_Prod A B) v q.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Building vectors from scratch                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

let rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝
  match n return λn. Vector A n with
    [ O ⇒ [[ ]]
    | S m ⇒ h ::: (replicate A m h)
    ].

(* DPM: fixme.  Weird matita bug in base case. *)
let rec append (A: Type[0]) (n: nat) (m: nat)
                (v: Vector A n) (q: Vector A m) on v ≝
  match v return (λn.λv. Vector A (n + m)) with
    [ VEmpty ⇒ (? q)
    | VCons o hd tl ⇒ hd ::: (append A o m tl q)
    ].
    # H
    assumption
qed.
    
notation "hvbox(l break @@ r)"
  right associative with precedence 47
  for @{ 'vappend $l $r }.
    
interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2).


lemma vsplit_ok:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v: Vector A (m + n).
  ∀upper: Vector A m.
  ∀lower: Vector A n.
    〈upper, lower〉 = vsplit A m n v →
      upper @@ lower = v.
  #A #m #n #v #upper #lower
  cases daemon
qed.

lemma vector_append_zero:
  ∀A,m.
  ∀v: Vector A m.
  ∀q: Vector A 0.
    v = q@@v.
  #A #m #v #q
  >(Vector_O A q) %
qed.

lemma vector_cons_empty:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
    [[ ]] @@ v = v.
  #A #n #v
  cases v try %
  #n' #hd #tl %
qed.

lemma vector_cons_append:
  ∀A: Type[0].
  ∀n: nat.
  ∀e: A.
  ∀v: Vector A n.
    e ::: v = [[ e ]] @@ v.
  #A #n #e #v
  cases v try %
  #n' #hd #tl %
qed.

lemma vector_cons_append2:
  ∀A: Type[0].
  ∀n, m: nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀hd: A.
    hd:::(v@@q) = (hd:::v)@@q.
  #A #n #m #v #q
  elim v try (#hd %)
  #n' #hd' #tl' #ih #hd'
  <ih %
qed.

lemma vector_append_empty : ∀A,n.∀v : Vector A n.v @@ [[ ]] ≃ v.
#A #n #v elim v -n [%]
#n #hd #tl change with (?→?:::(?@@?)≃?)
lapply (tl@@[[ ]])
<plus_n_O #v #EQ >EQ %
qed.

lemma vector_associative_append:
  ∀A: Type[0].
  ∀n, m, o:  nat.
  ∀v: Vector A n.
  ∀q: Vector A m.
  ∀r: Vector A o.
    (v @@ q) @@ r ≃ v @@ (q @@ r).
  #A #n #m #o #v #q #r
  elim v try %
  #n' #hd #tl #ih
  <(vector_cons_append2 A … hd)
  @jmeq_cons_vector_monotone
  try assumption
  @associative_plus
qed.

lemma tail_head:
  ∀a: Type[0].
  ∀m, n: nat.
  ∀hd: a.
  ∀l: Vector a m.
  ∀r: Vector a n.
    tail a ? (hd:::(l@@r)) = l@@r.
  #a #m #n #hd #l #r
  cases l try %
  #m' #hd' #tl' %
qed.

lemma head_head':
  ∀a: Type[0].
  ∀m: nat.
  ∀hd: a.
  ∀l: Vector a m.
    hd = head' … (hd:::l).
  #a #m #hd #l cases l try %
  #m' #hd' #tl %
qed.

axiom vsplit_elim':
  ∀A: Type[0].
  ∀B: Type[1].
  ∀l, m, v.
  ∀T: Vector A l → Vector A m → B.
  ∀P: B → Prop.
    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt).

axiom vsplit_elim'':
  ∀A: Type[0].
  ∀B,B': Type[1].
  ∀l, m, v.
  ∀T: Vector A l → Vector A m → B.
  ∀T': Vector A l → Vector A m → B'.
  ∀P: B → B' → Prop.
    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
      P (let 〈lft, rgt〉 ≝ vsplit A l m v in T lft rgt)
        (let 〈lft, rgt〉 ≝ vsplit A l m v in T' lft rgt).

lemma vsplit_succ:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd: A.
    v = l@@r → (〈l, r〉 = vsplit A m n v → 〈hd:::l, r〉 = vsplit A (S m) n (hd:::v)).
  #A #m
  elim m
  [1:
    #n #l #r #v #hd #eq #hyp
    destruct >(Vector_O … l) %
  |2:
    #m' #inductive_hypothesis #n #l #r #v #hd #equal #hyp
    destruct
    cases (Vector_Sn … l) #hd' #tl'
    whd in ⊢ (???%);
    >tail_head
    <(? : vsplit A (S m') n (l@@r) = vsplit' A (S m') n (l@@r))
    try (<hyp <head_head' %)
    elim l normalize //
  ]
qed.

corollary prod_vector_zero_eq_left:
  ∀A, n.
  ∀q: Vector A O.
  ∀r: Vector A n.
    〈q, r〉 = 〈[[ ]], r〉.
  #A #n #q #r
  generalize in match (Vector_O A q …);
  #hyp destruct %
qed.

lemma vsplit_prod:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = vsplit A m n p.
  #A #m elim m
  [1:
    #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @vsplit_zero
  |2:
    #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v) #hd #exists
    cases exists #tl #jmeq
    >jmeq @vsplit_succ try %
    @ih %
  ]
qed.

definition vsplit_elim:
  ∀A: Type[0].
  ∀l, m: nat.
  ∀v: Vector A (l + m).
  ∀P: (Vector A l) × (Vector A m) → Prop.
    (∀vl: Vector A l.
     ∀vm: Vector A m.
      v = vl@@vm → P 〈vl,vm〉) → P (vsplit A l m v) ≝
  λa: Type[0].
  λl, m: nat.
  λv: Vector a (l + m).
  λP. ?.
  cases daemon
qed.

axiom vsplit_append:
  ∀A: Type[0].
  ∀m, n: nat.
  ∀v, v': Vector A m.
  ∀q, q': Vector A n.
    let 〈v', q'〉 ≝ vsplit A m n (v@@q) in
      v = v' ∧ q = q'.

lemma vsplit_vector_singleton:
  ∀A: Type[0].
  ∀n: nat.
  ∀v: Vector A (S n).
  ∀rest: Vector A n.
  ∀s: Vector A 1.
    v = s @@ rest →
    ((get_index_v A ? v 0 ?) ::: rest) = v.
  [1:
    #A #n #v cases daemon (* XXX: !!! *)
  |2:
    @le_S_S @le_O_n
  ]
qed.

let rec scan_left (A: Type[0]) (B: Type[0]) (n: nat)
                   (f: A → B → A) (a: A) (v: Vector B n) on v ≝
  a :::
    (match v with
       [ VEmpty ⇒ VEmpty A
       | VCons o hd tl ⇒ scan_left A B o f (f a hd) tl
       ]).

let rec scan_right (A: Type[0]) (B: Type[0]) (n: nat)
                    (f: A → B → A) (b: B) (v: Vector A n) on v ≝
  match v with
    [ VEmpty ⇒ ?
    | VCons o hd tl ⇒ f hd b :: (scan_right A B o f b tl)
    ].
    //
qed.

lemma v_invert_append : ∀A,n,m.∀v,v' : Vector A n.∀u,u' : Vector A m.
  v @@ u = v' @@ u' → v = v' ∧ u = u'.
#A #n #m #v elim v -n
[ #v' >(Vector_O ? v') #u #u' normalize #EQ %{EQ} %
| #n #hd #tl #IH #v' elim (Vector_Sn ?? v') #hd' * #tl' #EQv' >EQv' -v'
  #u #u' normalize #EQ destruct(EQ) elim (IH … e0) #EQ' #EQ'' %{EQ''}
  >EQ' %
]
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Other manipulations.                                                       *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* At some points matita will attempt to reduce reverse with a known vector,
   which reduces the equality proof for the cast.  Normalising this proof needs
   to be fast enough to keep matita usable, so use plus_n_Sm_fast. *)

let rec revapp (A: Type[0]) (n: nat) (m:nat)
                (v: Vector A n) (acc: Vector A m) on v : Vector A (n + m) ≝
  match v return λn'.λ_. Vector A (n' + m) with
    [ VEmpty ⇒ acc
    | VCons o hd tl ⇒ (revapp ??? tl (hd:::acc))⌈Vector A (o+S m) ↦ Vector A (S o + m)⌉
    ].
< plus_n_Sm_fast @refl qed.

let rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v : Vector A n ≝
  (revapp A n 0 v [[ ]])⌈Vector A (n+0) ↦ Vector A n⌉.
< plus_n_O @refl qed.

let rec pad_vector (A:Type[0]) (a:A) (n,m:nat) (v:Vector A m) on n : Vector A (n+m) ≝
match n return λn.Vector A (n+m) with
[ O ⇒ v
| S n' ⇒ a:::(pad_vector A a n' m v)
].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Conversions to and from lists.                                             *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

let rec list_of_vector (A: Type[0]) (n: nat)
                        (v: Vector A n) on v ≝
  match v return λn.λv. list A with
    [ VEmpty ⇒ []
    | VCons o hd tl ⇒ hd :: (list_of_vector A o tl)
    ].

let rec vector_of_list (A: Type[0]) (l: list A) on l ≝
  match l return λl. Vector A (length A l) with
    [ nil ⇒ ?
    | cons hd tl ⇒ hd ::: (vector_of_list A tl)
    ].
    normalize
    @ VEmpty
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)   
(* Rotates and shifts.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
let rec rotate_left (A: Type[0]) (n: nat)
                     (m: nat) (v: Vector A n) on m: Vector A n ≝
  match m with
    [ O ⇒ v
    | S o ⇒
        match v with
          [ VEmpty ⇒ [[ ]]
          | VCons p hd tl ⇒
             rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉)
          ]
    ].
  /2/
qed.

definition rotate_right ≝
  λA: Type[0].
  λn, m: nat.
  λv: Vector A n.
    reverse A n (rotate_left A n m (reverse A n v)).

definition shift_left_1 ≝
  λA: Type[0].
  λn: nat.
  λv: Vector A (S n).
  λa: A.
   match v return λy.λ_. y = S n → Vector A y with
     [ VEmpty ⇒ λH.⊥
     | VCons o hd tl ⇒ λH.reverse … (a::: reverse … tl)
     ] (refl ? (S n)).
 destruct.
qed.


(* XXX this is horrible - but useful to ensure that we can normalise in the proof assistant. *)
definition switch_bv_plus : ∀A:Type[0]. ∀n,m. Vector A (n+m) → Vector A (m+n) ≝
λA,n,m. match commutative_plus_faster n m return λx.λ_.Vector A (n+m) → Vector A x with [ refl ⇒ λi.i ].

definition shift_right_1 ≝
  λA: Type[0].
  λn: nat.
  λv: Vector A (S n).
  λa: A.
    let 〈v',dropped〉 ≝ vsplit ? n 1 (switch_bv_plus ? 1 n v) in a:::v'.
(*    reverse … (shift_left_1 … (reverse … v) a).*)

definition shift_left : ∀A:Type[0]. ∀n,m:nat. Vector A n → A → Vector A n ≝
  λA: Type[0].
  λn, m: nat.
    match nat_compare n m return λx,y.λ_. Vector A x → A → Vector A x with
    [ nat_lt _ _ ⇒ λv,a. replicate … a
    | nat_eq _   ⇒ λv,a. replicate … a
    | nat_gt d m ⇒ λv,a. let 〈v0,v'〉 ≝ vsplit … v in switch_bv_plus … (v' @@ (replicate … a))
    ].

(*    iterate … (λx. shift_left_1 … x a) v m.*)
    
definition shift_right ≝
  λA: Type[0].
  λn, m: nat.
  λv: Vector A (S n).
  λa: A.
    iterate … (λx. shift_right_1 … x a) v m.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Decidable equality.                                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

let rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝
  (match b return λx.λ_. Vector A x → bool with
   [ VEmpty ⇒ λc.
       match c return λx.λ_. match x return λ_.Type[0] with [ O ⇒ bool | _ ⇒ True ] with
       [ VEmpty ⇒ true
       | VCons p hd tl ⇒ I
       ]
   | VCons m hd tl ⇒ λc. andb (f hd (head' A m c)) (eq_v A m f tl (tail A m c))
   ]
  ) c.

lemma vector_inv_n: ∀A,n. ∀P:Vector A n → Type[0]. ∀v:Vector A n.
  match n return λn'. (Vector A n' → Type[0]) → Vector A n' → Type[0] with
  [ O ⇒ λP.λv.P [[ ]] → P v
  | S m ⇒ λP.λv.(∀h,t. P (VCons A m h t)) → P v
  ] P v.
#A #n #P #v lapply P cases v normalize //
qed.

lemma eq_v_elim: ∀P:bool → Type[0]. ∀A,f.
  (∀Q:bool → Type[0]. ∀a,b. (a = b → Q true) → (a ≠ b → Q false) → Q (f a b)) →
  ∀n,x,y.
  (x = y → P true) →
  (x ≠ y → P false) →
  P (eq_v A n f x y).
#P #A #f #f_elim #n #x elim x
[ #y @(vector_inv_n … y)
  normalize /2/
| #m #h #t #IH #y @(vector_inv_n … y)
  #h' #t' #Ht #Hf whd in ⊢ (?%);
  @(f_elim ? h h') #Eh
  [ @IH [ #Et @Ht >Eh >Et @refl | #NEt @Hf % #E' destruct (E') elim NEt /2/ ]
  | @Hf % #E' destruct (E') elim Eh /2/
  ]
] qed.

lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
#A #f #f_true #n #v elim v
[ //
| #m #h #t #IH whd in ⊢ (??%%); >f_true >IH @refl
] qed.

lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
#A #n #h #t #t' * #NE % #E @NE >E @refl
qed.

lemma  eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
#A #f #f_true #n elim n
[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE; /2/
] qed.

lemma eq_v_append : ∀A,n,m,test,v1,v2,u1,u2.
  eq_v A (n+m) test (v1@@u1) (v2@@u2) =
  (eq_v A n test v1 v2 ∧ eq_v A m test u1 u2).
#A #n #m #test #v1 lapply m -m elim v1 -n
[ #m #v2 >(Vector_O … v2) #u1 #u2 % ]
#n #hd #tl #IH #m #v2
elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
#u1 #u2 whd in ⊢ (??%(?%?));
whd in match (head' ???);
whd in match (tail ???);
whd in match (tail ???);
elim (test ??) normalize nodelta [ @IH | % ]
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Subvectors.                                                                *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 

definition mem ≝
 λA: Type[0].
 λeq_a : A → A → bool.
 λn: nat.
 λl: Vector A n.
 λx: A.
  fold_right … (λy,v. (eq_a x y) ∨ v) false l.

lemma mem_append: ∀A,eq_a. (∀x. eq_a x x = true) → ∀n,m.∀v: Vector A n. ∀w: Vector A m. ∀x. mem A eq_a … (v@@x:::w) x.
 #A #eq_a #refl #n #m #v elim v
 [ #w #x whd whd in match (mem ?????); >refl //
 | /2/
 ]
qed.

lemma mem_monotonic_wrt_append:
  ∀A: Type[0].
  ∀m, o: nat.
  ∀eq: A → A → bool.
  ∀reflex: ∀a. eq a a = true.
  ∀p: Vector A m.
  ∀a: A.
  ∀r: Vector A o.
    mem A eq ? r a = true → mem A eq ? (p @@ r) a = true.
  #A #m #o #eq #reflex #p #a
  elim p try (#r #assm assumption)
  #m' #hd #tl #inductive_hypothesis #r #assm
  normalize
  cases (eq ??) try %
  @inductive_hypothesis assumption
qed.


let rec subvector_with
  (a: Type[0]) (n: nat) (m: nat) (eq: a → a → bool) (sub: Vector a n) (sup: Vector a m)
    on sub: bool ≝
  match sub with
  [ VEmpty         ⇒ true
  | VCons n' hd tl ⇒
    if mem … eq … sup hd then
      subvector_with … eq tl sup
    else
      false
  ].

lemma subvector_with_refl0:
 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
  ∀m. ∀w: Vector A m. subvector_with A … eq v (w@@v).
 #A #n #eq #refl #v elim v
 [ //
 | #m #hd #tl #IH #m #w whd in match (subvector_with ??????); >mem_append //
   change with (bool_to_Prop (subvector_with ??????)) lapply (IH … (w@@[[hd]]))
  lapply (vector_associative_append ???? w [[hd]] tl) #EQ
  @(dependent_rewrite_vectors … EQ) //
 ]
qed.

lemma subvector_with_refl:
 ∀A:Type[0]. ∀n. ∀eq: A → A → bool. (∀a. eq a a = true) → ∀v: Vector A n.
  subvector_with A … eq v v.
 #A #n #eq #refl #v @(subvector_with_refl0 … v … [[]]) //
qed.

lemma subvector_multiple_append:
  ∀A: Type[0].
  ∀o, n: nat.
  ∀eq: A → A → bool.
  ∀refl: ∀a. eq a a = true.
  ∀h: Vector A o.
  ∀v: Vector A n.
  ∀m: nat.
  ∀q: Vector A m.
    bool_to_Prop (subvector_with A ? ? eq v (h @@ q @@ v)).
  #A #o #n #eq #reflex #h #v
  elim v try (normalize #m #irrelevant @I)
  #m' #hd #tl #inductive_hypothesis #m #q
  change with (bool_to_Prop (andb ??))
  cut ((mem A eq (o + (m + S m')) (h@@q@@hd:::tl) hd) = true)
  [1:
    @mem_monotonic_wrt_append try assumption
    @mem_monotonic_wrt_append try assumption
    normalize >reflex %
  |2:
    #assm >assm
    >vector_cons_append
    change with (bool_to_Prop (subvector_with ??????))
    @(dependent_rewrite_vectors … (vector_associative_append … q [[hd]] tl))
    try @associative_plus
    @inductive_hypothesis
  ]
qed.



(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    
    
lemma map_fusion:
  ∀A, B, C: Type[0].
  ∀n: nat.
  ∀v: Vector A n.
  ∀f: A → B.
  ∀g: B → C.
    map B C n g (map A B n f v) = map A C n (λx. g (f x)) v.
  #A #B #C #n #v #f #g
  elim v
  [ normalize
    %
  | #N #H #V #H2
    normalize
    > H2
    %
  ]
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Vector prefix and suffix relations.                                        *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    

(* n.b.: if n = m this is equivalent to equality, without n and m needing to be
   Leibniz-equal *)
let rec vprefix A n m (test : A → A → bool) (v1 : Vector A n) (v2 : Vector A m) on v1 : bool ≝
match v1 with
[ VEmpty ⇒ true
| VCons n' hd1 tl1 ⇒
  match v2 with
  [ VEmpty ⇒ false
  | VCons m' hd2 tl2 ⇒ test hd1 hd2 ∧ vprefix … test tl1 tl2
  ]
].

let rec vsuffix A n m test (v1 : Vector A n) (v2 : Vector A m) on v2 : bool ≝
If leb (S n) m then with prf do
  match v2 return λm.λv2:Vector A m.leb (S n) m → bool with
  [ VEmpty ⇒ Ⓧ
  | VCons m' hd2 tl2 ⇒ λ_.vsuffix ?? m' test v1 tl2
  ] prf
else (if eqb n m then
  vprefix A n m test v1 v2
else
  false).

include alias "arithmetics/nat.ma".

lemma prefix_to_le : ∀A,n,m,test,v1,v2.
  vprefix A n m test v1 v2 → n ≤ m.
#A #n #m #test #v1 lapply m -m elim v1 -n [//]
#n #hd #tl #IH #m * -m [*]
#m #hd' #tl'
whd in ⊢ (?%→?);
elim (test ??) [2: *]
whd in ⊢ (?%→?);
#H @le_S_S @(IH … H)
qed.

lemma vprefix_ok : ∀A,n,m,test,v1,v2.
  vprefix A n m test v1 v2 → le n m ∧
  ∃pre.∃post : Vector A (m - n).v2 ≃ pre @@ post ∧
            bool_to_Prop (eq_v … test v1 pre).
#A #n #m #test #v1 #v2 #G %{(prefix_to_le … G)}
lapply G lapply v2 lapply m -m elim v1 -n
[ #m #v2 * <minus_n_O %{[[ ]]} %{v2} % % ]
#n #hd1 #tl1 #IH #m * -m [*]
#m #hd2 #tl2 whd in ⊢ (?%→?);
elim (true_or_false_Prop (test hd1 hd2)) #H >H normalize nodelta [2: *]
#G elim (IH … G) #pre * #post * #EQ #EQ'
%{(hd2:::pre)} %{post} %
[ change with (?≃hd2 ::: (? @@ ?)) lapply EQ lapply (pre @@ post)
  <(minus_to_plus m … (prefix_to_le … G) (refl …))
  #V #EQ'' >EQ'' %
| whd in ⊢ (?%);
  whd in match (head' ???); >H
  @EQ'
]
qed.

lemma vprefix_to_eq : ∀A,n,test,v1,v2.
  vprefix A n n test v1 v2 = eq_v … test v1 v2.
#A #n #test #v1 elim v1 -n
[ #v2 >(Vector_O … v2) %
| #n #hd1 #tl1 #IH
  #v2 elim (Vector_Sn … v2) #hd2 * #tl2 #EQ destruct(EQ)
  normalize elim (test ??) [2: %]
  normalize @IH
]
qed.

lemma vprefix_true : ∀A,n,m,test.∀v1,pre : Vector A n.∀post : Vector A m.
  eq_v … test v1 pre → bool_to_Prop (vprefix … test v1 (pre @@ post)).
#A #n #m #test #v1 lapply m -m elim v1 -n
[ #m #pre #post #_ %
| #n #hd #tl #IH #m #pre elim (Vector_Sn … pre) #hd' * #tl' #EQpre >EQpre
  #post
  whd in ⊢ (?%→?%); whd in match (head' ???);
  elim (test hd hd') [2: *] normalize nodelta whd in match (tail ???);
  @IH
]
qed.

lemma vsuffix_to_le : ∀A,n,m,test,v1,v2.
  vsuffix A n m test v1 v2 → n ≤ m.
#A #n #m #test #v1 #v2 lapply v1 lapply n -n elim v2 -m
[ #n * -n
  [ * %
  | #n #hd #tl *
  ]
| #m #hd2 #tl2 #IH
  #n #v1 change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
  @If_elim normalize nodelta @leb_elim #H *
  [ #_ @(transitive_le … H) %2 %1
  | #ABS elim (ABS I)
  | #_ @eqb_elim #G normalize nodelta [2: *]
    destruct #_ %
  ]
]
qed.
  
lemma vsuffix_ok : ∀A,n,m,test,v1,v2.
  vsuffix A n m test v1 v2 → le n m ∧
  ∃pre : Vector A (m - n).∃post.v2 ≃ pre @@ post ∧
            bool_to_Prop (eq_v … test v1 post).
#A #n #m #test #v1 #v2 #G %{(vsuffix_to_le … G)}
lapply G lapply v1 lapply n -n
elim v2 -m
[ #n #v1
  whd in ⊢ (?%→?);
  @eqb_elim #EQ1 [2: *]
  normalize nodelta lapply v1 -v1 >EQ1 #v1
  >(Vector_O … v1) * %{[[ ]]} %{[[ ]]} % %
| #m #hd2 #tl2 #IH #n #v1
  change with (bool_to_Prop (If ? then with prf do ? else ?) → ?)
  @If_elim normalize nodelta #H
  [ #G elim (IH … G) #pre * #post * #EQ1 #EQ2
    >minus_Sn_m
    [ %{(hd2:::pre)} %{post} %{EQ2}
      change with (?≃?:::(?@@?))
      lapply EQ1 lapply (pre@@post)
      <plus_minus_m_m
      [ #v #EQ >EQ %]
    ]
    @(vsuffix_to_le … G)
  | @eqb_elim #EQn [2: *] normalize nodelta
    generalize in match (hd2:::tl2);
    <EQn in ⊢ (%→%→??(λ_.??(λ_.?(?%%??)?)));
    #v2' >vprefix_to_eq #G
    <EQn in ⊢ (?%(λ_:%.??(λ_.?(???%%)?)));
    <minus_n_n %{[[ ]]} %{v2'} %{G}
    %
  ]
]
qed.

lemma vsuffix_true : ∀A,n,m,test.∀pre : Vector A n.∀v1,post : Vector A m.
  eq_v … test v1 post → bool_to_Prop (vsuffix … test v1 (pre @@ post)).
#A #n #m #test #pre lapply m -m elim pre -n
[ #m #v1 #post lapply v1 -v1 cases post -m
  [ #v1 >(Vector_O … v1) * %
  | #m #hd #tl #v1 #G
    change with (bool_to_Prop (If ? then with prf do ? else ?))
    @If_elim normalize nodelta 
    [ @leb_elim #H * @⊥ @(absurd ? H ?) normalize // ]
    #_ >eqb_n_n normalize nodelta
    >vprefix_to_eq assumption
  ]
| #n #hd2 #tl2 #IH
  #m #v1 #post #G
  change with (bool_to_Prop (If ? then with prf do ? else ?))
  @If_elim normalize nodelta
  [ #H @IH @G
  | @leb_elim [ #_ * #ABS elim (ABS I) ]
    #H #_ @eqb_elim #K
    [ @⊥ @(absurd ? K) @lt_to_not_eq // ]
    normalize elim H -H #H @H normalize
    >plus_n_Sm_fast //
  ]
]
qed.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Vector flattening and recursive splitting.                                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)    

let rec rvsplit A n m on n : Vector A (n * m) → Vector (Vector A m) n ≝
match n return λn.Vector ? (n * m) → Vector (Vector ? m) n with
[ O ⇒ λ_.VEmpty ?
| S k ⇒
  λv.let 〈pre,post〉 ≝ vsplit … m (k*m) v in
  pre ::: rvsplit … post
].

let rec vflatten A n m (v : Vector (Vector A m) n) on v : Vector A (n * m) ≝
match v return λn.λ_ : Vector ? n.Vector ? (n * m) with
[ VEmpty ⇒ VEmpty ?
| VCons n' hd tl ⇒ hd @@ vflatten ? n' m tl
].

lemma vflatten_rvsplit : ∀A,n,m,v.vflatten A n m (rvsplit A n m v) = v.
#A #n elim n -n
[ #m #v >(Vector_O ? v) %
| #n #IH #m #v
  whd in match (rvsplit ????);
  @vsplit_elim #pre #post #EQ
  normalize nodelta
  whd in match (vflatten ????); >IH >EQ %
]
qed.

lemma rvsplit_vflatten : ∀A,n,m,v.rvsplit A n m (vflatten A n m v) = v.
#A #n #m #v elim v -n
[ %
| #n #hd #tl #IH
  whd in match (vflatten ????);
  whd in match (rvsplit ????);
  @vsplit_elim #pre #post #EQ
  elim (v_invert_append … EQ) #EQ1 #EQ2 <EQ1 <EQ2
  normalize nodelta >IH %
]
qed.

(* Paolo: should'nt it be in the standard library? *)
lemma sym_jmeq : ∀A,B.∀a : A.∀b : B.a≃b → b≃a.
#A #B #a #b * % qed.

lemma vflatten_append : ∀A,n,m,p,v1,v2.
  vflatten A (n+m) p (v1 @@ v2) ≃ vflatten A n p v1 @@ vflatten A m p v2.
#A #n #m #p #v1 lapply m -m elim v1
[ #m #v2 %
| #n #hd1 #tl1 #IH #m #v2
  whd in ⊢ (??%?(????%?));
  lapply (IH … v2)
  lapply (vflatten … (tl1@@v2))
  cut ((n+m)*p = n*p + m*p)
  [ // ] #EQ whd in match (S n + m); whd in match (S ? * ?);
  whd in match (S n * ?); >EQ in ⊢ (%→?%%??→?%%??); -EQ
  #V #EQ >EQ -V @sym_jmeq @vector_associative_append
]
qed.

lemma eq_v_vflatten : ∀A,n,m,test,v1,v2.
  eq_v A ? test (vflatten A n m v1) (vflatten A n m v2) =
  eq_v ?? (eq_v … test) v1 v2.
#A #n #m #test #v1 elim v1 -n
[ #v2 >(Vector_O … v2) % ]
#n #hd #tl #IH #v2
elim (Vector_Sn … v2) #hd' * #tl' #EQ >EQ -v2
whd in ⊢ (??(????%%)%);
whd in match (head' ???);
whd in match (tail ???);
>eq_v_append >IH %
qed.

lemma vprefix_vflatten : ∀A,n,m,p,test.∀v1,v2.
  vprefix ? n m (eq_v ? p test) v1 v2 →
  bool_to_Prop (vprefix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
#A #n #m #p #test #v1 #v2 #G
elim (vprefix_ok … G) #le_nm
* #pre * #post *
lapply (vflatten_append … pre post)
lapply (pre @@ post)
<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
lapply (vflatten A m p v2')
cut (m*p = n*p + (m-n)*p)
[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
  <distributive_times_plus <(minus_to_plus … le_nm (refl …)) % ]
#EQ >EQ #v2' #EQ' >EQ' -v2' -v2'
#G @vprefix_true
>eq_v_vflatten @G
qed.

lemma vsuffix_vflatten : ∀A,n,m,p,test.∀v1,v2.
  vsuffix ? n m (eq_v ? p test) v1 v2 →
  bool_to_Prop (vsuffix A (n*p) (m*p) test (vflatten … v1) (vflatten … v2)).
#A #n #m #p #test #v1 #v2 #G
elim (vsuffix_ok … G) #le_nm * #pre * #post * 
lapply (vflatten_append … pre post)
lapply (pre @@ post)
>commutative_plus in ⊢ (%→?%%??→???%%→?);
<(minus_to_plus … le_nm (refl …)) in ⊢ (%→?%%??→???%%→?);
#v2' #EQ1 #EQ2 >EQ2 -v2 lapply EQ1 -EQ1
lapply (vflatten A m p v2')
cut (m*p = (m-n)*p + n*p)
[ <(commutative_times p) <(commutative_times p) <(commutative_times p)
  <distributive_times_plus <commutative_plus <(minus_to_plus … le_nm (refl …)) % ]
#EQ >EQ #v2' #EQ' >EQ'
#G @vsuffix_true
>eq_v_vflatten @G
qed.