adders.agda

module adders where

open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning; _≗_)
open import Function
  using (_∘_; id)

private variable
  A B C D X Y Z W : Set
  f f₁ f₂ g₁ g₂ t t₁ t₂ b b₁ b₂ l l₁ l₂ r r₁ r₂ : A → B
  g : C → D
  h : X → Y
  i : Z → W
  x : A → B
  y : A → B
  w : A → B
  z : A → B

record □₂ (bot : A → B) (left : A → C) (top : C → D) (right : B → D) : Set where
  constructor square
  field
    commutes : top ∘ left ≗ right ∘ bot

arr : ∀ {bot top} → (left : A → C) (right : B → D) → (top ∘ left ≗ right ∘ bot) → □₂ bot left top right
arr _ _ c = square c

_ᵀ : □₂ f g h i → □₂ g f i h
square commutes ᵀ = square (sym ∘ commutes)


infix 3 _⇉_
_⇉_ : ∀ {h i} → (C → D) → (A → B) → Set
_⇉_ {h = h} {i} g f = □₂ g h f i

□-id : (f : A → B) → □₂ f id f id
□₂.commutes (□-id f) a = refl

infixr 3 _□∘_
infixr 3 _□⊚_

_□∘_ : □₂ x l₁ t₁ r₁ → □₂ b₂ l₂ x r₂ → □₂ b₂ (l₁ ∘ l₂) t₁ (r₁ ∘ r₂)
□₂.commutes (_□∘_ {x = b₁} {l₁ = l₁} {t₁ = t₁} {r₁ = r₁} {b₂ = b₂} {l₂ = l₂} {r₂ = r₂} g f) a
  = begin
  t₁ (l₁ (l₂ a))  ≡⟨ □₂.commutes g _ ⟩
  r₁ (b₁ (l₂ a))  ≡⟨ cong r₁ (□₂.commutes f _) ⟩
  r₁ (r₂ (b₂ a))  ∎
  where open ≡-Reasoning

_□⊚_ : □₂ b₁ x t₁ r₁ → □₂ b₂ l₂ t₂ x → □₂ (b₁ ∘ b₂) l₂ (t₁ ∘ t₂) r₁
□₂.commutes (_□⊚_ {b₁ = b₁} {x = l₁} {t₁ = t₁} {r₁ = r₁} {b₂ = b₂} {l₂ = l₂} {t₂ = t₂}  g f) a
  = begin
  t₁ (t₂ (l₂ a))    ≡⟨ cong t₁ (□₂.commutes f _) ⟩
  t₁ (l₁ (b₂ a))    ≡⟨ □₂.commutes g _ ⟩
  r₁ ((b₁ ∘ b₂) a)  ∎
  where open ≡-Reasoning

open import Data.Nat
open import Data.Product
  using (_×_; _,_; map₁; map₂; proj₁; proj₂; assocˡ; assocʳ; <_,_>)


infixr 6 _⊗_
_⊗_ : (A → B) → (C → D) → A × C → B × D
(f ⊗ g) (a , c) = f a , g c


□-fst : (f ⊗ g) ⇉ f
□-fst = arr proj₁ proj₁ λ { x → refl }

□-snd : (f ⊗ g) ⇉ g
□-snd = arr proj₂ proj₂ λ { x → refl }

□-fork : □₂ f l₁ g₁ r₁ → □₂ f l₂ g₂ r₂ → f ⇉ g₁ ⊗ g₂
□-fork {l₁ = l₁} {r₁ = r₁} {l₂ = l₂} {r₂ = r₂} (square fg₁) (square fg₂)
  = arr (< l₁ , l₂ >) (< r₁ , r₂ >) λ { x → cong₂ _,_ (fg₁ x) (fg₂ x) }

□-map₁ : □₂ f l g r → f ⊗ h ⇉ g ⊗ h
□-map₁ {l = l}  {r = r} (square commutes)
  = arr (map₁ l) (map₁ r) λ { x → cong (_, _) (commutes (proj₁ x)) }

□-map₂ : □₂ f l g r → h ⊗ f ⇉ h ⊗ g
□-map₂ {l = l}  {r = r} (square commutes)
  = arr (map₂ l) (map₂ r) λ { x → cong (_ ,_) (commutes (proj₂ x)) }

□-assocˡ : f ⊗ (g ⊗ h) ⇉ (f ⊗ g) ⊗ h
□-assocˡ = arr assocˡ assocˡ λ { x → refl }

□-assocʳ : (f ⊗ g) ⊗ h ⇉ f ⊗ (g ⊗ h)
□-assocʳ = arr assocʳ assocʳ λ { x → refl }



ℕ² : Set
ℕ² = ℕ × ℕ

⟨+⟩ : ℕ² → ℕ
⟨+⟩ (x , y) = x + y

open import Data.Fin
  using (Fin; toℕ; zero; suc; inject≤)

private variable
  m n p : ℕ
  mn : ℕ²

Fin² : ℕ² → Set
Fin² (m , n) = Fin m × Fin n

toℕ² : Fin² mn → ℕ²
toℕ² = toℕ ⊗ toℕ

open import Data.Nat.Properties
  using (m≤m+n; +-comm; module ≤-Reasoning)

⟨+ᶠ⟩ : Fin (suc m) × Fin n → Fin (m + n)
⟨+ᶠ⟩ {m} {n} (zero , y) = inject≤ y (begin
  n      ≤⟨ m≤m+n n m ⟩
  n + m  ≡⟨ +-comm n m ⟩
  m + n  ∎
  )
  where open ≤-Reasoning
⟨+ᶠ⟩ {suc m} {n} (suc x , y) = suc (⟨+ᶠ⟩ (x , y))

infixl 6 _+ᶠ_
_+ᶠ_ : Fin (suc m) → Fin n → Fin (m + n)
x +ᶠ y = ⟨+ᶠ⟩ (x , y)

open import Data.Fin.Properties
  using (toℕ-inject≤)

toℕ-suc : ∀ x → toℕ (suc {m} x) ≡ suc (toℕ x)
toℕ-suc zero = refl
toℕ-suc (suc x) = cong suc (toℕ-suc x)

toℕ-+ᶠ : ⟨+⟩ ∘ toℕ² {suc (suc m) , n} ≗ toℕ {suc m + n} ∘ ⟨+ᶠ⟩
toℕ-+ᶠ (zero , y) = begin
  toℕ y                    ≡⟨ sym (toℕ-inject≤ y _) ⟩
  (toℕ ∘ ⟨+ᶠ⟩) (zero , y)  ∎
  where open ≡-Reasoning
toℕ-+ᶠ {zero} (suc zero , y) = begin
  suc (toℕ y)             ≡⟨ sym (cong suc (toℕ-inject≤ y _)) ⟩
  suc (toℕ (inject≤ y _)) ≡⟨ sym (toℕ-suc _) ⟩
  toℕ (suc (inject≤ y _)) ∎
  where open ≡-Reasoning
toℕ-+ᶠ {suc m} (suc x , y) = cong suc (toℕ-+ᶠ (x , y))

+ᶠ⇉ : (⟨+ᶠ⟩ {suc m} {n}) ⇉ ⟨+⟩
+ᶠ⇉ = arr toℕ² toℕ toℕ-+ᶠ

+ᶠ⇉' : ∀ {m} {n} → toℕ² ⇉ toℕ
+ᶠ⇉' {m} {n} = +ᶠ⇉ {m} {n} ᵀ

ℕ³ : Set
ℕ³ = ℕ × ℕ²

Fin³ : ℕ³ → Set
Fin³ (p , m , n) = Fin p × Fin m × Fin n

addFin : ∀ {(m , n) : ℕ²} → Fin³ (2 , m , n) → Fin (m + n)
addFin (ci , a , b) = ci +ᶠ a +ᶠ b

addℕ : ℕ³ → ℕ
addℕ (c , a , b) = c + a + b

toℕ³ : {pmn : ℕ³} → Fin³ pmn → ℕ³
toℕ³ = toℕ ⊗ toℕ²

toℕ-addFin : addℕ ∘ toℕ³ ≗ toℕ ∘ addFin {suc m , n}
toℕ-addFin (ci , a , b)
  rewrite sym (toℕ-+ᶠ (ci +ᶠ a , b))
        | toℕ-+ᶠ (ci , a)
  = refl

addFin⇉₀ : addFin {suc m , n} ⇉ addℕ
addFin⇉₀ = arr toℕ³ toℕ toℕ-addFin

refactor-addℕ : addℕ ≗ ⟨+⟩ ∘ map₁ ⟨+⟩ ∘ assocˡ
refactor-addℕ _ = refl

refactor-addFin : addFin {m , n} ≗ ⟨+ᶠ⟩ ∘ map₁ ⟨+ᶠ⟩ ∘ assocˡ
refactor-addFin _ = refl

addFin⇉ : □₂ (toℕ³ {2 , suc m , n }) (⟨+ᶠ⟩ ∘ map₁ ⟨+ᶠ⟩ ∘ assocˡ) (toℕ {suc m + n}) (⟨+⟩ ∘ map₁ ⟨+⟩ ∘ assocˡ)
addFin⇉ = +ᶠ⇉ ᵀ □∘ □-map₁ +ᶠ⇉' □∘ □-assocˡ