[Agda] Associativity for free!

[Alan Jeffrey]

Cool! For your next trick, difference vectors over difference naturals, 
and get associativity for free there :-)

A.

On 10/26/2011 04:28 PM, Nicolas Pouillard wrote:
> On Wed, Oct 26, 2011 at 4:48 PM, Alan Jeffrey<ajeffrey at bell-labs.com>  wrote:
>> Hi everyone,
>>
>> A quick note about a trick for representing lists (or any other monoid) up
>> to associativity. Am I reinventing a wheel here?
>
> Well done, nice trick!
>
> I've just tried on natural numbers using difference nats, then vectors based
> on these nats and finally associativity of ++ goes well.
>
> module diffnat-assoc where
>
> open import Data.Nat
> open import Function
> open import Relation.Binary.PropositionalEquality
>
> record D : Set where
>    constructor mk
>    field
>      n    : ℕ
>      f     : ℕ → ℕ
>      .f✓ : f ≡ _+_ n
>
> _ᴰ : ℕ → D
> n ᴰ = mk n (_+_ n) refl
>
> _+ᴰ_ : D → D → D
> mk m f f✓ +ᴰ mk n g g✓ = mk (f n) (f ∘ g) (f∘g✓ f f✓ g g✓)
>   where
>    assoc : ∀ m {n} → (λ x → m + (n + x)) ≡ _+_ (m + n)
>    assoc zero    = refl
>    assoc (suc m) = cong (_∘_ suc) (assoc m)
>
>    .f∘g✓ : ∀ f (f✓ : f ≡ _+_ m) g (g✓ : g ≡ _+_ n) → f ∘ g ≡ _+_ (f n)
>    f∘g✓ ._ refl ._ refl = assoc m
>
> 0ᴰ : D
> 0ᴰ = 0 ᴰ
>
> 1ᴰ : D
> 1ᴰ = 1 ᴰ
>
> sucᴰ : D → D
> sucᴰ = _+ᴰ_ 1ᴰ
>
> free-assoc : ∀ {m n o} → m +ᴰ (n +ᴰ o) ≡ (m +ᴰ n) +ᴰ o
> free-assoc = refl
>
> data Vec (A : Set) : D → Set where
>    [] : Vec A 0ᴰ
>    _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (sucᴰ n)
>
> _++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +ᴰ n)
> []       ++ ys = ys
> (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
>
> free-Vec-assoc : ∀ {A m n o} → Vec A ((m +ᴰ n) +ᴰ o) ≡ Vec A (m +ᴰ (n +ᴰ o))
> free-Vec-assoc = refl
>
> -- With usual vectors one can't even state this
> -- lemma using homogeneous equality.
> ++-assoc : ∀ {A m n o} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
>               (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
> ++-assoc []       ys zs = refl
> ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
>
>