# Library problem

# Puzzle: Escaping the death plank (EDP)

*or*two to the left will send you plunging into the cold seas (it's not your standard pirate's plank, I know).

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 n → list Step :=

let fix go {n : nat} curSkip (steps : Vector.t Step n) := match steps with

| Vector.nil ⇒ nil

| Vector.cons step _ steps´ ⇒ match curSkip with

| 0 ⇒ step :: go skip steps´

| S curSkip´ ⇒ go curSkip´ steps´

end

end

in go skip.

let fix go {n : nat} curSkip (steps : Vector.t Step n) := match steps with

| Vector.nil ⇒ nil

| 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 Step → list Z :=

let fix go curPos (steps : list Step) := match steps with

| nil ⇒ nil

| step :: steps´ ⇒ let curPos´ := (curPos + move step)%Z

in curPos´ :: go curPos´ steps´

end

in go 0%Z.

let fix go curPos (steps : list Step) := match steps with

| nil ⇒ nil

| 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 Z → Prop := let width := Z.of_nat plank_width in

List.Forall (fun position ⇒ (position ≤ width)%Z ∧ (position ≥ (- width)%Z)%Z).

: list Z → Prop := 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)).

(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.

∃ (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).

∀ (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)).

(∀ (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.

Theorem Solution : Puzzle.

Proof.

Abort.

Theorem GeneralizedSolution (plank_width : nat) : GeneralizedPuzzle plank_width.

Proof.

Abort.