diff options
Diffstat (limited to 'src/Problem4.agda')
| -rw-r--r-- | src/Problem4.agda | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/src/Problem4.agda b/src/Problem4.agda new file mode 100644 index 0000000..3215dd0 --- /dev/null +++ b/src/Problem4.agda @@ -0,0 +1,97 @@ +{-# OPTIONS --safe #-} + +module Problem4 where + +open import Data.Integer renaming (suc to sucℤ; pred to predℤ) hiding (_≤_) +open import Data.Nat renaming (_+_ to _ℕ+_) +open import Data.Nat.Properties using ( +-monoʳ-≤; +-monoˡ-≤; +-suc; ≤-trans; module ≤-Reasoning ) +open import Data.Integer.Properties using ( +-inverseʳ ) +open import Data.Product +open import Relation.Binary.PropositionalEquality +-- The theorems explicitly imported above were useful to prove this! + +-- the below theorems are just used to prove the helpers +open import Data.Integer.Properties using ( ∣m+n∣≤∣m∣+∣n∣; +-assoc; neg-distrib-+; +-comm; +-identityʳ ) + +Point = ℤ × ℤ + +up : Point → Point +up (x , y) = (x , sucℤ y) +down : Point → Point +down (x , y) = (x , predℤ y) +left : Point → Point +left (x , y) = (predℤ x , y) +right : Point → Point +right (x , y) = (sucℤ x , y) + +data OrthoPath (p : Point) : Point → Set where + move-up : ∀ {q} → OrthoPath (up p) q → OrthoPath p q + move-down : ∀ {q} → OrthoPath (down p) q → OrthoPath p q + move-left : ∀ {q} → OrthoPath (left p) q → OrthoPath p q + move-right : ∀ {q} → OrthoPath (right p) q → OrthoPath p q + stop : OrthoPath p p + +path-length : ∀{p q} → OrthoPath p q → ℕ +path-length (move-up p) = suc (path-length p) +path-length (move-down p) = suc (path-length p) +path-length (move-left p) = suc (path-length p) +path-length (move-right p) = suc (path-length p) +path-length stop = 0 + +manhattan : Point → Point → ℕ +manhattan (x₁ , y₁) (x₂ , y₂) = ∣ (x₂ - x₁) ∣ ℕ+ ∣ (y₂ - y₁) ∣ + +helper-sucℤ : ∀(a b : ℤ) → ∣ (a - b) ∣ ≤ suc ∣ (a - sucℤ b) ∣ +helper-sucℤ a b rewrite + sym (+-identityʳ (- b)) + | sym (+-assoc (- b) (- 1ℤ) 1ℤ) + | sym (+-comm (- 1ℤ) (- b)) + | sym (neg-distrib-+ 1ℤ b) + | sym (+-assoc a (- sucℤ b) 1ℤ) + | +-comm (a - sucℤ b) 1ℤ + = ∣m+n∣≤∣m∣+∣n∣ (1ℤ) (a - sucℤ b) + +helper-predℤ : ∀(a b : ℤ) → ∣ (a - b) ∣ ≤ suc ∣ (a - predℤ b) ∣ +helper-predℤ a b rewrite + sym (+-identityʳ (- b)) + | sym (+-assoc (- b) 1ℤ -1ℤ) + | sym (+-comm 1ℤ (- b)) + | sym (neg-distrib-+ -1ℤ b) + | sym (+-assoc a (- predℤ b) -1ℤ ) + | +-comm (a - predℤ b) -1ℤ + = ∣m+n∣≤∣m∣+∣n∣ (-1ℤ) (a - predℤ b) + +open ≤-Reasoning + +goal : ∀(p q : Point) → (path : OrthoPath p q) → manhattan p q ≤ path-length path +goal p@(px , py) q@(qx , qy) (move-up path) = begin + manhattan p q ≡⟨⟩ + ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣ ≤⟨ +-monoʳ-≤ ∣ (qx - px) ∣ (helper-sucℤ qy py) ⟩ + ∣ (qx - px) ∣ ℕ+ suc ∣ (qy - sucℤ py) ∣ ≡⟨ +-suc ∣ (qx - px) ∣ ∣ (qy - sucℤ py) ∣ ⟩ + suc ∣ (qx - px) ∣ ℕ+ ∣ (qy - sucℤ py) ∣ ≡⟨⟩ + suc (manhattan (up p) q) ≤⟨ s≤s (goal (up p) q path) ⟩ + suc (path-length path) ∎ +goal p@(px , py) q@(qx , qy) (move-down path) = begin + manhattan p q ≡⟨⟩ + ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣ ≤⟨ +-monoʳ-≤ ∣ (qx - px) ∣ (helper-predℤ qy py) ⟩ + ∣ (qx - px) ∣ ℕ+ suc ∣ (qy - predℤ py) ∣ ≡⟨ +-suc ∣ (qx - px) ∣ ∣ (qy - predℤ py) ∣ ⟩ + suc ∣ (qx - px) ∣ ℕ+ ∣ (qy - predℤ py) ∣ ≡⟨⟩ + suc (manhattan (down p) q) ≤⟨ s≤s (goal (down p) q path) ⟩ + suc (path-length path) ∎ +goal p@(px , py) q@(qx , qy) (move-left path) = begin + manhattan p q ≡⟨⟩ + ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣ ≤⟨ +-monoˡ-≤ ∣ (qy - py) ∣ (helper-predℤ qx px) ⟩ + suc ∣ (qx - predℤ px) ∣ ℕ+ ∣ (qy - py) ∣ ≡⟨⟩ + suc (manhattan (left p) q) ≤⟨ s≤s (goal (left p) q path) ⟩ + suc (path-length path) ∎ +goal p@(px , py) q@(qx , qy) (move-right path) = begin + manhattan p q ≡⟨⟩ + ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣ ≤⟨ +-monoˡ-≤ ∣ (qy - py) ∣ (helper-sucℤ qx px) ⟩ + suc ∣ (qx - sucℤ px) ∣ ℕ+ ∣ (qy - py) ∣ ≡⟨⟩ + suc (manhattan (right p) q) ≤⟨ s≤s (goal (right p) q path) ⟩ + suc (path-length path) ∎ +goal p@(px , py) .p stop = begin + manhattan p p ≡⟨⟩ + ∣ (px - px) ∣ ℕ+ ∣ (py - py) ∣ ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → ∣ ◌ᵃ ∣ ℕ+ ∣ ◌ᵇ ∣) (+-inverseʳ px) (+-inverseʳ py) ⟩ + 0 ℕ+ 0 ≡⟨⟩ + 0 ∎ |