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
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