diff options
Diffstat (limited to 'src/Problem13.agda')
| -rw-r--r-- | src/Problem13.agda | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/src/Problem13.agda b/src/Problem13.agda new file mode 100644 index 0000000..53cc178 --- /dev/null +++ b/src/Problem13.agda @@ -0,0 +1,93 @@ +{-# 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 ∎ |