# Gas Cans and Decks of Cards

My friend told me the following riddle. Suppose there is a circular track with some gas cans distributed around it. You have a car which has no gas in its tank. If you took all of the gas in the cans and put it in the car, there would be enough gas to go around the track exactly once. Show that there is some point on the track you can start at such that you will be able to make one trip around the track just by filling your tank with the gas in the cans as you drive by them. Obviously, you need to begin next to a gas can and start by putting that in your tank, otherwise you will have no gas and you can't go anywhere.

After solving this riddle, I came up with another riddle about a game which is basically the same. The game has two players. Player 1 takes a standard deck of playing cards and removes the aces and face cards. Next, player 1 shuffles the resulting deck and arranges the cards however he or she likes. Then player 1 hands the deck to player 2. Player 2 is allowed to look at the arrangement of the cards in the deck and then gets to cut the deck exactly once. Then they play the following game. One by one, they flip over the top card on the deck and look at it. If it is a black card, player 2 gets points equal to its value. If it is a red card, player 2 loses points equal to its value. They keep going until they reach the end of the deck. Player 2 starts with 0 points, and if at any time the running total of points is less than 0, player 2 loses. If they make it to the end of the deck without this happening, player 2 wins. Show that it is always possible for player 2 to cut the deck so that he or she wins.

I will now give a formal proof of this in Coq. For our purposes, a deck of cards will be formalized as a list of integers. Black cards will be positive and red cards will be negative.

First we have to formalize what a cut is. We use the standard library functions firstn and skipn. firstn n l returns the first n elements of the list l, while skipn n l returns everything except the first n elements of l.

Definition cut n {A} (l: list A) := skipn n l ++ firstn n l.

Another way to think of this is as rotating the deck by popping cards from the top of the deck and putting them on the bottom.

Fixpoint rotate {A} n (l: list A) :=
match n with
| O => l
| S n' => match l with
| nil => rotate n' l
| a :: l' => rotate n' (l' ++ (a :: nil))
end
end.

There are some easy facts we can establish about rotate and skipn.

Lemma rotate_nil: forall A n, rotate n nil = @nil A.
Lemma rotate_nil2: forall A n (l: list A), rotate n l = nil -> l = nil.
Lemma rotate_rotate: forall A n1 n2 (l: list A), rotate n1 (rotate n2 l) = rotate (n2 + n1) l.
Lemma removelast_aux: forall A (l : list A) a, l = removelast (l ++ a :: nil).
Lemma skipn_aux: forall A n (l: list A) a,
n < length (l ++ a :: nil) -> skipn n (l ++ a :: nil) = skipn n l ++ a :: nil.

Lemma skipn_small: forall A (l: list A) n, (n < length l -> skipn n l <> nil)%nat.
Lemma firstn_length: forall A (l: list A), firstn (length l) l = l.
Lemma firstn_length2: forall A (l: list A) n, n >= length l -> firstn n l = l.
Lemma skipn_length: forall A (l: list A), skipn (length l) l = nil.
Lemma skipn_length2: forall A (l: list A) n, n >= length l -> skipn n l = nil.
Lemma firstn_nil: forall {A} n, firstn n (@nil A) = @nil A.
Lemma rotate_append: forall {A} (l1 l2: list A),
rotate (length l1) (l1 ++ l2) = l2 ++ l1.
Lemma rotate_preserve_length: forall A n (l: list A), length (rotate n l) = length l.

This lets us show that for small n, rotate n l is equal to cut n l.

Lemma rotate_skip_first: forall A n (l: list A),
n <= length l -> rotate n l = skipn n l ++ firstn n l.
Proof.
induction n; intros.
simpl in *. rewrite app_nil_r; auto.
destruct l. inversion H.
simpl.
simpl in H.
rewrite IHn.
assert (n < length (l ++ a :: nil)).
simpl in H.
rewrite app_length. simpl. omega.
assert (firstn n l = firstn n (removelast (l ++ a ::nil))).
rewrite <-(removelast_aux); auto.
rewrite H1.
rewrite firstn_removelast.
rewrite skipn_aux. rewrite <-app_assoc. rewrite <-app_comm_cons. rewrite app_nil_l.
auto. auto. auto. rewrite app_length. simpl. omega.
Qed.

This lets us establish some nice algebraic properties about rotate. Namely, rotations are additive and cyclic in a way that cut is not.

Lemma rotate_length: forall A (l: list A), rotate (length l) l = l.
Lemma rotate_mod: forall {A} (l: list A) k r, rotate (length l * k + r) l = rotate r l.
Lemma rotate_small:
forall {A} (l: list A) n, exists k, (k <= length l /\ rotate n l = rotate k l)%nat.

Now we define a function that sums up the elements in a list and one that sums up the first n elements in a list.

Local Open Scope Z_scope.
Definition sumlist l := fold_right Zplus 0 l.
Definition partialsum n (l: list Z) := fold_right Zplus 0 (firstn n l).

We show that latter is equivalent to the former if n is greater than or equal to the length of the list. We can also show some properties of partial sums of the combinations of two lists.

Lemma partialsum_length1: forall l, partialsum (length l) l = sumlist l.

Lemma partialsum_length2: forall n l, (n >= length l)%nat -> partialsum n l = sumlist l.
Lemma sumlist_app: forall l1 l2, sumlist (l1 ++ l2) = sumlist l1 + sumlist l2.
Lemma partial_sum_append1: forall n l1 l2,
partialsum n (l1 ++ l2) = partialsum n l1 + partialsum (n - length l1) l2.
Lemma partial_sum_append2: forall n l1 l2,
(n <= length l1)%nat -> partialsum n (l1 ++ l2) = partialsum n l1.
Lemma sumlist_rotate: forall l n, sumlist l = sumlist (rotate n l).

Now, with these prerequisites out of the way, we are ready to prove the key lemmas for this proof. Our proof will be by induction on the number of cards in a deck. The result is straight forward if there is only one card in the deck.

For the inductive step, observe that if the sum of the point values of all the cards in the deck is greater than or equal to 0, there must exist some card with non-negative point value. There is some cut which puts this card at the top of the deck. Perform this cut and then take this card and the card beneath it out of the deck. Replace them with a card that is equal to their combined point value. The resulting deck has fewer cards, and the sum of the points of the cards still greater than or equal to 0. Thus, our inductive hypothesis applies, giving us a cut such that player 2 will win with the resulting deck Perform this cut, then replace our combined card with the two original cards.

Note that if we play the game now, player 2 will not lose. Why? The cards that preceded the combined card in the winning deck have not changed, so player 2's running score throughout these cards will not change. Now, when we reach the two replacement cards, the first has non-negative value, so after flipping that over, player 2 still has a non-negative score. The second replacement card may have negative value, but after flipping that one over, player 2's score will be just as it was in the winning deck when he or she flipped over the combined card. Thus it must be non-negative. The rest of the deck is unchanged, so player 2 will still win. Now, we have really made two cuts here, but of course for any sequence of cuts there is a single cut that is equivalent to performing all of them.

First we prove that if the sum of the point values is greater than or equal to 0, there must be some card in the deck with non-negative point value. More precisely, we show that there must be some card whose value is greater than or equal to the average value of all the cards in the deck.

Lemma sumlist_average:
forall (l: list Z) a,
exists k, In k (a :: l) /\ sumlist (a :: l) <= k * Z_of_nat (length (a :: l)).

Next we prove that if a card is in a deck, there is some way to rotate the cards so that this card will be on the top of the deck.

Lemma rotate_to_front:
forall A (l: list A) a, In a l -> exists k, exists l', (k < length l /\ rotate k l = a :: l')%nat.

The next two lemmas have to do with the effects of replacing the combined card with the two original cards. Namely, they say that if the partial sums were originally all non negative, they will continue to be so.

Lemma unglue_lemma1: forall i a b l,
a >= 0 ->
(partialsum i (a + b :: l)
= partialsum i (a :: b :: l)) \/
(partialsum (i - 1) (a + b :: l))
<= partialsum i (a :: b :: l).
Lemma unglue_lemma2: forall n i a b l,
(n <= length l)%nat -> a >= 0 ->
(partialsum i (rotate (S n) (a + b :: l))
= partialsum i (rotate (S (S n)) (a :: b :: l)) \/
(partialsum (i -1) (rotate (S n) (a + b :: l))
<= partialsum i (rotate (S (S n)) (a :: b :: l)))).

With these out of the way, we can prove that the result holds when phrased in terms of rotations instead of cuts.

Lemma card_riddle_aux:
forall n a l, (S n) = length (a :: l) -> partialsum (S n) (a :: l) = 0
-> exists k, forall i, partialsum i (rotate k (a::l)) >= 0.

Using this and the earlier results about the equivalence of rotations and cuts, we can prove the desired theorem.

Theorem card_riddle: forall l, sumlist l = 0
-> exists k, (forall i, partialsum i (cut k l) >= 0).
Proof.
intros. destruct l. exists O. intros. unfold cut; unfold partialsum; simpl.
rewrite firstn_nil. simpl. omega.
generalize (card_riddle_aux (length l) z l); intros.
destruct H0. simpl. auto.
unfold sumlist in *; unfold partialsum in *.
assert (S (length l) = length (z::l)). simpl in *; auto.
rewrite H0. rewrite firstn_length. auto.
specialize (rotate_small (z :: l) x). intros.
destruct H1. destruct H1.
specialize (rotate_skip_first _ _ _ H1); intros.
exists x0. unfold cut. rewrite <-H3. rewrite <-H2. auto.
Qed.

This is not the most exciting fact, but it is a fun little exercise. One interesting thing was the way that reasoning about rotations instead of cuts made things much nicer because of the algebraic properties involved.