I agree 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.
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.
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
theory Submission imports Defs begin text ‹Task 1 (1/10 points)› theorem G_L: "G ⊆ L" sorry text ‹Task 2 (9/10 points)› theorem L_G: "L ⊆ G" sorry end
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
-- 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⟩
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
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
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.
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)].
Admitted.
End HillClimbing.
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
theory Submission imports Defs begin text ‹Task 1 (1/10 points)› theorem G_L: "G ⊆ L" sorry text ‹Task 2 (9/10 points)› theorem L_G: "L ⊆ G" sorry end
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
-- Lean version: 3.16.2
-- Mathlib version: eb5b7fb7f406385cd1f2efaa15d9c0923541b955
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⟩
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
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
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
theory Submission imports Defs begin text ‹Task 1 (1/10 points)› theorem G_L: "G ⊆ L" sorry text ‹Task 2 (9/10 points)› theorem L_G: "L ⊆ G" sorry end
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