`take n (take n xs) ≡ take n xs` for `Vec` in Agda

I want to prove a nearly trivial property of the take function for Vec in Agda.

open import Data.Vec
open import Data.Nat
open import Relation.Binary.PropositionalEquality

take-idempotent : ∀ n (xs : Vec ℕ n) → take n (take n xs) ≡ take n xs
take-idempotent n xs = ?

My problem stems from the fact that the type index of take consists of the addition of natural numbers. Agda outputs the following message to the above code.

n != n + _n_9 of type ℕ
when checking that the inferred type of an application
  Vec _A_8 n
matches the expected type
  Vec _A_8 (n + _n_9)

I could make xs to have a type like Vec ℕ (n + 0) and apply take once, but the type of the outcome will be Vec ℕ n. To apply take twice, I need to set the type of xs to be Vec ℕ (n + 0 + 0) and use take (n + 0) for the first application. In addition, I would need + 0 adjustments to pass lhs and rhs to _≡_, since these have different numbers of applications of take.

Is there a simple way to state and prove this proposition?

Solution 1:

This might be a harder problem than it seems. Another deceptive example: reversing a vector twice yields the original vector. How hard can it be to prove? It's easy to prove for lists, right? Turns out that it is pretty hard. See the recent contribution to Agda's standard library: https://github.com/agda/agda-stdlib/issues/942

In my (very limited) experience, something that's easy to prove with pencil and paper can be more challenging to prove in Agda because of technicalities like the ones at hand. It's important to develop an intuition on what's hard to prove in Agda and what isn't and structure your propositions around that. I think that this isn't emphasized enough.

That said, here are a few things that have helped me in the past to navigate issues with types that have different indices:

• subst - which seems to be a controversial choice. You can easily end up in subst hell, where you can't see your proof for all the substs.
• Pointwise equality of vectors, i.e., a proof that each element of one vector matches the corresponding element of the other vector. The nice thing is that pointwise equality (unlike propositional equality) can be stated between, say, a vector of size n and a vector of size n + 0.

To be more concrete:

open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Vec
open import Data.Vec.Relation.Binary.Pointwise.Inductive as PI
open import Relation.Binary.PropositionalEquality as PE

take-all₁ : ∀ n → (xs : Vec ℕ n) → (xs′ : Vec ℕ (n + 0)) → Pointwise _≡_ xs xs′ →
  take n xs′ ≡ xs
take-all₁ n xs xs′ p = {!!}

take-all₂ : ∀ n (xs : Vec ℕ n) → take n (subst (Vec ℕ) (PE.sym (+-identityʳ n)) xs) ≡ xs
take-all₂ n xs = {!!}

use₁ : (xs : Vec ℕ 3) → take 3 xs ≡ xs
use₁ xs = take-all₁ 3 xs xs (PI.refl PE.refl)

use₂ : (xs : Vec ℕ 3) → take 3 xs ≡ xs
use₂ = take-all₂ 3

Note that in use₁ and use₂ all the subst and pointwise nastiness goes away, because 3 and 3 + 0 both reduce to 3. (Unlike n and n + 0.)

What also worked for me in the past is passing two indices (say, i and k) to a proof, along with p : i ≡ k. Then pretend that i and k are unrelated for most of the proof and only use p where needed. But this doesn't seem to apply here.

There's also the concept of heterogeneous equality that seems to act as a replacement for propositional equality, but which allows for different indices. I haven't yet explored that.