[Agda] How can I prove associativity of vectors?

[Andrea Vezzosi]

In The HoTT-Agda lib they have PathOver:

PathOver : ∀ {i j} {A : Type i} (B : A → Type j)
                     {x y : A} (p : x == y) (u : B x) (v : B y) → Type j
PathOver B idp u v = (u == v)

i.e. PathOver P eq x y = cong P eq ⊨ x ≅ y

and a bunch of nice combinators for it:

https://github.com/HoTT/HoTT-Agda/blob/master/lib/PathOver.agda

If you are missing a K axiom it's pretty useful to know that the
equality on Vec A n and Vec A m only depends on the equality of n and
m, and not some more involved equivalence.

Cheers,
Andrea

On Thu, Dec 18, 2014 at 3:13 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> 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
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda