What if we reify plus and other things normally expressed as functions?

Reify.agda

module Reify where

open import Agda.Builtin.Equality

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

module Function where
  _+_ : ℕ → ℕ → ℕ
  zero + y = y
  suc x + y = suc (x + y)

  0+ : (x : ℕ) → 0 + x ≡ x
  0+ x = refl

  +0 : (x : ℕ) → x + 0 ≡ x
  +0 zero = refl
  +0 (suc x) rewrite +0 x = refl

  +assoc : (x y z : ℕ) → (x + y) + z ≡ x + (y + z)
  +assoc zero y z = refl
  +assoc (suc x) zero z rewrite +0 x = refl
  +assoc (suc x) (suc y) zero rewrite +0 (x + suc y) | +0 y = refl
  +assoc (suc x) (suc y) (suc z) rewrite +assoc x (suc y) (suc z) = refl

module +Relation where
  data _+_ : (x y : ℕ) → Set where
    zero+ : (y : ℕ) → zero + y
    suc+ : {x y : ℕ} → x + y → suc x + y

  _+total_ : (x y : ℕ) → x + y
  zero +total y = zero+ y
  suc x +total y = suc+ (x +total y)

module +Relation-ReduceFunction where
  open +Relation
  +reduce : {x y : ℕ} → x + y → ℕ
  +reduce (zero+ y) = y
  +reduce (suc+ p) = suc (+reduce p)

  0+ : {x : ℕ} → (r : 0 + x) → +reduce r ≡ x
  0+ (zero+ y) = refl

  +0 : {x : ℕ} → (r : x + 0) → +reduce r ≡ x
  +0 (zero+ .zero) = refl
  +0 (suc+ r) rewrite +0 r = refl

--  +assoc : {x y z : ℕ} → (x + y) + z → x + (y + z)

open import Agda.Primitive
record ∃ {lx ly : Level} {X : Set lx} (Y : X → Set ly) : Set (lx ⊔ ly) where
  constructor lo
  field
    item : X
    dep : Y item

module +Relation-ReduceRelation where
  open +Relation
  data _+~>_
    : {x y : ℕ}
    → x + y
    → ℕ
    → Set where
    zero+R : (y : ℕ) → zero+ y +~> y
    suc+R : {x y z : ℕ} → (p : x + y) → suc+ p +~> suc z

  +~>total : (x y : ℕ) → (p : x + y) → ∃ (λ z → p +~> z)
  +~>total .0 y (zero+ .y) = lo y (zero+R y)
  +~>total _ y (suc+ x₁) = lo (suc y) (suc+R x₁)

  0+ : {x : ℕ} → (p : 0 + x) → p +~> x
  0+ (zero+ y) = zero+R y

  +0 : {x : ℕ} → (p : x + 0) → p +~> x
  +0 (zero+ .0) = zero+R zero
  +0 (suc+ x₁) = suc+R x₁

module +ReduceRelation where
  data _+_~>_ : (x y z : ℕ) → Set where
    zero+ : (x : ℕ) → 0 + x ~> x
    suc+ : (x y z : ℕ) → x + y ~> z → suc x + y ~> suc z

  +~>total : (x y : ℕ) → ∃ (λ z → x + y ~> z)
  +~>total zero y = lo y (zero+ y)
  +~>total (suc x) y =
    let lo item dep = +~>total x y
    in lo (suc item) (suc+ x y item dep)

  +~>unique : (x y z r : ℕ) → x + y ~> z → x + y ~> r → z ≡ r
  +~>unique .0 r .r .r (zero+ .r) (zero+ .r) = refl
  +~>unique .(suc x) y .(suc z₁) .(suc z) (suc+ x .y z₁ p) (suc+ .x .y z q) rewrite +~>unique x y z₁ z p q = refl

  _+'_ : (x y : ℕ) → ℕ
  x +' y = ∃.item (+~>total x y)

  +~>≡ : (x y z : ℕ) → x + y ~> z → x +' y ≡ z
  +~>≡ .0 z .z (zero+ .z) = refl
  +~>≡ .(suc x) y .(suc z) (suc+ x .y z p) rewrite +~>≡ x y z p = refl

  0+ : (x : ℕ) → 0 + x ~> x
  0+ x = zero+ x

  0+' : (x : ℕ) → 0 +' x ≡ x
  0+' x = refl

  +0 : (x : ℕ) → x + 0 ~> x
  +0 zero = zero+ zero
  +0 (suc x) = suc+ x zero x (+0 x)

  +'0 : (x : ℕ) → x +' 0 ≡ x
  +'0 zero = refl
  +'0 (suc x) rewrite +'0 x = refl

  +'0' : (x : ℕ) → x +' 0 ≡ x
  +'0' x = +~>≡ x 0 x (+0 x)

  sucr : (x y z : ℕ) → x + y ~> z → x + suc y ~> suc z
  sucr .0 z .z (zero+ .z) = zero+ (suc z)
  sucr .(suc x) y .(suc z) (suc+ x .y z x₁) = suc+ x (suc y) (suc z) (sucr x y z x₁)

  +comm : (x y z : ℕ) → x + y ~> z → y + x ~> z
  +comm .0 z .z (zero+ .z) = +0 z
  +comm .(suc x) y .(suc z) (suc+ x .y z p) = sucr y x z (+comm x y z p)

  +assoc : (x y r s t z : ℕ)
    → x + y ~> r
    → r + z ~> t
    → y + z ~> s
    → x + s ~> t
  +assoc .0 .0 .0 s .s .s (zero+ .0) (zero+ .s) (zero+ .s) = zero+ s
  +assoc .0 .(suc x) .(suc x) .(suc z₁) .(suc z₂) z (zero+ .(suc x)) (suc+ x .z z₂ q) (suc+ .x .z z₁ v)
    rewrite +~>unique x z z₂ z₁ q v = zero+ (suc z₁)
  +assoc .(suc x) .0 .(suc z) s .(suc z₁) .s (suc+ x .0 z p) (suc+ .z .s z₁ q) (zero+ .s)
    = suc+ x s z₁ (+assoc x zero z s z₁ s p q (zero+ s))
  +assoc .(suc x₁) .(suc x) .(suc z₂) .(suc z₁) .(suc z₃) z (suc+ x₁ .(suc x) z₂ p) (suc+ .z₂ .z z₃ q) (suc+ x .z z₁ v)
    = suc+ x₁ (suc z₁) z₃ (+assoc x₁ (suc x) z₂ (suc z₁) z₃ z p q (suc+ x z z₁ v))

module +ReduceRelationDoubleZero where
  data _+_~>_ : (x y z : ℕ) → Set where
    zero+ : (x : ℕ) → 0 + x ~> x
    +zero : (x : ℕ) → suc x + 0 ~> suc x
    suc+suc : (x y z : ℕ) → x + y ~> z → suc x + suc y ~> suc (suc z)

  +~>total : (x y : ℕ) → ∃ (λ z → x + y ~> z)
  +~>total zero y = lo y (zero+ y)
  +~>total (suc x) zero = lo (suc x) (+zero x)
  +~>total (suc x) (suc y) =
    let lo item dep = +~>total x y
    in lo (suc (suc item)) (suc+suc x y item dep)

  +~>unique : (x y z r : ℕ) → x + y ~> z → x + y ~> r → z ≡ r
  +~>unique .0 r .r .r (zero+ .r) (zero+ .r) = refl
  +~>unique .(suc x) .0 .(suc x) .(suc x) (+zero x) (+zero .x) = refl
  +~>unique .(suc x) .(suc y) .(suc (suc z₁)) .(suc (suc z)) (suc+suc x y z₁ p) (suc+suc .x .y z q)
    rewrite +~>unique x y z₁ z p q = refl

  _+'_ : (x y : ℕ) → ℕ
  x +' y = ∃.item (+~>total x y)

  0+ : (x : ℕ) → 0 + x ~> x
  0+ x = zero+ x

  +0 : (x : ℕ) → x + 0 ~> x
  +0 zero = zero+ zero
  +0 (suc x) = +zero x

  0+' : (x : ℕ) → 0 +' x ≡ x
  0+' x = refl

  +'0 : (x : ℕ) → x +' 0 ≡ x
  +'0 zero = refl
  +'0 (suc x) = refl

  +comm : (x y z : ℕ) → x + y ~> z → y + x ~> z
  +comm .0 z .z (zero+ .z) = +0 z
  +comm .(suc x) .0 .(suc x) (+zero x) = zero+ (suc x)
  +comm .(suc x) .(suc y) .(suc (suc z)) (suc+suc x y z p) = suc+suc y x z (+comm x y z p)

  sucl : (x y z : ℕ) → x + y ~> z → suc x + y ~> suc z
  sucl .0 zero .0 (zero+ .0) = +zero zero
  sucl .0 (suc z) .(suc z) (zero+ .(suc z)) = suc+suc zero z z (zero+ z)
  sucl .(suc x) .0 .(suc x) (+zero x) = +zero (suc x)
  sucl .(suc x) .(suc y) .(suc (suc z)) (suc+suc x y z p) = suc+suc (suc x) y (suc z) (sucl x y z p)

  sucr : (x y z : ℕ) → x + y ~> z → x + suc y ~> suc z
  sucr .0 z .z (zero+ .z) = zero+ (suc z)
  sucr .1 .0 .1 (+zero zero) = suc+suc zero zero zero (zero+ zero)
  sucr .(suc (suc x)) .0 .(suc (suc x)) (+zero (suc x)) = suc+suc (suc x) zero (suc x) (+zero x)
  sucr .(suc x) .(suc y) .(suc (suc z)) (suc+suc x y z p) = suc+suc x (suc y) (suc z) (sucr x y z p)

  suc-swap : (x y z : ℕ) → suc x + y ~> z → x + suc y ~> z
  suc-swap zero .0 .1 (+zero .0) = zero+ (suc zero)
  suc-swap (suc zero) .0 .2 (+zero .1) = suc+suc zero zero zero (zero+ zero)
  suc-swap (suc (suc x)) .0 .(suc (suc (suc x))) (+zero .(suc (suc x))) = suc+suc (suc x) zero (suc x) (+zero x)
  suc-swap .0 .(suc z) .(suc (suc z)) (suc+suc .0 z .z (zero+ .z)) = zero+ (suc (suc z))
  suc-swap .(suc x) .1 .(suc (suc (suc x))) (suc+suc .(suc x) .0 .(suc x) (+zero x)) = suc+suc x (suc zero) (suc x) (suc-swap x zero (suc x) (+zero x))
  suc-swap .(suc x) .(suc (suc y)) .(suc (suc (suc (suc z)))) (suc+suc .(suc x) .(suc y) .(suc (suc z)) (suc+suc x y z x₁)) = suc+suc x (suc (suc y)) (suc (suc z)) (suc-swap x (suc y) (suc (suc z)) (suc+suc x y z x₁))

  +assoc : (x y r s t z : ℕ)
    → x + y ~> r
    → r + z ~> t
    → y + z ~> s
    → x + s ~> t
  +assoc .0 .0 .0 s .s .s (zero+ .0) (zero+ .s) (zero+ .s) = zero+ s
  +assoc .0 .(suc x) .(suc x) .(suc x) .(suc x) .0 (zero+ .(suc x)) (+zero x) (+zero .x) = zero+ (suc x)
  +assoc .0 .(suc x) .(suc x) .(suc (suc z)) .(suc (suc z₁)) .(suc y) (zero+ .(suc x)) (suc+suc x y z₁ q) (suc+suc .x .y z v)
    rewrite +~>unique x y z₁ z q v = zero+ (suc (suc z))
  +assoc .(suc x) .0 .(suc x) .0 .(suc x) .0 (+zero x) (+zero .x) (zero+ .0) = +zero x
  +assoc .(suc x) .0 .(suc x) .(suc y) .(suc (suc z)) .(suc y) (+zero x) (suc+suc .x y z q) (zero+ .(suc y)) = suc+suc x y z q
  +assoc .(suc x₁) .(suc x) .(suc (suc z)) .(suc x) .(suc (suc z)) .0 (suc+suc x₁ x z p) (+zero .(suc z)) (+zero .x) = suc+suc x₁ x z p
  +assoc .(suc x) .(suc y) .(suc (suc z₁)) .(suc (suc z)) .(suc (suc z₂)) .(suc y₁) (suc+suc x y z₁ p) (suc+suc .(suc z₁) y₁ z₂ q) (suc+suc .y .y₁ z v) = suc+suc x (suc z) z₂ (+assoc x y z₁ (suc z) z₂ (suc y₁) p (suc-swap z₁ y₁ z₂ q) (sucr y y₁ z v))