Consider the following problem. Suppose we are in a 100-story building. We know that, when dropping an egg from the window, the egg will stay intact if we are below a certain floor. However, if we repeat the same exercise above that critical floor, the egg will break. How can we find this floor and minimize the number of egg drops performed in the worst case if we have only two eggs? We suppose that we are allowed to reuse eggs that fall without breaking. We will see how we can model this problem in Coq and find a correct solution. We model a playing strategy as a decision tree:

In the above definition, Guess floor represents the end of the algorithm, when we try to guess the target floor. If floor is equal to the target, we win the game; otherwise, we lose. Drop floor broken intact represents an egg drop at floor. If the egg breaks, we continue playing with strategy broken; otherwise, we continue with intact. Simulating an egg-drop game is just a matter of performing a tree search. play target s returns true if and only if strategy s succeeds in guessing floor target.

We can also find how many eggs a strategy needs and how many drops are performed in the worst case. drops just computes the strategy tree height, whereas eggs computes a "skewed" height, where right branches do not add to the final value.

Finally, using these concepts, we can describe what the solution for our problem is. winning lower range s says that strategy s is able to find range target floors starting at lower, while is_optimal range e d states that there is a winning strategy for guessing range target floors, uses at most e eggs and performing at most d drops, such that d is the smallest possible.

A simple first strategy

Before trying to find an optimal solution, let us try to find one that works. A simple strategy is to perform linear search, starting at the bottom and going up one floor at a time. As soon as the egg breaks, we know that we have found our target.

linear lower range works on a range of S range floors, using at most one egg. Because of this, it is not very efficient, performing n drops in the worst case.

Improving our strategy

Now that we know a naive search strategy, we will try to find an optimal one. Intuitively, it seems that it should be possible to perform some form of binary search, starting at the middle of our floor range, and continuing recursively depending on the outcome of our drop.

Although much better than a pure linear strategy, this is still far from being optimal: if our egg doesn't break on our first drop, we will still be using at most only one egg on that upper range. If we allowed ourselves to break one of them, presumably, we would be able to solve the upper range in less than 50 drops, which would in turn allow us to perform our first drop at a lower floor, e.g.

Our new solution performs much better, but there is still room for improvement. Once again, if our first two drops are below the target floor, we will be using only one egg to search through 33 floors, which could be done better if we had used both of them. This suggests that the optimal strategy should be some form of skewed binary search, where the upper range that is produced by an egg drop should use its available eggs in an optimal way.

Finding the optimum

How can we formalize the intuition that we just developed? The key insight is to reason by duality and, instead, ask "what is the largest range of floors we can scan using at most some number of eggs and drops?" When looking at the problem this way, it becomes clear that optimality has a recursive structure that is easy to describe: to find a floor using at most e eggs and d drops, we need to combine two optimal strategies: one using at most e-1 eggs and d-1 drops, for the case where our first drop causes the egg to break, and another using at most e eggs and d-1 drops, for the case where our egg does not break at first. We can readily express this idea as code. optimal_range e d computes the maximal range size that can be solved using e eggs and d drops at most, while optimal lower e d computes a strategy for doing so starting from floor lower.

It is easy to show that optimal lower e d scans optimal_range e d floors, as well that it uses the resources that we expect.

To actually show optimality, we need to show that optimal_range indeed computes what it is supposed to. We start by showing two inversion lemmas, relating the range that is scanned by a winning strategy to the range scanned by its sub-strategies.

Combining this lemma with the ranges we had derived for linear and optimal, we can prove useful results about optimal_range.

Given that optimal_range is monotone, we can find what the optimal number of drops for a given range is by picking the smallest value of t such that range <= optimal_range e t. We formalize this idea by writing a generic function find_root that can find such values for any monotone function f, given a suitable initial guess.

By instantiating this theorem with optimal_range and applying the appropriate theorems, we obtain our final result. The proof of optimality goes by contradiction. Let t = find_optimum (S e) range. if we find another strategy s such that eggs s <= S e and drops s < t, we know that range <= optimal_range (S e) t by optimal_range_correct, but we must also have optimal_range (S e) t < range by the correctness of find_root.

Using this result, we can find the answer for our original problem.