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

[Nils Anders Danielsson]

On 2009-01-08 14:41, Shin-Cheng Mu wrote:
> For lists, it is a trivial matter proving that:
> 
>    reverse xs = revcat xs []
> 
> But how to do so for Vectors?

[...]

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

[...]

> Is (1) provable at all?

No.

> If not, is there a way to avoid it?

Yes, prove that foldl is congruential in a suitable sense:

   module Rev where

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

   revcat : ∀ {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

   foldl-cong :
     {A : Set}
     {B₁ : ℕ → Set} {n₁ : B₁ zero}
     {c₁ : ∀ {n} → B₁ n → A → B₁ (suc n)}
     {B₂ : ℕ → Set} {n₂ : B₂ zero}
     {c₂ : ∀ {n} → B₂ n → A → B₂ (suc n)} →
     (B-eq : ∀ n → B₁ n ≡₁ B₂ n) →
     (∀ {n} {b₁ : B₁ n} {b₂ : B₂ n} {a : A} →
        b₁ ≅ b₂ → c₁ b₁ a ≅ c₂ b₂ a) →
     n₁ ≅ n₂ →
     ∀ {m} (xs : Vec A m) → foldl B₁ c₁ n₁ xs ≅ foldl B₂ c₂ n₂ xs
   foldl-cong B-eq c-eq n-eq []       = n-eq
   foldl-cong B-eq c-eq n-eq (x ∷ xs) =
     foldl-cong (λ n → B-eq (suc n)) c-eq (c-eq n-eq) xs

   ∷-cong : ∀ {A x n₁ n₂} {xs₁ : Vec A n₁} {xs₂ : Vec A n₂} →
            xs₁ ≅ xs₂ → x ∷ xs₁ ≅ x ∷ xs₂
   ∷-cong ≅-refl = ≅-refl

   lemma : ∀ {A m} (xs : Vec A m) -> reverse xs ≅ revcat xs []
   lemma {A} = foldl-cong (λ n → ≡₀₁-cong (Vec A) (n=n+0 n)) ∷-cong ≅-refl
     where
     n=n+0 = sym ∘ proj₂ +-identity
       where open CommutativeSemiring Nat.commutativeSemiring

-- 
/NAD



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.