Defining commutative functions

SymIter.agda

-- From Conor McBride: https://lists.chalmers.se/pipermail/agda/2015/007768.html
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Function

symIter : {X : Set} → (ℕ → X) → (X → X) → ℕ → ℕ → X
symIter zen more zero    y       = zen y
symIter zen more x       zero    = zen x
symIter zen more (suc x) (suc y) = more $ symIter zen more x y

Commutative : {A B : Set} → (A → A → B) → Set
Commutative f = ∀ x y → f x y ≡ f y x

comm : ∀ {X : Set} (zen : ℕ → X) → ∀ more → Commutative (symIter zen more)
comm zen more zero    zero    = refl
comm zen more zero    (suc y) = refl
comm zen more (suc x) zero    = refl
comm zen more (suc x) (suc y) = cong more (comm zen more x y)

_⊔_ : ℕ → ℕ → ℕ
_⊔_ = symIter id suc

_⊓_ : ℕ → ℕ → ℕ
_⊓_ = symIter (const 0) suc

infixl 6 _+_
infixl 7 _*_

_+_ : ℕ → ℕ → ℕ
_+_ = symIter id (suc ∘ suc)

open import Data.Product

_+*_ : ℕ → ℕ → ℕ × ℕ
_+*_ = symIter (λ x → x , 0) $ λ { (y+x , x*y) → suc (suc y+x) , suc (y+x + x*y) }

_*_ : ℕ → ℕ → ℕ
_*_ = λ x y → proj₂ $ x +* y

module Correct where
  open Data.Nat renaming (_⊔_ to _⊔₀_; _⊓_ to _⊓₀_; _+_ to _+₀_; _*_ to _*₀_)
  open import Data.Nat.Properties.Simple
  open ≡-Reasoning

  ⊔-correct : ∀ x y → x ⊔ y ≡ x ⊔₀ y
  ⊔-correct zero y = refl
  ⊔-correct (suc x) zero = refl
  ⊔-correct (suc x) (suc y) = cong suc $ ⊔-correct x y

  ⊓-correct : ∀ x y → x ⊓ y ≡ x ⊓₀ y
  ⊓-correct zero y = refl
  ⊓-correct (suc x) zero = refl
  ⊓-correct (suc x) (suc y) = cong suc $ ⊓-correct x y

  +-correct : ∀ x y → x + y ≡ x +₀ y
  +-correct zero    y       = refl
  +-correct (suc x) zero    = sym $ +-right-identity (suc x)
  +-correct (suc x) (suc y) = begin
    suc (suc (x + y))  ≡⟨ cong (suc ∘ suc) $ +-correct x y ⟩
    suc (suc (x +₀ y)) ≡⟨ cong suc $ sym $ +-suc x y ⟩
    suc (x +₀ suc y)   ∎

  *-correct : ∀ x y → x * y ≡ x *₀ y
  *-correct zero    y       = refl
  *-correct (suc x) zero    = sym $ *-right-zero x
  *-correct (suc x) (suc y) = begin
    suc x * suc y                ≡⟨ refl ⟩
    proj₂ (suc x +* suc y)       ≡⟨ refl ⟩
    suc (proj₁ (x +* y) + x * y) ≡⟨ cong suc $ cong (λ z → z + x * y) $ lem x y ⟩
    suc ((x + y) + x * y)        ≡⟨ cong suc $ +-correct (x + y) (x * y) ⟩
    suc ((x + y)  +₀ x * y)      ≡⟨ cong suc $ cong₂ _+₀_ (+-correct x y) (*-correct x y) ⟩
    suc ((x +₀ y) +₀ x *₀ y)     ≡⟨ solve 2 (λ x y → con 1 :+ (x :+ y) :+ (x :* y) := (con 1 :+ y) :+ x :* (con 1 :+ y)) refl x y ⟩
    suc y +₀ x *₀ suc y          ∎
    where
      import Data.Nat.Properties as Nat
      open Nat.SemiringSolver

      lem : ∀ x y → proj₁ (x +* y) ≡ x + y
      lem zero    y = refl
      lem (suc x) zero = refl
      lem (suc x) (suc y) = begin
        suc (suc (proj₁ (x +* y))) ≡⟨ cong (suc ∘ suc) $ lem x y ⟩
        suc (suc (x + y)) ≡⟨ refl ⟩
        suc x + suc y ∎