[Agda] How can I prove associativity of vectors?

[Dan Licata]

In case anyone is curious, here's the example in question with path-over:
https://github.com/dlicata335/hott-agda/blob/master/misc/VecAssoc.agda

  ++-assoc : ∀ {A m n p} 
           (xs : Vec A m) (ys : Vec A n) (zs : Vec A p)
           → PathOver (Vec A) (+-assoc m n p) 
                              (xs ++ (ys ++ zs))
                              ((xs ++ ys) ++ zs)
  ++-assoc [] ys zs = id
  ++-assoc {A} (x :: xs) ys zs = 
    over-o-ap (Vec A) {S} (ap-nt-over (_::_ x) (++-assoc xs ys zs))

This says that the vectors are equal along the proof that + on numbers is associative (which is defined as usual elsewhere).  

The two lemmas I used are

  ap-nt-over :
    ∀ {A} {B C : A → Type} {a0 a1 : A} {b0 : B a0} {b1 : B a1}
      {p : a0 == a1} 
    → (f : {x : A} → B x → C x)
    → PathOver B p b0 b1
    → PathOver C p (f b0) (f b1)
  ap-nt-over f id = id

This says that if you have a map between fibrations over A, then it's functorial on path-overs (this is the "i-cong" discussed elsewhere in the thread, basically).

The second is

  over-o-ap : {A B : Type} (C : B → Type) {θ : A → B} 
               {a1 a2 : A} {p : a1 == a2}  {b1 : B a1} {b2 : B a2}
             → PathOver (C o θ) p b1 b2
             → PathOver C (ap θ p) b1 b2
  over-o-ap _ id = id

This "re-associates", moving stuff between the dependent type C and the path that you're over in the base.  

I don't think there's much difference between the factored PathOver and the (A≡B ⊨ x ≅ y) type described below by Alan Jeffrey (and of course formally they're equivalent types, and equivalent to using transport), but I've sometimes found it helpful to think in terms of PathOvers, at least in a HoTT setting.  

-Dan


On Dec 18, 2014, at 11:07 AM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda