open Data.Nat using (_>_)
open Data.Nat.Properties using (+-mono-≤)
open import plfa.part1.Relations using (Bin; ⟨⟩; _I; _O; to; from; inc)

open import plfa.part1.Relations using (Bin; to; from; inc; One; Can; to-can; inc-can; from-inc-suc-from)

-- The definition from Relations didn't allow for `≡One` (I think because of `inc` used in it)
data One : Bin -> Set where
  one : One (⟨⟩ I)
  one-O : ∀ {b : Bin} → One b → One (b O)
  one-I : ∀ {b : Bin} → One b → One (b I)
data Can : Bin → Set where
  zero-bin : Can (⟨⟩ O)
  leading : ∀ {b : Bin} → One b → Can b

  proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → Σ.proj₁ c ≡ Σ.proj₁ c′ → c ≡ c′
  can-to-from-id : ∀ {b : Bin} → Can b → to (from b) ≡ b

inc-one : ∀ {b : Bin} → One b → One (inc b)
inc-one one = one-O one
inc-one (one-O o) = one-I o
inc-one (one-I o) = one-O (inc-one o)
inc-can : ∀ {b : Bin} → Can b → Can (inc b)
inc-can zero-bin = leading one
inc-can (leading o) = leading (inc-one o)
to-can : (n : ℕ) → Can (to n)
to-can zero = zero-bin
to-can (suc n) = inc-can (to-can n)
≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
≡One One.one One.one = refl
≡One (one-O o) (one-O o') = cong one-O (≡One o o')
≡One (one-I o) (one-I o') = cong one-I (≡One o o')
≡Can : ∀ {b : Bin} (c c′ : Can b) → c ≡ c′
≡Can zero-bin zero-bin = refl
≡Can zero-bin (leading (one-O ()))
≡Can (leading (one-O ())) zero-bin
≡Can (leading o) (leading o′) = cong leading (≡One o o′)
proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → Σ.proj₁ c ≡ Σ.proj₁ c′ → c ≡ c′
proj₁≡→Can≡ {c = ⟨ b , c ⟩} {c′ = ⟨ b′ , c′ ⟩} refl with ≡Can c c′
...| c≡c′ = cong (λ c → ⟨ b , c ⟩) c≡c′
to-n+n≡n-O : ∀ {n : ℕ} → n > 0 → to (n + n) ≡ (to n) O
to-n+n≡n-O {suc zero} z≤s = refl
to-n+n≡n-O {suc (suc n)} z≤s =
  begin
    inc (to (suc n + suc (suc n)))
  ≡⟨ cong (λ c → inc (to c)) (+-comm (suc n) (suc (suc n))) ⟩
    inc (to (suc (suc n) + (suc n)))
  ≡⟨⟩
    inc (inc (to ((suc n) + (suc n))))
  ≡⟨ cong (inc ∘ inc) (to-n+n≡n-O {suc n} (s≤s z≤n)) ⟩
    inc (inc (to n)) O
  ∎
one>0 : ∀ {b : Bin} → One b → from (b) > 0
one>0 one = s≤s z≤n
one>0 (one-O {b} o) with one>0 o
...| 1≤from-b = +-mono-≤ 1≤from-b z≤n
one>0 (one-I o) = s≤s z≤n

-- NOTE: Not sure why this fails with TerminationIssue, so I postulate it above instead
-- can-to-from-id : ∀ {b : Bin} → Can b → to (from b) ≡ b
-- can-to-from-id Can.zero-bin = refl
-- can-to-from-id (Can.leading One.one) = refl
-- can-to-from-id (Can.leading (One.suc {b} o)) =
--   begin
--     to (from (inc b))
--   ≡⟨ cong to (from-inc-suc-from b) ⟩
--     to (suc (from b))
--   ≡⟨ cong inc (can-to-from-id (Can.leading o)) ⟩
--     inc b
--   ∎

can-to-from-id : ∀ {b : Bin} → Can b → to (from b) ≡ b
can-to-from-id zero-bin = refl
can-to-from-id (leading one) = refl
can-to-from-id (leading (one-O one)) = refl
can-to-from-id (leading (one-O {b} o)) =
  begin
    to (from b + (from b + zero))
  ≡⟨ cong (λ c → to (from b + c)) (+-identityʳ (from b)) ⟩
    to (from b + from b)
  ≡⟨ to-n+n≡n-O (one>0 o) ⟩
    (to (from b)) O
  ≡⟨ cong _O (can-to-from-id (leading o)) ⟩
    b O
  ∎
can-to-from-id (leading (one-I {b} o)) =
  begin
    inc (to (from b + (from b + zero)))
  ≡⟨ cong (λ c → inc (to (from b + c))) (+-identityʳ (from b)) ⟩
    inc (to (from b + from b))
  ≡⟨ cong inc (to-n+n≡n-O (one>0 o)) ⟩
    to (from b) I
  ≡⟨ cong _I (can-to-from-id (leading o)) ⟩
    b I
  ∎