symIter is complete

SymIterComplete.agda

-- continued from https://gist.github.com/gergoerdi/46ad83513fd9db65c286

module Complete where
  open import Data.Product

  record SymItery {X Y : Set} : Set where
    constructor SymIter
    field
      zen : ℕ → X
      more : X → X
      post : X → Y

  eval : ∀ {X Y} → SymItery {X} {Y} → ℕ → ℕ → Y
  eval (SymIter zen more post) x y = post (symIter zen more x y)

  open import Data.Nat using (_+_)

  symIter-complete : ∀ {X} (f : ℕ → ℕ → X) → Commutative f → ∃ λ si → ∀ x y → eval {ℕ × ℕ} si x y ≡ f x y
  symIter-complete {X} f comm = min-diff (uncurry f′) , prf
    where
      min-diff : ∀ {A} (f : ℕ × ℕ → A) → SymItery
      min-diff = SymIter (λ diff → 0 , diff) (λ { (min , diff) → (suc min , diff) })

      f′ : ℕ → ℕ → X
      f′ min diff = f min (min + diff)

      open import Data.Sum

      lem : ∀ x y → let min = eval (min-diff proj₁) x y; diff = eval (min-diff proj₂) x y in
                    (min ≡ x × min + diff ≡ y) ⊎ (min ≡ y × min + diff ≡ x)
      lem zero y = inj₁ (refl , refl)
      lem (suc x) zero = inj₂ (refl , refl)
      lem (suc x) (suc y) with lem x y
      ... | inj₁ (p1 , p2) = inj₁ (cong suc p1 , cong suc p2)
      ... | inj₂ (p1 , p2) = inj₂ (cong suc p1 , cong suc p2)

      prf : ∀ x y → eval (min-diff (uncurry f′)) x y ≡ f x y
      prf x y with lem x y
      ... | inj₁ (p1 , p2) = cong₂ f p1 p2
      ... | inj₂ (p1 , p2) = trans (comm _ _) (cong₂ f p2 p1)