splitAt equality in Agda

Question

How can someone prove this equality

≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
         -> (xs₁ : Vec A l₁)
         -> (xs₂ : Vec A l₂)
         -> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)

? The base case is obvious

≡splitAt  []       xs₂ = refl

But then

≡splitAt (x ∷ xs₁) xs₂

gives

Goal: (x ∷ xs₁ , xs₂ , refl) ≡
      (splitAt (suc .n) (x ∷ xs₁ ++ xs₂)
       | splitAt .n (xs₁ ++ xs₂))

This

≡splitAt (x ∷ xs₁) xs₂ with ≡splitAt xs₁ xs₂
... | refl = {!!}

throws an error: "Refuse to solve heterogeneous constraint refl...".

And this

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

throws an error: "xs₁ != xs₁' of type Vec A l₁...". I wrote this definition:

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

but don't know, how to use it.

Maybe there is some source, from where i can learn more about with-expressions?

Thanks.

Jesper Jesper · Accepted Answer · 2014-02-02T10:32:25

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).

splitAt equality in Agda

1 Answers