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 + 0)
  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