Library problem

Puzzle: Escaping the death plank (EDP)

A pirate has taken you captive and is forcing you to walk the plank!
The plank is three paces wide, and you begin in the center, from where taking either two steps to the right or two to the left will send you plunging into the cold seas (it's not your standard pirate's plank, I know).
The pirate forces you to write down a planned list of steps you will take. Each step must be either a step to the right, or a step to the left. The pirate will force you to take these steps, but not necessarily exactly as you gave them. He also may force you to take every second step (starting with the second step), or every third step (starting with the third), and so on.
Nevertheless, if he reaches the end of the list before you have fallen to your death, he will let you go. Are you able to avoid sending yourself overboard no matter how long your list of steps? Or is saving yourself impossible if you are required to provide at least some number of steps? If so, what is that critical number?
Now consider the generalized problem, where the plank has a buffer of n paces on each side for any n > 0. Can the pirate guarantee that he sends you overboard by forcing you to provide at least some number of steps? (Warning: the generalized problem is very hard!)
Download the Coq source!

Require Import ZArith.
Require Vector.

Local Open Scope list.

Inductive Step :=
  | Left
  | Right.

Definition move (s : Step) : Z := match s with
  | Left ⇒ (-1)%Z
  | Right ⇒ 1%Z
  end.

Given a skip stride length, filterSteps takes every skip + 1th step, starting with the skip+1th step. For example, if skip = 0, we take the entire list of steps.
Definition filterSteps {n : nat} (skip : nat) : Vector.t Step nlist Step :=
  let fix go {n : nat} curSkip (steps : Vector.t Step n) := match steps with
  | Vector.nilnil
  | Vector.cons step _ steps´match curSkip with
    | 0 ⇒ step :: go skip steps´
    | S curSkip´go curSkip´ steps´
    end
  end
  in go skip.

Given a list of steps to be executed, runSteps returns the list of positions that will encountered.
Definition runSteps : list Steplist Z :=
  let fix go curPos (steps : list Step) := match steps with
  | nilnil
  | step :: steps´let curPos´ := (curPos + move step)%Z
                     in curPos´ :: go curPos´ steps´
  end
  in go 0%Z.

survives tells us, given a certain plank_width, would we survive if we passed through a given list of positions?
Definition survives (plank_width : nat)
  : list ZProp := let width := Z.of_nat plank_width in
  List.Forall (fun position ⇒ (position width)%Z (position (- width)%Z)%Z).

stepsSurvive plank_width steps is true if there is no skipping distance that the pirate can choose so that the plan of steps results in walking off the plank for a given plank_width.
Definition stepsSurvive (plank_width : nat) {num_steps : nat}
  (steps : Vector.t Step num_steps) :=
   (skip : nat), survives plank_width (runSteps (filterSteps skip steps)).

canSurvive plank_width num_steps states the proposition that it is possible to issue a list of steps of length num_steps such that we can guarantee to survive (given a particular plank_width).
Definition canSurvive (plank_width num_steps : nat) :=
   (steps : Vector.t Step num_steps), stepsSurvive plank_width steps.

If we can't survive, we must drown!
Definition mustDrown (plank_width num_steps : nat) :=
   (steps : Vector.t Step num_steps), ¬ (stepsSurvive plank_width steps).

This is the generalized form of the puzzle. For any given plank_width, is it always possible to stay on the plank no matter how long we are forced to make our list of steps, or is there some critical number of steps above which the pirate can guarantee that we plunge into the deep blue? Warning: the generalized puzzle is very tough.
Definition GeneralizedPuzzle (plank_width : nat) :=
  ( (num_steps : nat), canSurvive plank_width num_steps)
  
  ( (critical_num_steps : nat), canSurvive plank_width critical_num_steps
                               mustDrown plank_width (S critical_num_steps)).

If the plank is 3 paces wide, that is, we have one step of buffer on each side, how long must our list of steps be before the pirate is sure to throw us overboard?
Definition Puzzle := GeneralizedPuzzle 1.

Theorem Solution : Puzzle.
Proof.
Abort.

Theorem GeneralizedSolution (plank_width : nat) : GeneralizedPuzzle plank_width.
Proof.
Abort.