Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

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     ∎