Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Hill Climbing

During a trip in the alps Stefan was thinking about how to find a hill — i.e. a local maximum in altitude — in an efficient way. Following steepest ascent could mean checking every position once. Back home he had an idea for a divide-and-conquer program that minimizes querying height positions with a satellite. While implementing, he thought about whether there will always be such a local maximum. As he does not want to think about the proof, he delegates it to you.

Given an rectangular area of the map (`lx < x < ux` and `ly < y < uy`) with at least one position higher than the border, prove that there is a position that is higher than any of its adjacent positions (north, west, south, east). You can assume that all heights are distinct.

Thanks to Maximilian Haslbeck for stating the problem. Thanks to Armaël Guéneau and Kevin Kappelmann for translating.

## Resources

### Definitions File

```theory Defs
imports Main
begin

definition onborder where
"onborder lx ux ly uy ix iy ≡ ( (ix=lx ∨ ix=ux) ∧ ly≤iy ∧ iy≤uy)  ∨
( (iy=ly ∨ iy=uy) ∧ lx≤ix ∧ ix≤ux)"

definition within where
"within lx ux ly uy ix iy ≡ ( ly<iy ∧ iy<uy ∧ lx<ix ∧ ix<ux)"

lemma "within lx ux ly uy ix iy ⟷ (ix,iy) ∈ {lx<..<ux} × {ly<..<uy}"
unfolding within_def by auto

end```

### Template File

```theory Submission
imports Defs
begin

lemma has_global_maximum:
fixes terrain :: "int ⇒ int ⇒ nat"
and (* delimiters *) lx ux ly uy :: int
and (* one element *) ix iy :: int
assumes  w: "within lx ux ly uy ix iy"
and distinct: "⋀ax ay bx by. (ax,ay) ≠ (bx,by) ⟹ terrain ax ay ≠ terrain bx by"
and border: "⋀bx by. onborder lx ux ly uy bx by ⟹ terrain bx by < terrain ix iy"
shows "∃tx ty. within lx ux ly uy tx ty ∧
(∀d∈{(0,1),(1,0),(-1,0),(0,-1)}. terrain tx ty > terrain (tx+fst d) (ty+snd d))"
sorry

end```

### Check File

```theory Check
imports Submission
begin

lemma has_global_maximum:
fixes terrain :: "int ⇒ int ⇒ nat"
and (* delimiters *) lx ux ly uy :: int
and (* one element *) ix iy :: int
assumes  w: "within lx ux ly uy ix iy"
and distinct: "⋀ax ay bx by. (ax,ay) ≠ (bx,by) ⟹ terrain ax ay ≠ terrain bx by"
and border: "⋀bx by. onborder lx ux ly uy bx by ⟹ terrain bx by < terrain ix iy"
shows "∃tx ty. within lx ux ly uy tx ty ∧
(∀d∈{(0,1),(1,0),(-1,0),(0,-1)}. terrain tx ty > terrain (tx+fst d) (ty+snd d))"
using assms apply(rule has_global_maximum) by assumption

end```

### Definitions File

```-- Lean version: 3.4.2
-- Mathlib version: 2019-09-11

structure rectangle := (lx ux ly uy : ℤ)

structure ipos := (x y : ℤ)

namespace ipos

-- check if x y is on one of the borders of the rectangles
def on_border (r : rectangle) (p : ipos) :=
((p.x = r.lx ∨ p.x = r.ux) ∧ r.ly ≤ p.y ∧ p.y ≤ r.uy) ∨ -- on the upper or lower border
((p.y = r.ly ∨ p.y = r.uy) ∧ r.lx ≤ p.x ∧ p.x ≤ r.ux) -- on the left or right border

-- check if x y is inside the rectangle
def within (r : rectangle) (p : ipos) := r.ly < p.y ∧ p.y < r.uy ∧ r.lx < p.x ∧ p.x < r.ux

end ipos

-- the goal used in submission
notation `GOAL` :=
∀ {terrain : ipos → ℕ} {r : rectangle} {p : ipos},
(p.within r) →
(∀ p1 p2, p1 ≠ p2 → terrain p1 ≠ terrain p2) →
(∀ (p' : ipos), p'.on_border r → terrain p' < terrain p) →
∃ (p' : ipos), p'.within r ∧
∀ (d ∈ ({(0, 1), (1, 0),(-1, 0), (0, -1)} : set (ℤ × ℤ))),
terrain p' > terrain ⟨p'.x + prod.fst d, p'.y + prod.snd d⟩```

### Template File

```import .defs

lemma has_global_maximum {terrain : ipos → ℕ} {r : rectangle} {p : ipos}
(hyp_within : p.within r)
(hyp_distinct : ∀ p1 p2, p1 ≠ p2 → terrain p1 ≠ terrain p2)
(hyp_border : ∀ (p' : ipos), p'.on_border r → terrain p' < terrain p) :
∃ (p' : ipos), p'.within r ∧
∀ (d ∈ ({(0, 1), (1, 0),(-1, 0), (0, -1)} : set (ℤ × ℤ))),
terrain p' > terrain ⟨p'.x + prod.fst d, p'.y + prod.snd d⟩ :=
sorry```

### Check File

```import .defs
import .submission

lemma maximum_fun {terrain : ipos → ℕ} {r : rectangle} {p : ipos}
(hyp_within : p.within r)
(hyp_distinct : ∀ p1 p2, p1 ≠ p2 → terrain p1 ≠ terrain p2)
(hyp_border : ∀ (p' : ipos), p'.on_border r → terrain p' < terrain p) :
∃ (p' : ipos), p'.within r ∧
∀ (d ∈ ({(0, 1), (1, 0),(-1, 0), (0, -1)} : set (ℤ × ℤ))),
terrain p' > terrain ⟨p'.x + prod.fst d, p'.y + prod.snd d⟩ :=
has_global_maximum hyp_within hyp_distinct hyp_border```

### Definitions File

```Require Export ZArith Psatz Lia.
Require Export List.
Export ListNotations.
Open Scope Z_scope.

Notation pos := (Z * Z)%type.

(*
(ux, uy)
+-----------+
|           |
|           |
+-----------+
(lx, ly)
*)

Record rect := mkrect {
(* bottom left corner *)
lx : Z; ly : Z;
(* upper right corner *)
ux : Z; uy : Z;
}.

Inductive on_border : pos -> rect -> Prop :=
| On_horizontal_border : forall x y lx ly ux uy,
(* on the upper or lower border *)
(x = lx \/ x = ux) /\
ly <= y /\
y <= uy
->
on_border (x, y) (mkrect lx ly ux uy)
| On_vertical_border : forall x y lx ly ux uy,
(* on the left or right border *)
(y = ly \/ y = uy) /\
lx <= x /\
x <= ux
->
on_border (x, y) (mkrect lx ly ux uy).

Definition within '(x, y) (r: rect) :=
ly r < y /\
y < uy r /\
lx r < x /\
x < ux r.```

### Template File

```Require Import Defs.

Section HillClimbing.

Variable terrain : pos -> nat.
Variable r : rect.
Variables x y : Z.

Hypothesis p_within_r : within (x,y) r.
Hypothesis distinct : forall p1 p2, p1 <> p2 -> terrain p1 <> terrain p2.
Hypothesis border : forall x' y',
on_border (x', y') r ->
(terrain (x', y') < terrain (x, y))%nat.

Theorem has_global_maximum :
exists tx ty,
within (tx, ty) r /\
Forall (fun '(dx, dy) => terrain (tx, ty) > terrain (tx + dx, ty + dy)%Z)%nat
[(0,1); (1,0); (-1,0); (0, -1)].