# Library solution

Require Import problem.

# Solution: Escaping the death plank (EDP)

If your list of steps includes 12 or more steps, the pirate is guaranteed to be able to send you overboard. You can confirm this by trying to provide a list of 12 steps. You'll see that all of the choices become constrained, and further that there eventually become mutually contradictory constraints.
Here's one example of a list of 11 steps for which it is impossible for the pirate to send you overboard.

Local Open Scope list.

Notation " [ x ; .. ; y ] " := (Vector.cons _ x _ .. (Vector.cons _ y _ (Vector.nil _)) ..) : vector_scope.
Local Open Scope vector_scope.

Definition mySteps : Vector.t Step 11 :=
[ Right; Left; Left; Right; Left; Right
; Right; Left; Left; Right; Right].

The generalized problem, where the plank has a buffer of n > 0 paces on each side, is known as the Erdős Discrepancy Problem (which motivated the acronym for this puzzle's name!).
The solution to a buffer of n = 2 paces was found recently, in 2014, using a SAT solver:
Boris Konev, Alexei Lisitsa. A SAT Attack on the Erdos Discrepancy Conjecture.
The SAT solver found a working list of 1160 steps, and proved that the pirate could send overboard any list of 1161 steps or longer. The formal proof of unsatisfiability for 1161 steps was 13 GB large.
The general solution was unknown until last month (September 2015), when Terence Tao solved it. I did warn that the generalized problem was difficult! No matter what size the buffer on each side, there is some number of steps after which the pirate is guaranteed to be able to send you overboard.
Terence Tao. The Erdos discrepancy problem.
I am not expecting a Coq proof of the generalized problem anytime soon! What follows is a very incomplete proof sketch that currently only proves that the list of 11 steps works, and even that has a few holes.

Fixpoint myForall {A : Set} (P : AProp) (xs : list A) : Prop := match xs with
| nilTrue
| x :: xs´P x myForall P xs´
end.

Theorem forallEquiv {A : Set} {P : AProp} (xs : list A)
: myForall P xs List.Forall P xs.
Proof.
split; induction xs; intros.
constructor.
simpl in H. destruct H.
constructor. assumption.
apply IHxs. assumption.
constructor.
inversion H. split. assumption. apply IHxs.
assumption.
Qed.

Lemma filterStepsLength (num_steps skip : nat) (steps : Vector.t Step num_steps)
: length (filterSteps skip steps) × S skip num_steps.
Proof.
induction num_steps.
- dependent inversion steps.
constructor.
- dependent inversion steps.
Qed.

Require Import ZArith.

Lemma numProp (x y : nat) : x × S y yx = 0.
Proof.
generalize dependent x.
induction y; intros.
- inversion H. rewrite H1. induction x. reflexivity. simpl in ×. inversion H.
- apply IHy. rewrite mult_comm in H. simpl in H. rewrite mult_comm. simpl.
Qed.

Lemma longSkipsOk (num_steps skip : nat) :
skip num_steps (plank_width : nat) (steps : Vector.t Step num_steps),
survives plank_width (runSteps (filterSteps skip steps)).
Proof.
intros.
pose proof (filterStepsLength num_steps skip steps).
assert (length (filterSteps skip steps) × S skip skip).
apply le_trans with (m := num_steps); assumption.
apply numProp in H1.
destruct (filterSteps skip steps).
apply List.Forall_nil.
inversion H1.
Qed.

Fixpoint smallNums (n M : nat) := match M with
| 0 ⇒ n = 0
| S n = M smallNums n
end.

Lemma smallNumsLE (n M : nat) : n M smallNums n M.
Proof.
generalize dependent M.
induction M; split; intros.
- induction H.
+ induction n. reflexivity.
simpl. left. reflexivity.
+ simpl. right. assumption.
- simpl in H. rewrite H. constructor.
- simpl. inversion H.
+ left. reflexivity.
+ right. apply IHM. apply H1.
- simpl in H. destruct H.
+ rewrite H. apply le_refl.
+ apply le_S. apply IHM. assumption.
Qed.

The list of 11 steps that we provided earlier indeed have discrepancy no greater than 1.
Lemma myStepsSurvive : stepsSurvive 1 mySteps.
Proof.
unfold stepsSurvive. intro skip.
destruct (le_gt_dec skip 11).
apply smallNumsLE in l.
simpl in l.
repeat match goal with
| [ H : skip = ?x ?others |- _ ] ⇒ destruct H; subst; unfold mySteps; unfold survives
| [ |- List.Forall _ _ ] ⇒ apply forallEquiv; simpl
| [ |- True ] ⇒ constructor
| [ |- _ _ ] ⇒ split
| [ |- (_ _)%Z ] ⇒ omega
| [ |- (_ _)%Z ] ⇒ omega
end.
apply gt_le_S in g.

fold stepsSurvive.
apply longSkipsOk.
unfold ge. omega.
Qed.

Theorem Solution : Puzzle.
Proof.
unfold Puzzle. unfold GeneralizedPuzzle.
right. 11. split.
- unfold canSurvive. mySteps. apply myStepsSurvive.
- unfold mustDrown.