How to prove unfold-reverse for Vec?

Question

The Agda standard library has a few properties on how reverse and _++_ work on List. Trying to transfer these proofs to Vec appears to be non-trivial (disregarding universes):

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

unfold-reverse : {A : Set} → (x : A) → {n : ℕ} → (xs : Vec A n) →
                 reverse (x ∷ xs) ≅ reverse xs ++ [ x ]

TL;DR: How to prove unfold-reverse?

The rest of this question outlines approaches to doing so and explains what problems surface.

The type of this property is very similar to the List counter part in Data.List.Properties. The proof involves a helper which roughly translates to:

open import Function

helper : ∀ {n m} → (xs : Vec A n) → (ys : Vec A m) →
         foldl (Vec A ∘ (flip _+_ n)) (flip _∷_) xs ys ≅ reverse ys ++ xs

Trying to insert this helper in unfold-reverse fails, because the left hand reverse is a foldl application with Vec A ∘ suc as first argument whereas the left hand side of helper has a foldl application with Vec A ∘ (flip _+_ 1) as first argument. Even though suc ≗ flip _+_ 1 is readily available from Data.Nat.Properties.Simple, it cannot be used here as cong would need a non-pointwise equality here and we don't have extensionality without further assumptions.

Removing the flip from flip _+_ n in helper yields a type error, so that is no option either.

Any other ideas?

Answer 1

The Data.Vec.Properties module contains this function:

foldl-cong : ∀ {a b} {A : Set a}
               {B₁ : ℕ → Set b}
               {f₁ : ∀ {n} → B₁ n → A → B₁ (suc n)} {e₁}
               {B₂ : ℕ → Set b}
               {f₂ : ∀ {n} → B₂ n → A → B₂ (suc n)} {e₂} →
             (∀ {n x} {y₁ : B₁ n} {y₂ : B₂ n} →
                y₁ ≅ y₂ → f₁ y₁ x ≅ f₂ y₂ x) →
             e₁ ≅ e₂ →
             ∀ {n} (xs : Vec A n) →
             foldl B₁ f₁ e₁ xs ≅ foldl B₂ f₂ e₂ xs
foldl-cong           _     e₁=e₂ []       = e₁=e₂
foldl-cong {B₁ = B₁} f₁=f₂ e₁=e₂ (x ∷ xs) =
  foldl-cong {B₁ = B₁ ∘ suc} f₁=f₂ (f₁=f₂ e₁=e₂) xs

Here is more or less elaborated solution:

unfold-reverse : {A : Set} → (x : A) → {n : ℕ} → (xs : Vec A n) →
                 reverse (x ∷ xs) ≅ reverse xs ++ (x ∷ [])
unfold-reverse x xs = begin
  foldl (Vec _ ∘ _+_ 1) (flip _∷_) (x ∷ []) xs
    ≅⟨ (foldl-cong
         {B₁ = Vec _ ∘ _+_ 1}
         {f₁ = flip _∷_}
         {e₁ = x ∷ []}
         {B₂ = Vec _ ∘ flip _+_ 1}
         {f₂ = flip _∷_}
         {e₂ = x ∷ []}
         (λ {n} {a} {as₁} {as₂} as₁≅as₂ -> {!!})
         refl
         xs) ⟩
  foldl (Vec _ ∘ flip _+_ 1) (flip _∷_) (x ∷ []) xs
    ≅⟨ helper (x ∷ []) xs  ⟩
  reverse xs ++ x ∷ []
  ∎

Note, that only B₁ and B₂ are distinct in the arguments of the foldl-cong function. After simplifying context in the hole we have

Goal: a ∷ as₁ ≅ a ∷ as₂
————————————————————————————————————————————————————————————
as₁≅as₂ : as₁ ≅ as₂
as₂     : Vec A (n + 1)
as₁     : Vec A (1 + n)
a       : A
n       : ℕ
A       : Set

So we need to prove, that at each recursive call adding an element to an accumulator of type Vec A (n + 1) is equal to adding an element to an accumulator of type Vec A (1 + n), and then results of two foldls are equal. The proof itself is simple. Here is the whole code:

open import Function
open import Relation.Binary.HeterogeneousEquality
open import Data.Nat
open import Data.Vec
open import Data.Nat.Properties.Simple
open import Data.Vec.Properties

open ≅-Reasoning

postulate
  helper : ∀ {n m} {A : Set} (xs : Vec A n) (ys : Vec A m)
         -> foldl (Vec A ∘ flip _+_ n) (flip _∷_) xs ys ≅ reverse ys ++ xs

cong' : ∀ {α β γ} {I : Set α} {i j : I}
      -> (A : I -> Set β) {B : {k : I} -> A k -> Set γ} {x : A i} {y : A j}
      -> i ≅ j
      -> (f : {k : I} -> (x : A k) -> B x)
      -> x ≅ y
      -> f x ≅ f y
cong' _ refl _ refl = refl

unfold-reverse : {A : Set} → (x : A) → {n : ℕ} → (xs : Vec A n) →
                 reverse (x ∷ xs) ≅ reverse xs ++ (x ∷ [])
unfold-reverse x xs = begin
  foldl (Vec _ ∘ _+_ 1) (flip _∷_) (x ∷ []) xs
    ≅⟨ (foldl-cong
         {B₁ = Vec _ ∘ _+_ 1}
         {f₁ = flip _∷_}
         {e₁ = x ∷ []}
         {B₂ = Vec _ ∘ flip _+_ 1}
         {f₂ = flip _∷_}
         {e₂ = x ∷ []}
         (λ {n} {a} {as₁} {as₂} as₁≅as₂ -> begin
            a ∷ as₁
              ≅⟨ cong' (Vec _) (sym (≡-to-≅ (+-comm n 1))) (_∷_ a) as₁≅as₂ ⟩
            a ∷ as₂
            ∎)
         refl
         xs) ⟩
  foldl (Vec _ ∘ flip _+_ 1) (flip _∷_) (x ∷ []) xs
    ≅⟨ helper (x ∷ []) xs  ⟩
  reverse xs ++ x ∷ []
  ∎