[Agda] How can I prove associativity of vectors?

[Alan Jeffrey]

A variant of this is to define a relation:

   (A≡B ⊨ x ≅ y)

where x : A, y : B and A≡B : A ≡ B. From that, proving properties modulo 
≡ on types is doable. There's probably a slicker version of xcong, or at 
least one compatible with --without-K.

A.

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

module Tmp where

_⊨_≅_ : ∀ {A B : Set} → (A ≡ B) → A → B → Set
_⊨_≅_ refl = _≡_

xcong : ∀ {I : Set} (F G : I → Set) (f : ∀ {i} → F i → G i) {i j x y} →
   ∀ (i≡j : i ≡ j) {Fi≡Fj : F i ≡ F j} {Gi≡Gj : G i ≡ G j} →
    (Fi≡Fj ⊨ x ≅ y) → (Gi≡Gj ⊨ f x ≅ f y)
xcong F G f refl {refl} {refl} refl = refl

+-assoc : ∀ ℓ m n → ((ℓ + m) + n) ≡ (ℓ + (m + n))
+-assoc zero    m n = refl
+-assoc (suc ℓ) m n = cong suc (+-assoc ℓ m n)

++-assoc : ∀ {A ℓ m n} (xs : Vec A ℓ) (ys : Vec A m) (zs : Vec A n) →
   (cong (Vec A) (+-assoc ℓ m n) ⊨
     ((xs ++ ys) ++ zs) ≅ (xs ++ (ys ++ zs)))
++-assoc {A} {zero}  []       ys zs = refl
++-assoc {A} {suc ℓ} (x ∷ xs) ys zs =
   xcong (Vec A) (Vec A ∘ suc) (_∷_ x)
     (+-assoc ℓ _ _) (++-assoc xs ys zs)


On 12/17/2014 04:52 PM, Conor McBride wrote:
> Hi
>
> A little bird told me I should pay attention for a change. Here’s what I cooked up.
>
> Given that intensional equality is always a disappointment, it is too much to expect
> the values on either side of a propositional equation to have intensionally equal
> types. The method for working with heterogeneous equality is always to work with
> whole telescopes and make sure that whenever the types stretch apart (like the
> vector types below), you always have an equation which tells you why they are
> provably equal.
>
> I could probably be more systematic about building the “resp” family, but it’s late and
> I’m tired.
>
> All the best
>
> Conor
>
> --------------------------------------------------------------
> module VVV where
>
> data Nat : Set where
>   ze : Nat
>   su : Nat -> Nat
>
> _+_ : Nat -> Nat -> Nat
> ze + y = y
> su x + y = su (x + y)
>
> data Vec (X : Set) : Nat -> Set where
>   [] : Vec X ze
>   _,_ : {n : Nat} -> X -> Vec X n -> Vec X (su n)
>
> data _==_ {A : Set}(a : A) : {B : Set} -> B -> Set where
>   refl : a == a
>
> _++_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m + n)
> [] ++ ys = ys
> (x , xs) ++ ys = x , (xs ++ ys)
>
> record _*_ (S T : Set) : Set where
>   constructor _,_
>   field
>     fst : S
>     snd : T
> open _*_ public
>
> resp1 : {A : Set}{B : A -> Set}
>   (f : (a : A) -> B a)
>   {a a' : A} -> a == a' ->
>   f a == f a'
> resp1 f refl = refl
>
> resp3 : {A : Set}{B : A -> Set}{C : (a : A)(b : B a) -> Set}{D : (a : A)(b : B a)(c : C a b) -> Set}
>   (f : (a : A)(b : B a)(c : C a b) -> D a b c) ->
>   {a a' : A} -> a == a' ->
>   {b : B a}{b' : B a'} -> b == b' ->
>   {c : C a b}{c' : C a' b'} -> c == c' ->
>   f a b c == f a' b' c'
> resp3 f refl refl refl = refl
>
> vc : {X : Set}(n : Nat)(x : X) -> Vec X n -> Vec X (su n)
> vc n x xs = x , xs
>
> vass : {X : Set}{l m n : Nat}(xs : Vec X l)(ys : Vec X m)(zs : Vec X n) ->
>   (((l + m) + n) == (l + (m + n))) *
>   (((xs ++ ys) ++ zs) == (xs ++ (ys ++ zs)))
> vass [] ys zs = refl , refl
> vass (x , xs) ys zs with vass xs ys zs
> ... | q , q' = (resp1 su q) , resp3 vc q refl q'
> --------------------------------------------------------------
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>