# Library solution

# Solution: Escaping the death plank (EDP)

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

*A SAT Attack on the Erdos Discrepancy Conjecture*.*The Erdos discrepancy problem*.Fixpoint myForall {A : Set} (P : A → Prop) (xs : list A) : Prop := match xs with

| nil ⇒ True

| x :: xs´ ⇒ P x ∧ myForall P xs´

end.

Theorem forallEquiv {A : Set} {P : A → Prop} (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.

admit.

Qed.

Require Import ZArith.

Lemma numProp (x y : nat) : x × S y ≤ y → x = 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.

admit.

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 M´ ⇒ n = M ∨ smallNums n M´

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.

admit.

Qed.

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.

admit.

Qed.