module Padova2025.ProvingBasics.Equality.Vectors where

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Vectors
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General

take-drop
  : {A : Set} {n : ℕ} (k : ℕ) (xs : Vector A (k + n))
  → takeV k xs ++V dropV k xs ≡ xs
take-drop = {!!}

Let xs : Vector A n, ys : Vector A m and zs : Vector A o.

Then (xs ++V ys) ++V zs is of type Vector A ((n + m) + o, whereas xs ++V (ys ++V zs) is of type Vector A (n + (m + o)).

These two types are equal, but not by definition. Hence the expression “(xs ++V ys) ++V zs ≡ xs ++V (ys ++V zs)” is ill-typed. To state the desired equality, we have three options.

1. Transport one of the two sides of the equation to the type of the other.
2. Introduce so-called heterogeneous equality.
3. Switch to Cubical Agda, where we still have to do the transporting (and heterogeneous equality does no longer work well), but where working with this transporting gets simplified.

open import Padova2025.ProvingBasics.Equality.NaturalNumbers

Method 1: Transporting one of the two sides of the equation

cons-subst
  : {A : Set} {n m : ℕ}
  → (p : n ≡ m) (x : A) (xs : Vector A n)
  → subst (Vector A) (cong succ p) (x ∷ xs) ≡ x ∷ subst (Vector A) p xs
cons-subst = {!!}

++V-assoc
  : {A : Set} {n m o : ℕ} (xs : Vector A n) (ys : Vector A m) (zs : Vector A o)
  → subst (Vector A) (+-assoc n m o) ((xs ++V ys) ++V zs) ≡ xs ++V (ys ++V zs)
++V-assoc = {!!}

Method 1’: Transporting one of the two sides, but with a twist

Method 1 becomes more pleasant by introducing a cast operation which, unlike subst, does not look at the given equality witness, as in the standard library. It also becomes more pleasant when using Cubical Agda. In both variations, there is no longer a need for cons-subst.

The trick is to not pattern match on the equality witness, but only on the dimensions and on the vectors themselves.

In the following type signature, the dot before (n ≡ m) expresses that we will not look at the value of this argument (and Agda will then forbid us from peeking).

cast
  : {A : Set} {n m : ℕ}
  → .(n ≡ m) → Vector A n → Vector A m
cast = {!!}

cast-is-id
  : {A : Set} {n : ℕ}
  → (p : n ≡ n) (xs : Vector A n)
  → cast p xs ≡ xs
cast-is-id = {!!}

++V-assoc'
  : {A : Set} {n m o : ℕ} (xs : Vector A n) (ys : Vector A m) (zs : Vector A o)
  → cast (+-assoc n m o) ((xs ++V ys) ++V zs) ≡ xs ++V (ys ++V zs)
++V-assoc' = {!!}

Method 2: Heterogeneous equality

Alternatively, we can introduce so-called heterogeneous equality. However, the iconv function presented below requires the K axiom which is incompatible with Cubical Agda. We hence only include this alternative here as a comment.

infix  _≅_
data _≅_ {A : Set} (x : A) : {B : Set} → B → Set₁ where
   refl : x ≅ x

{-
icong
  : {I : Set} (F : I → Set) {G : {k : I} → F k → Set}
  → {i j : I} {x : F i} {y : F j}
  → i ≡ j → (f : {k : I} (z : F k) → G z)
  → x ≅ y
  → f x ≅ f y
icong F refl _ refl = refl

++V-assoc''
  : {A : Set} {n m o : ℕ} (xs : Vector A n) (ys : Vector A m) (zs : Vector A o)
  → (xs ++V ys) ++V zs ≅ xs ++V (ys ++V zs)
++V-assoc''              []       ys zs = refl
++V-assoc'' {n = succ n} (x ∷ xs) ys zs = icong (Vector _) (+-assoc n _ _) (x ∷_) (++V-assoc'' xs ys zs)
-}