[Agda] Extensional equality, or how to avoid needing it?

[Shin-Cheng Mu]

Vector reversal can be defined in terms of a foldl:

   reverse : forall {a n} -> Vec a n -> Vec a n
   reverse {a} = foldl (Vec a) (\rev x -> x ∷ rev) []

where foldl has type

   foldl :  forall {a : Set} (b : ℕ -> Set) {m}
         -> (forall {n} -> b n -> a -> b (suc n))
         -> b zero
         -> Vec a m -> b m

In many situations when we want to prove properties
of reverse, we have to prove the property for a
generalisation of reverse, which I call "revcat",
which abstracts the third argument to foldl as well:

   revcat : forall {a m n}
          -> Vec a m -> Vec a n -> Vec a (m + n)
   revcat {a}{m}{n} xs ys =
      foldl (\i -> Vec a (i + n)) (\rev x -> x ∷ rev) ys xs

(They are related by the equation:
   revcat xs ys = reverse xs ++ ys)

For lists, it is a trivial matter proving that:

    reverse xs = revcat xs []

But how to do so for Vectors?

I started with:

   lemma : forall {a m} (xs : Vec a m)
         -> reverse xs ≅ revcat xs []
   lemma xs = { }0

and didn't get very far. The term reverse xs has type
Vec a m, while revcat xs [] has type Vec a (m + 0). Thus
we use heterogenous equality. The hole { }0 expects a
term having type:

?0 : foldl (Vec .a) (\{.n} rev x -> x ∷ rev) [] xs ≅
      foldl (\i -> Vec .a (i + 0)) (\{.n} rev x -> x ∷ rev) [] xs

The only part that does not match are the first arguments:
(\i -> Vec a i) and (\i -> Vec a (i + 0)). At the first
glance it appears that they are the same by congruence.
We can prove that

      forall i -> i ≅ (i + 0)

and by (a variation of) congruence we get

      forall i -> Vec a i ≅₁ Vec a (i + 0)

However, what we need now is

      (\i -> Vec a i) ≅₁ (\i -> Vec a (i + 0))  ... (1)

from which we may prove { }0 by congruence.
I could not figure out how to prove (1).

Is (1) provable at all? If not, is there a way to
avoid it?

Thanks!

sincerely,
Shin

    ---- Code attached below

module Rev where

open import Data.Product
open import Data.Nat
open import Data.Vec
open import Relation.Binary.HeterogeneousEquality
open import Algebra
open import Data.Nat.Properties

{- Defined in Data.Vec
reverse : forall {a n} -> Vec a n -> Vec a n
reverse {a} = foldl (Vec a) (\rev x -> x ∷ rev) []
-}

revcat : forall {a m n} -> Vec a m -> Vec a n -> Vec a (m + n)
revcat {a}{m}{n} xs ys = foldl (\i -> Vec a (i + n)) (\rev x -> x ∷  
rev) ys xs

lemma : forall {a m} (xs : Vec a m) -> reverse xs ≅ revcat xs []
lemma xs = {! !}
   where
      n+0=n = (proj₂ (CommutativeSemiring.+-identity  
commutativeSemiring))
         where open CommutativeSemiring commutativeSemiring