import data.finset
def list.part_sums : (list ℕ) → (list ℕ)
| [] := [0]
| (a::as) := 0::(as.part_sums.map (+ a))
theorem grasshopper_aux :
forall n : ℕ,
forall jumps : list ℕ,
let size := jumps.sum in
forall mines : list ℕ,
(list.sorted (>) jumps) → mines.length < n → jumps.length = n →
(forall jump ∈ jumps, 0 < jump) → (forall mine ∈ mines, 0 < mine)
→
exists jumps_l : list ℕ,
jumps ~ jumps_l ∧
forall jump ∈ jumps_l.part_sums, forall mine ∈ mines,
mine < size → jump ≠ mine
:=
begin
assume n,
induction n with n n_ih, -- zero case is trivial
intros,
have : list.length mines < 0, by assumption,
have : ¬list.length mines < 0, by apply nat.not_lt_zero,
contradiction,
intros, -- inductive case
cases jumps with J other_jumps,
contradiction, -- jumps is empty
cases (classical.em (J ∈ mines)) with mine_on_J,
sorry,
cases (classical.em (∃ mine ∈ mines, mine < J)) with mine_before,
let other_mines := list.filter_map (
assume mine, if mine < J then none else some (mine-J)
) mines,
have : other_mines.length < n, from
sorry,
-- take the biggest jump J,
-- if all mines before J, easy
-- push all mines strictly before J by J to the right
-- remove the first mine, apply J, use induction
-- if unshifted mine was visited, swap the first two jumps
/- if m < J and no mine on J,
perform J as the first jump and use induction -/
/- if mine on J, add J to all mines before J,
perform J as the first jump, use induction, and
swap the first two jumps -/
/- if m > J, remove m, perform J as the first jump,
use induction, and if m was visited, -/
sorry
end
theorem grasshopper :
forall jumps : list ℕ,
let size := jumps.sum in
forall mines : list ℕ,
( jumps.nodup ∧ mines.length < jumps.length ∧
(forall mine ∈ mines, 0 < mine ∧ mine < size) ∧
(forall jump ∈ jumps, 0 < jump))
→
exists jumps_l : list ℕ,
jumps ~ jumps_l ∧
forall jump ∈ jumps_l.part_sums, forall mine ∈ mines, jump ≠ mine
:= sorry