splitAt equality in Agda

Question

A good rule of thumb when proving something about a function defined by pattern matching (such as splitAt here) is to use the same patterns in your proof. So you're on the right track here by writing

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
...                                  | (xs₁' , xs₂' , e) = ?

Here, e has type xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'. Agda doesn't know how to solve this equation since it contains the function _++_, so you cannot replace it by refl. So we have to help Agda a little instead:

split≡ : {α : Level} {A : Set α} (l₁ : Nat) {l₂ : Nat}
       -> (xs₁ xs₁' : Vec A l₁)
       -> (xs₂ xs₂' : Vec A l₂)
       -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
       -> (xs₁ ≡ xs₁') × (xs₂ ≡ xs₂')

The case for zero is again easy:

split≡ zero [] [] xs₂ .xs₂ refl = refl , refl

In the case for suc l₁, we use cong from the standard library to split the equality proof e into an equality on the heads and one on the tails, feeding the last one into a recursive call to split≡:

split≡ (suc l₁) (x ∷ xs₁) (x' ∷ xs₁') xs₂ xs₂' e with cong head e | split≡ l₁ xs₁ xs₁' xs₂ xs₂' (cong tail e)
split≡ (suc l₁) (x ∷ xs₁) (.x ∷ .xs₁) xs₂ .xs₂ e    | refl        | refl , refl = refl , refl

Now that we have split≡, we can return to the definition of ≡splitAt:

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl = {!!}

We are almost there now: we know that xs₁ = xs₁' and xs₂ = xs₂', but not yet that e = refl. Unfortunately, pattern matching on e directly doesn't work:

xs₁ != xs₁' of type Vec A l₁
when checking that the pattern refl has type
xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'

The reason is that Agda considers patterns from left to right, but we want a different order here. Another with-pattern comes to the rescue:

≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e | e
≡splitAt {α} {A} {ℕ.suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl | refl = refl

Here is my complete code for reference:

split≡ : {α : Level} {A : Set α} (l₁ : Nat) {l₂ : Nat}
       -> (xs₁ xs₁' : Vec A l₁)
       -> (xs₂ xs₂' : Vec A l₂)
       -> xs₁ ++ xs₂ ≡ xs₁' ++ xs₂'
       -> (xs₁ ≡ xs₁') × (xs₂ ≡ xs₂')
split≡ zero [] [] xs₂ .xs₂ refl = refl , refl
split≡ (suc l₁) (x ∷ xs₁) (x' ∷ xs₁') xs₂ xs₂' e with cong head e | split≡ l₁ xs₁ xs₁' xs₂ xs₂' (cong tail e)
split≡ (suc l₁) (x ∷ xs₁) (.x ∷ .xs₁) xs₂ .xs₂ e | refl | refl , refl = refl , refl

≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
         -> (xs₁ : Vec A l₁)
         -> (xs₂ : Vec A l₂)
         -> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)
≡splitAt [] xs₂ = refl
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ with splitAt l₁ (xs₁ ++ xs₂)
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | xs₁' , xs₂' , e with split≡ l₁ xs₁ xs₁' xs₂ xs₂' e | e
≡splitAt {l₁ = suc l₁} (x ∷ xs₁) xs₂ | .xs₁ , .xs₂ , e | refl , refl | refl = refl

There might be an easier way to prove this, but this was the best I could come up with.

Concerning your question how to learn more about with-patterns, the best way to learn is by writing with-patterns yourself a lot (at least that's how I learned). Do not forget to let Agda help you in making case distinctions (by using C-c C-c in Emacs).