Lang.vectByIndAppend

import Natural (+, plusZeroId, plusSucId, zeroPlusId, sucPlus, plusAssoc)
import Lang.vectByInd (vect)

vappend : (n : ℕ) {A : 𝕌} (m : ℕ) → vect n A → vect m A → vect (n + m) A
  using (Natural.+.unfold, sucPlus.rw, vect.eq, Lang.vectByInd.vect.unfold, zeroPlusId.rw)
vappend = λn A m. ℕ-elim (λv w. w) (k ih. λv w. v .π₁, ih (v .π₂) w) n

-- This equation holds by direct computation
vappendZ : (A : 𝕌) (n : ℕ) (v : vect Z A) (w : vect n A) → vappend _ _ v w ≡ w ∈ vect n A
  using (hyp.rw,
    sucPlus.rw,
    vappend.eq,
    vect.eq,
    Lang.vectByInd.vect.unfold,
    zeroPlusId,
    zeroPlusId.rw)
vappendZ = λA n v w. ⋆

--  ^^^^^^^^^ FIXME: Can't be synthesised
vappendS : (n : ℕ)
  (A : 𝕌)
  (m : ℕ)
  (v : vect (S n) A)
  (w : vect m A)
  → vappend _ _ v w ≡ (v .π₁, vappend _ _ (v .π₂) w)
  using (hyp.rw,
    Natural.+.unfold,
    sucPlus,
    sucPlus.rw,
    vappend.eq,
    vect.eq,
    Lang.vectByInd.vect.unfold,
    zeroPlusId.rw)
vappendS = λn A m v w. ⋆

-- the associativity step case, packaged: with the tail instance of
-- the induction hypothesis supplied as an equation, both sides
-- compute (sucPlus + one vappend unfolding each) to cons cells whose
-- tails the hypothesis relates
vappendAssocS : {A : 𝕌}
  {m k p : ℕ}
  {v : vect m A}
  {w : vect k A}
  {q : vect (S p) A}
  → (vappend (p + m) k (vappend _ _ (q .π₂) v) w
    ≡ vappend _ _ (q .π₂) (vappend _ _ v w)
    ∈ vect (p + (m + k)) A)
    → vappend (S p + m) k (vappend _ _ q v) w
      ≡ vappend _ _ q (vappend _ _ v w)
      ∈ vect (S p + (m + k)) A
  using (hyp.rw,
    Natural.+.unfold,
    plusAssoc.rw,
    sucPlus.rw,
    vappend.eq,
    vect.eq,
    Lang.vectByInd.vect.unfold,
    zeroPlusId.rw)
vappendAssocS = λA m k p v w q hih. ⋆

-- Associativity: the statement itself only type-checks up to
-- plus-associativity (the two sides' lengths differ intensionally)
-- — the extensional mismatch the imported plus lemmas discharge.
--  ^^^^^^^^^^^^^ FIXME: Can't be synthesised
vappendAssoc : (n : ℕ)
  (A : 𝕌)
  (m k : ℕ)
  (v : vect m A)
  (w : vect k A)
  (u : vect n A)
  → vappend _ _ (vappend _ _ u v) w ≡ vappend n (m + k) u (vappend _ _ v w)
  using (hyp.rw,
    Natural.+.unfold,
    plusAssoc,
    plusAssoc.rw,
    sucPlus,
    sucPlus.rw,
    vappendS.rw,
    vappendZ.rw,
    vect.eq,
    Lang.vectByInd.vect.unfold,
    zeroPlusId,
    zeroPlusId.rw)
vappendAssoc =
  λn A m k v w u. ℕ-elim
    p. (q : vect p A)
      → vappend (p + m) k (vappend _ _ q v) w
        ≡ vappend _ _ q (vappend _ _ v w)
        ∈ vect (p + (m + k)) A
    λq. ⋆ using (vappend.eq, vect.eq, zeroPlusId.rw, sucPlus.rw, hyp.rw)
    p ih. λq. vappendAssocS (ih (q .π₂))
    n
    u