[Agda] How can I prove associativity of vectors?

[Alan Jeffrey]

Ah, that's the trick for getting it to work --without-K. Nice.

A.

{-# OPTIONS --without-K #-}

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

module Tmp where

_⊨_⇒_≡_ : ∀ {I : Set} (F : I → Set) {i j} →
   (i ≡ j) → (F i) → (F j) → Set
(F ⊨ refl ⇒ x ≡ y) = (x ≡ y)

xcong : ∀ {I J F G} (f : I → J) (g : ∀ {i} → F i → G (f i)) →
   ∀ {i j} (i≡j : i ≡ j) {x y} →
     (F ⊨ i≡j ⇒ x ≡ y) → (G ⊨ cong f i≡j ⇒ g x ≡ g y)
xcong f g refl refl = refl

+-assoc : ∀ ℓ m n → ((ℓ + m) + n) ≡ (ℓ + (m + n))
+-assoc 0       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) →
   (Vec A ⊨ (+-assoc ℓ m n) ⇒ ((xs ++ ys) ++ zs) ≡ (xs ++ (ys ++ zs)))
++-assoc 0       m n []       ys zs = refl
++-assoc (suc ℓ) m n (x ∷ xs) ys zs =
   xcong suc (_∷_ x) (+-assoc ℓ m n) (++-assoc ℓ m n xs ys zs)

On 12/18/2014 10:07 AM, Andrea Vezzosi 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