[Agda] Re: How can I prove associativity of vectors?

[Kenichi Asai]

Thank you for the messages!  I could now implement it in two ways.

>  * Use Data.Vec.Equality rather than PropositionalEquality.

Attached Append.agda.

>  * Use Relation.Binary.HeterogeneousEquality rather than
>    PropositionalEquality.

Attached Append2.agda.  But I had to use hcong' as shown in the
following stackoverflow article:

http://stackoverflow.com/questions/24139810/stuck-on-proof-with-heterogeneous-equality

Rather than using hcong', I wanted to say:

assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) → 
        (l1 ++ l2) ++ l3 ≅ l1 ++ (l2 ++ l3)
assoc [] l2 l3 = refl
assoc (x ∷ l1) l2 l3 = cong (λ l → x ∷ l) (assoc l1 l2 l3)

but it did not work, because cong appears to assume that two sides of
≅ has the same type.  Why is it so?  I think it is more natural that
cong etc. in HeterogeneousEquality module are defined for heterogeneous
types.

The above stackoverflow article implies that there are general
versions hcong, hsubst, etc.  Are they going to be included in the
standard library?

>  * Use Relation.Binary.PropositionalEquality.Core.subst and
>    Data.Nat.Properties.Simple.+-assoc to make the types match.
> 
> The last option gets ugly but allows you to keep using
> PropositionalEquality.

I dare not try this one.  I think HeterogeneousEquality is the way to
go.

> May be, this can be used instead?

I did not use toList because I wanted to keep the length of vectors.

Sincerely,

-- 
Kenichi Asai
-------------- next part --------------
module Append where

open import Data.Nat
open import Data.Vec
open import Data.Vec.Properties
open import Data.Vec.Equality
open import Relation.Binary.PropositionalEquality
open Equality (setoid ℕ) renaming (refl to vrefl)

assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) → 
        (l1 ++ l2) ++ l3 ≈ l1 ++ (l2 ++ l3)
assoc [] l2 l3 = vrefl (l2 ++ l3)
assoc (x ∷ l1) l2 l3 = refl ∷-cong assoc l1 l2 l3
-------------- next part --------------
module Append2 where

open import Data.Nat
open import Data.Vec
open import Relation.Binary.PropositionalEquality using (_≡_) renaming (refl to prefl)
open import Relation.Binary.HeterogeneousEquality
open import Level using (Level)

open import Data.Nat.Properties
open import Algebra.Structures
private module M = IsCommutativeSemiring

+-assoc : ∀ m n o → (m + n) + o ≡  m + (n + o)
+-assoc = M.+-assoc isCommutativeSemiring

hcong' : {α β γ : Level} {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
hcong' _ prefl _ refl = refl

assoc : ∀ {l m n} → (l1 : Vec ℕ l) → (l2 : Vec ℕ m) → (l3 : Vec ℕ n) → 
        (l1 ++ l2) ++ l3 ≅ l1 ++ (l2 ++ l3)
assoc [] l2 l3 = refl
assoc {suc l} {m} {n} (x ∷ l1) l2 l3 = hcong' (Vec ℕ) (+-assoc l m n) (λ l → x ∷ l) (assoc l1 l2 l3)