blob: 53cc17862fec02f5d41de18ec7c1159f65934d29 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
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 ∎
|
