[Agda] Associativity for free!

[Nicolas Pouillard]

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)


-- 
Nicolas Pouillard
http://nicolaspouillard.fr