module Data.CounterIndexed where

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

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

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    +1 = subst Counter i+0 (cut zero i)
cut i (suc j) +1 = subst Counter (suc→ {i}) (cut (suc i) j)

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

open import Relation.Binary.HeterogeneousEquality using (_≅_; refl; ≡-subst-removable; ≅-to-≡)

private
  Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
                 {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
                 n ≡ n′ → k ≅ k′ → f k ≅ f k′
  Counter-cong f refl refl = refl

  open Relation.Binary.HeterogeneousEquality.≅-Reasoning using (begin_; _∎; _≅⟨_⟩_; _≡⟨_⟩_)
  open import Function

  +1-1₀ : ∀ {n} → (k : Counter n) → k +1 -1 ≅ k
  +1-1₀ (cut zero    zero)    = refl
  +1-1₀ (cut zero    (suc j)) = refl
  +1-1₀ (cut (suc i) zero) =
    begin
      cut (suc i) zero +1 -1
    ≡⟨ refl ⟩
      (subst Counter i+0 (cut zero (suc i))) -1
    ≅⟨ Counter-cong _-1 (cong (suc ∘ suc) (sym (i+0 {i}))) (≡-subst-removable Counter i+0 (cut zero (suc i))) ⟩
      (cut zero (suc i)) -1
    ≡⟨ refl ⟩
      subst Counter (sym i+0) (cut (suc i) zero)
    ≅⟨ ≡-subst-removable Counter (sym i+0) (cut (suc i) zero) ⟩
      cut (suc i) zero
    ∎
  +1-1₀ (cut (suc i) (suc j)) =
    begin
      cut (suc i) (suc j) +1 -1
    ≡⟨ refl ⟩
      subst Counter (suc→ {suc i}) (cut (suc (suc i)) j) -1
    ≅⟨ Counter-cong _-1 (cong suc (sym (suc→ {i}))) (≡-subst-removable Counter (suc→ {suc i}) (cut (suc (suc i)) j)) ⟩
      cut (suc (suc i)) j -1
    ≅⟨ refl ⟩
      subst Counter (sym (suc→ {suc i})) (cut (suc i) (suc j))
    ≅⟨ ≡-subst-removable Counter (sym (suc→ {suc i})) (cut (suc i) (suc j)) ⟩
      cut (suc i) (suc j)
    ∎

+1-1 : ∀ {n} → {k : Counter n} → k +1 -1 ≡ k
+1-1 = ≅-to-≡ (+1-1₀ _)