vec.v

Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Fixpoint vec (n : nat) (A : Type) : Type :=
  if n is n'.+1 then A * vec n' A else unit.

Fixpoint vcat (n m : nat) (A : Type) : vec n A -> vec m A -> vec (n + m) A :=
  if n is n'.+1
  then fun '(l, ls) rs => (l, vcat ls rs)
  else fun _ rs => rs.

Fixpoint vmap (n : nat) (A B : Type) (f : A -> B) : vec n A -> vec n B :=
  if n is n'.+1
  then fun '(x, xs) => (f x, vmap f xs)
  else fun _ => tt.

Lemma v_map_cat
      (n m : nat) (A B : Type) (f : A -> B) (xs : vec n A) (ys : vec m A) :
  vmap f (vcat xs ys) = vcat (vmap f xs) (vmap f ys).
Proof. by elim: n xs ys => //= n IH [x xs] ys; rewrite -IH. Qed.

Lemma vcatA (n1 n2 n3 : nat) (A : Type)
      (s1 : vec n1 A) (s2 : vec n2 A) (s3 : vec n3 A) :
  vcat s1 (vcat s2 s3) =
  ecast n (vec n A) (esym (addnA n1 n2 n3)) (vcat (vcat s1 s2) s3).
Proof.
elim: n1 s1 => //= [_ | n1 IH [h s1]].
- by rewrite (eq_irrelevance (esym _) (erefl _)).
- rewrite IH.
  move: {IH s1 s2 s3} (vcat (vcat _ _) _) => s.
  rewrite -!/(addn _ _).
  Set Printing All.
Abort.