module Data.Counter where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

data Counter (n : ℕ) : Set where
  cut : (i j : ℕ) → (i+j+1=n : suc (i + j) ≡ n) → Counter n

private
  -- todo: use proofs from std lib
  i+0 : {i : ℕ} → i ≡ (i + )
  i+0 {zero} = refl
  i+0 {suc n} = cong suc i+0

  suc→ : ∀ {i j} → suc ((suc i) + j) ≡ suc (i + (suc j))
  suc→ {zero} = refl
  suc→ {suc i} = cong suc (suc→ {i})

_+1 : ∀ {n} → Counter n → Counter n
(cut  i  zero     i+1=n)    +1  = cut  zero     i  (trans (cong suc i+0) i+1=n)
(cut  i  (suc j)  i+j+2=n)  +1  = cut  (suc i)  j  (trans (suc→ {i}) i+j+2=n)

_-1 : ∀ {n} → Counter n → Counter n
(cut  zero     j  j+1=n)    -1  = cut  j  zero     (trans (sym (cong suc i+0)) j+1=n)
(cut  (suc i)  j  i+j+2=n)  -1  = cut  i  (suc j)  (trans (sym (suc→ {i})) i+j+2=n)

+1-1 : ∀ {n} → {k : Counter n} → k +1 -1 ≡ k
+1-1  {k = cut  i        zero     _}  = cong  (cut  i        zero)     (proof-irrelevance _ _)
+1-1  {k = cut  i        (suc j)  _}  = cong  (cut  i        (suc j))  (proof-irrelevance _ _)

-1+1 : ∀ {n} → {k : Counter n} → k -1 +1 ≡ k
-1+1  {k = cut  zero     j        _}  = cong  (cut  zero     j)  (proof-irrelevance _ _)
-1+1  {k = cut  (suc i)  j        _}  = cong  (cut  (suc i)  j)  (proof-irrelevance _ _)

private
  open import Data.Nat.Show renaming (show to showℕ)
  open import Data.String

show : ∀ {n} → Counter n → String
show (cut i _ _) = showℕ i