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
94
95
96
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 ∎
|
