Cookies disclaimer

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.

[Proof Ground 2019] 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

Download Files

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

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

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
Download Files

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
Download Files

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)].
Admitted.

End HillClimbing.
Download Files

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

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

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
Download Files

Definitions File

-- 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⟩

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
Download Files

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

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

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

Terms and Conditions