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

    {-# OPTIONS --cubical-compatible --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           ∎