{-# 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                              ∎