From 4527250aee1d1d4655e84f0583d04410b7c53642 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 22 Jan 2024 11:51:56 +0000
Subject: Advent of proof submissions.

Completed all problems save 12, where I had to postulate two lemma.
---
 src/Problem4.agda | 97 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 97 insertions(+)
 create mode 100644 src/Problem4.agda

(limited to 'src/Problem4.agda')

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                              ∎
-- 
cgit v1.2.3