GeneralisedArithmetic

------------------------------------------------------------------------
-- The Agda standard library
--
-- A generalisation of the arithmetic operations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Nat.GeneralisedArithmetic where

open import Data.Nat.Base using (β„•; zero; suc; _+_; _*_; _^_)
open import Data.Nat.Properties
  using (+-comm; +-assoc; *-identityΛ‘; *-assoc)
open import Function.Base using (_βˆ˜β€²_; _∘_; id)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core
  using (_≑_; refl; cong; sym)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≑-Reasoning)
open ≑-Reasoning

private
  variable
    a : Level
    A : Set a

fold : A β†’ (A β†’ A) β†’ β„• β†’ A
fold z s zero    = z
fold z s (suc n) = s (fold z s n)

iterate : (A β†’ A) β†’ A β†’ β„• β†’ A
iterate f x zero    = x
iterate f x (suc n) = iterate f (f x) n

add : (0# : A) (1+ : A β†’ A) β†’ β„• β†’ A β†’ A
add 0# 1+ n z = fold z 1+ n

mul : (0# : A) (1+ : A β†’ A) β†’ (+ : A β†’ A β†’ A) β†’ (β„• β†’ A β†’ A)
mul 0# 1+ _+_ n x = fold 0# (Ξ» s β†’ x + s) n

-- Properties

fold-+ : βˆ€ (z : A) (s : A β†’ A) m {n} β†’
         fold z s (m + n) ≑ fold (fold z s n) s m
fold-+ z s zero    = refl
fold-+ z s (suc m) = cong s (fold-+ z s m)

fold-k : βˆ€ (z : A) (s : A β†’ A) {k} m β†’
         fold k (s βˆ˜β€²_) m z ≑ fold (k z) s m
fold-k z s zero    = refl
fold-k z s (suc m) = cong s (fold-k z s m)

fold-* : βˆ€ (z : A) (s : A β†’ A) m {n} β†’
         fold z s (m * n) ≑ fold z (fold id (s ∘_) n) m
fold-* z s zero        = refl
fold-* z s (suc m) {n} = let +n = fold id (s βˆ˜β€²_) n in begin
  fold z s (n + m * n)        β‰‘βŸ¨ fold-+ z s n ⟩
  fold (fold z s (m * n)) s n β‰‘βŸ¨ cong (Ξ» z β†’ fold z s n) (fold-* z s m) ⟩
  fold (fold z +n m) s n      β‰‘βŸ¨ sym (fold-k _ s n) ⟩
  fold z +n (suc m)           ∎

fold-pull : βˆ€ (z : A) (s : A β†’ A) (g : A β†’ A β†’ A) (p : A)
            (eqz : g z p ≑ p)
            (eqs : βˆ€ l β†’ s (g l p) ≑ g (s l) p) β†’
            βˆ€ m β†’ fold p s m ≑ g (fold z s m) p
fold-pull z s _ _ eqz _ zero    = sym eqz
fold-pull z s g p eqz eqs (suc m) = begin
  s (fold p s m)       β‰‘βŸ¨ cong s (fold-pull z s g p eqz eqs m) ⟩
  s (g (fold z s m) p) β‰‘βŸ¨ eqs (fold z s m) ⟩
  g (s (fold z s m)) p ∎

iterate-is-fold : βˆ€ (z : A) s m β†’ fold z s m ≑ iterate s z m
iterate-is-fold z s zero    = refl
iterate-is-fold z s (suc m) = begin
  fold z s (suc m)  β‰‘βŸ¨ cong (fold z s) (+-comm 1 m) ⟩
  fold z s (m + 1)  β‰‘βŸ¨ fold-+ z s m ⟩
  fold (s z) s m    β‰‘βŸ¨ iterate-is-fold (s z) s m ⟩
  iterate s (s z) m ∎

id-is-fold : βˆ€ m β†’ fold zero suc m ≑ m
id-is-fold zero    = refl
id-is-fold (suc m) = cong suc (id-is-fold m)

+-is-fold : βˆ€ m {n} β†’ fold n suc m ≑ m + n
+-is-fold zero    = refl
+-is-fold (suc m) = cong suc (+-is-fold m)

*-is-fold : βˆ€ m {n} β†’ fold zero (n +_) m ≑ m * n
*-is-fold zero        = refl
*-is-fold (suc m) {n} = cong (n +_) (*-is-fold m)

^-is-fold : βˆ€ {m} n β†’ fold 1 (m *_) n ≑ m ^ n
^-is-fold     zero    = refl
^-is-fold {m} (suc n) = cong (m *_) (^-is-fold n)

*+-is-fold : βˆ€ m n {p} β†’ fold p (n +_) m ≑ m * n + p
*+-is-fold m n {p} = begin
  fold p (n +_) m     β‰‘βŸ¨ fold-pull _ _ _+_ p refl
                         (Ξ» l β†’ sym (+-assoc n l p)) m ⟩
  fold 0 (n +_) m + p β‰‘βŸ¨ cong (_+ p) (*-is-fold m) ⟩
  m * n + p           ∎

^*-is-fold : βˆ€ m n {p} β†’ fold p (m *_) n ≑ m ^ n * p
^*-is-fold m n {p} = begin
  fold p (m *_) n     β‰‘βŸ¨ fold-pull _ _ _*_ p (*-identityΛ‘ p)
                         (Ξ» l β†’ sym (*-assoc m l p)) n ⟩
  fold 1 (m *_) n * p β‰‘βŸ¨ cong (_* p) (^-is-fold n) ⟩
  m ^ n * p           ∎