{-# OPTIONS --safe #-}

module Problem13 where

open import Data.Empty using (⊥-elim)
open import Data.Fin hiding (_≟_; _+_; _<_; _>_; _≤_)
open import Data.Fin.Properties hiding (_≟_; ≤-trans)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.Properties
open import Data.Product
open import Data.Unit using (tt)
open import Data.Vec
open import Function.Base using (_$′_)
open import Relation.Nullary.Decidable
open import Relation.Binary.PropositionalEquality

open ≤-Reasoning renaming (begin_ to begin-≤_)

okToDivide : ∀ n → n > 1 → False (n ≟ 0)
okToDivide (suc n) p = tt

toRadix : (n : ℕ)(nz : n > 1) → (f : ℕ) → ℕ → Vec (Fin n) f
toRadix n nz zero k = []
toRadix n nz (suc f) k with (k divMod n) {okToDivide _ nz}
... | result q r prf₂ = r ∷ toRadix n nz f q

fromRadix : (n : ℕ) {f : ℕ} → Vec (Fin n) f → ℕ
fromRadix n [] = 0
fromRadix n (x ∷ xs) = toℕ x + n * fromRadix n xs

goal₁ : (n : ℕ)(nz : n > 1){f : ℕ}(num : Vec (Fin n) f)
      → toRadix n nz f (fromRadix n num) ≡ num
goal₁ n nz [] = refl
goal₁ n nz (x ∷ xs) with ((toℕ x + n * fromRadix n xs) divMod n) {okToDivide _ nz}
... | result q r prf =
  let (prf₁ , prf₂) = invertProof x r (fromRadix n xs) q prf in
  cong₂ _∷_ (sym prf₁) (trans (sym (cong (toRadix n nz _) prf₂)) (goal₁ n nz xs))
  where
  invertProof : (x y : Fin n) (p q : ℕ) → toℕ x + n * p ≡ toℕ y + q * n → x ≡ y × p ≡ q
  invertProof x y zero zero    prf .proj₁ =
    toℕ-injective $′ +-cancelʳ-≡ (toℕ x) (toℕ y) $′ begin-equality
      toℕ x + n * zero ≡⟨  prf ⟩
      toℕ y + zero     ≡˘⟨ cong (toℕ y +_) (*-zeroʳ n) ⟩
      toℕ y + n * zero ∎
  invertProof x y zero zero    prf .proj₂ = refl
  invertProof x y zero (suc q) prf =
    ⊥-elim $′ <⇒≱ (toℕ<n x) $′ begin-≤
               n          ≤⟨  m≤m+n n (q * n) ⟩
               n + q * n  ≤⟨  m≤n+m (n + q * n) (toℕ y) ⟩
      toℕ y + (n + q * n) ≡˘⟨ prf ⟩
      toℕ x + n * zero    ≡⟨  cong (toℕ x +_) (*-zeroʳ n) ⟩
      toℕ x + zero        ≡⟨  +-identityʳ (toℕ x) ⟩
      toℕ x               ∎
  invertProof x y (suc p) zero    prf =
    ⊥-elim $′ <⇒≱ (toℕ<n y) $′ begin-≤
               n          ≤⟨ m≤m+n n (p * n) ⟩
               n + p * n  ≡⟨ *-comm (suc p) n ⟩
               n * suc p  ≤⟨ m≤n+m (n * suc p) (toℕ x) ⟩
      toℕ x + (n * suc p) ≡⟨ prf ⟩
      toℕ y + zero        ≡⟨ +-identityʳ (toℕ y) ⟩
      toℕ y               ∎
  invertProof x y (suc p) (suc q) prf =
    map₂ (cong suc) $′
    invertProof x y p q $′
    +-cancelʳ-≡ (toℕ x + n * p) (toℕ y + q * n) $′ begin-equality
      toℕ x +  n * p + n  ≡⟨  +-assoc (toℕ x) (n * p) n ⟩
      toℕ x + (n * p + n) ≡⟨  cong (λ ◌ → toℕ x + (◌ + n)) (*-comm n p) ⟩
      toℕ x + (p * n + n) ≡⟨  cong (toℕ x +_) (+-comm (p * n) n) ⟩
      toℕ x + (n + p * n) ≡⟨  cong (toℕ x +_) (*-comm (suc p) n) ⟩
      toℕ x + (n * suc p) ≡⟨  prf ⟩
      toℕ y + (n + q * n) ≡⟨  cong (toℕ y +_) (+-comm n (q * n)) ⟩
      toℕ y + (q * n + n) ≡˘⟨ +-assoc (toℕ y) (q * n) n ⟩
      toℕ y +  q * n + n  ∎


goal₂ : (n : ℕ)(nz : n > 1)(f : ℕ)(k : ℕ)(p : k < n ^ f)
      → fromRadix n (toRadix n nz f k) ≡ k
goal₂ n nz zero    k k<n^0   = sym $′ n<1⇒n≡0 k<n^0
goal₂ n nz (suc f) k k<n*n^f with (k divMod n) {okToDivide _ nz}
... | result q r prf = begin-equality
  toℕ r + n * fromRadix n (toRadix n nz f q) ≡⟨  cong (λ ◌ → toℕ r + n * ◌) (goal₂ n nz f q q<n^f) ⟩
  toℕ r + n * q                              ≡⟨  cong (toℕ r +_) (*-comm n q) ⟩
  toℕ r + q * n                              ≡˘⟨ prf ⟩
  k                                          ∎
  where
  q<n^f : q < n ^ f
  q<n^f = *-cancelˡ-< n $′ begin-strict
            n * q ≡⟨  *-comm n q ⟩
            q * n ≤⟨  m≤n+m (q * n) (toℕ r) ⟩
    toℕ r + q * n ≡˘⟨ prf ⟩
    k             <⟨  k<n*n^f ⟩
    n * n ^ f     ∎