Poleiro

Where the Coq lives

| Comments GitHub

Searching with eggs

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:

Inductive strategy : Type :=
| Guess (floor : nat)
| Drop (floor : nat) (broken intact : strategy).

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.

Fixpoint play (target : nat) (s : strategy) : bool :=
  match s with
  | Guess floor =>
    beq_nat floor target
  | Drop floor broken intact =>
    play target (if leb target floor then broken
                 else intact)
  end.

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.

Fixpoint eggs (s : strategy) : nat :=
  match s with
  | Guess _ => 0
  | Drop _ broken intact => max (S (eggs broken)) (eggs intact)
  end.

Fixpoint drops (s : strategy) : nat :=
  match s with
  | Guess _ => 0
  | Drop _ broken intact => S (max (drops broken) (drops intact))
  end.

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.

Definition winning (lower range : nat) (s : strategy) : Prop :=
  forall target, lower <= target < lower + range ->
                 play target s = true.

Definition is_optimal (range e d : nat) : Prop :=
  exists s : strategy,
    eggs s <= e /\
    drops s = d /\
    winning 0 range s /\
    forall s', eggs s' <= e ->
               winning 0 range s' ->
               d <= drops s'.

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.

Fixpoint linear (lower range : nat) : strategy :=
  match range with
  | 0 => Guess lower
  | S range' => Drop lower (Guess lower) (linear (S lower) range')
  end.

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.

Lemma linear_winning lower range :
  winning lower (S range) (linear lower range).

Lemma linear_eggs lower range :
  eggs (linear lower range) = min 1 range.

Lemma linear_drops lower range :
  drops (linear lower range) = range.

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.

Definition solution_take_2 : strategy :=
  Drop 33 (linear 0 33)
          (Drop 66 (linear 34 32) (linear 67 32)).

Lemma solution_take_2_winning :
  winning 0 100 solution_take_2.

Lemma solution_take_2_eggs :
  eggs solution_take_2 = 2.

Lemma solution_take_2_drops :
  drops solution_take_2 = 34.

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.

Fixpoint optimal_range_minus_1 (e d : nat) {struct d} : nat :=
  match d, e with
  | S d', S e' => S (optimal_range_minus_1 e' d' +
                     optimal_range_minus_1 (S e') d')
  | _, _ => 0
  end.

Definition optimal_range e d := S (optimal_range_minus_1 e d).

Fixpoint optimal (lower e d : nat) {struct d} : strategy :=
  match d, e with
  | S d', S e' =>
    let floor := lower + optimal_range_minus_1 e' d' in
    Drop floor
         (optimal lower e' d')
         (optimal (S floor) (S e') d')
  | _, _ => Guess lower
  end.

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.

Lemma optimal_winning lower e d :
  winning lower (optimal_range e d) (optimal lower e d).

Lemma optimal_eggs lower e d :
  eggs (optimal lower e d) = min e d.

Lemma optimal_drops lower e d :
  drops (optimal lower e d) = min 1 e * d.

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.

Lemma winning_inv_guess lower range floor :
  winning lower range (Guess floor) -> range <= 1.

Lemma winning_inv_drop lower range floor broken intact :
  winning lower range (Drop floor broken intact) ->
  exists r1 r2 lower',
    range = r1 + r2 /\
    winning lower r1 broken /\
    winning lower' r2 intact.

Lemma optimal_range_correct :
  forall lower e d s range,
    eggs s <= e ->
    drops s <= d ->
    winning lower range s ->
    range <= optimal_range e d.

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

Lemma optimal_range_monotone :
  forall e e' d d',
    e <= e' ->
    d <= d' ->
    optimal_range e d <= optimal_range e' d'.
Proof.
  intros e e' d d' He Hd.
  apply (optimal_range_correct 0 e' d' (optimal 0 e d));
    [ rewrite optimal_eggs; lia
    | rewrite optimal_drops; destruct e; simpl; lia
    | apply optimal_winning ].
Qed.

Lemma optimal_range_lower_bound :
  forall e d, d <= (optimal_range (S e) d).
Proof.
  intros e d.
  cut (S d <= optimal_range (S e) d); try lia.
  apply (optimal_range_correct 0 (S e) d (linear 0 d));
    [ rewrite linear_eggs
    | rewrite linear_drops
    | apply linear_winning ]; lia.
Qed.

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.

Fixpoint find_root (f : nat -> nat) (target n : nat) : nat :=
  match n with
  | 0 => 0
  | S n' =>
    if leb target (f n') then
      find_root f target n'
    else
      S n'
  end.

Lemma find_root_correct :
  forall f target n,
    (forall x y, x <= y -> f x <= f y) ->
    target <= f n ->
    let x := find_root f target n in
    target <= f x /\
    forall y, y < x -> f y < target.

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.

Definition find_optimum e target :=
  find_root (optimal_range e) target target.

Lemma find_optimum_correct :
  forall e range,
    let d := find_optimum (S e) range in
    is_optimal range (S e) d.
Proof.
  intros e range d.
  assert (H : range <= optimal_range (S e) d /\
              forall d', d' < d -> optimal_range (S e) d' < range).
  (* By correctness of find_root *)
  destruct H as [H1 H2].
  exists (optimal 0 (S e) d).
  rewrite optimal_drops, optimal_eggs.
  repeat split; try lia; simpl; try lia.
  - intros x Hx.
    apply optimal_winning. lia.
  - intros s Hs WIN.
    destruct (le_lt_dec d (drops s)) as [LE | LT]; trivial.
    assert (Hd : drops s <= drops s) by lia.
    assert (He : eggs s <= S e) by lia.
    (* optimal_range < range *)
    pose proof (H2 _ LT).
    (* range <= optimal_range *)
    pose proof (optimal_range_correct _ _ _ _ _ He Hd WIN).
    lia.
Qed.

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

Lemma solution :
  is_optimal 100 2 14.
Proof. apply find_optimum_correct. Qed.

| Comments GitHub

Automatic naming considered harmful

Whenever a user doesn't name a variable in an Ltac script, Coq will automatically generate a fresh name for it. After doing some proofs, however, you start to realize that this behavior is more of a nuisance than a feature. The heuristics used by Coq when choosing new names are hard to predict and depend on the current proof state, making proofs likely to break whenever a small change is introduced. As every experienced Coq user knows, trying to figure out whether hypothesis H22 now corresponds to H9 or H24 when fixing a complicated proof script cannot exactly be described as a pleasant experience, specially when the proof script is 2000 lines long and you've spent hours dealing with similar horrors.
When writing robust proof scripts, one must ensure that the code doesn't depend on weird automatically chosen names. Here are some tips for making the naming problem disappear.

Name variables explicitly

Most of the times, you can get rid of this problem by not being lazy and naming everything explicitly. Avoid using tactics like intros or destruct in their unnamed form; instead, use intros v1 v2 v3 ... or destruct v as [a1 a2|a1 a2 a3|...]. You can also name hypothesis in the statement of your lemma, using a forall instead of a plain implication arrow (remember, in Coq, these are actually the same thing). If you don't pass any names to intros, it will try to keep the same names that appear in the current goal:

Lemma l1 : forall (A : Prop) (HYP : A), A.
Proof. intros. exact HYP. Qed.

This also works when reintroducing a variable from the context into the goal, for instance with generalize dependent.

Name constructor arguments

When working with complicated inductive predicates, naming all new variables explicitly on every destruct or inversion can be cumbersome. A reasonable compromise is to name all the arguments to your constructors in inductive definitions. This makes the names that are generated by those tactics meaningful, more stable and predictable. Here's an example of a simple inductively defined relation with explicit argument names:

Inductive collatz : nat -> nat -> Prop :=
| collatz_even (n m : nat)
               (EVEN : 2 * m = n) : collatz n m
| collatz_odd (n m : nat)
              (ODD : 2 * m + 1 = n) : collatz n (3 * n + 1)
| collatz_trans (n m p : nat)
                (COLLATZnm : collatz n m)
                (COLLATZmp : collatz m p) : collatz n p.

Don't refer to names in proofs

Weird automatically generated names are not a problem if they do not appear in Ltac scripts. Automated proofs can obviously help here, but there are small things you can do even if you're not an automation expert. By using match, you can avoid mentioning automatically generated names without having to convert an unnamed inversion or destruct into a named one:

Lemma collatz_cycle :
  forall n m,
    (n = 1 \/ n = 4 \/ n = 2) ->
    collatz n m ->
    m = 1 \/ m = 4 \/ m = 2.
Proof.
  intros.
  match goal with
    | H : collatz _ _ |- _ => induction H
  end.
  - omega.
  - repeat match goal with
             | H : _ \/ _ |- _ => destruct H
           end; omega.
  - match goal with
      | H1 : ?P,
        H2 : ?P -> ?Q,
        H3 : ?Q -> ?R |- ?R =>
        apply H3; apply H2; apply H1
    end.
Qed.

In the above (admittedly artificial) example, we were able to refer exactly to what we wanted in the context without having to resort to the names that Coq chose. Notice how in the third case we were able to specify how premises and conclusions should match when picking the hypotheses. In most cases, a simple match suffices to remove explicit names from proofs.

| Comments GitHub

Summing combinatorial games

In the previous post, we've introduced the concept of combinatorial game and saw how we can employ a simple formalism to model all such games uniformly, the game type. To see what this point of view can bring us, we'll discuss the idea of summing combinatorial games, which can be used to analyze games by decomposing them into smaller, simpler ones. As we'll see, this notion has a straightforward computational interpretation for the game type, making it convenient to manipulate and reason about.
The intuition behind summing games is that they often evolve to a point where they can be seen as several smaller ones being played "simultaneously". In go, for instance, the board is progressively partioned into different regions, and each player must choose in which of those to play during their turn. This suggests a representation where the state of a game is given by the product of the states of the subgames. To make a move, a player modifies the state of one of the subgames according to its rules, leaving the rest of the state untouched.
To define the sum of two combinatorial games (as given by the combinatorial_game type), we can simply combine the lists of moves available for each game component. We must still show that this results in a terminating game, but it suffices to observe that the valid_move relation in this case is equivalent to the product of two well-founded relations, and the Coq standard library provides lemmas for dealing with this case.

Definition cg_pair_order {cg1 cg2} :=
  symprod _ _ (valid_move cg1) (valid_move cg2).
Definition cg_pair_order_wf {cg1 cg2} : well_founded cg_pair_order :=
  wf_symprod _ _ _ _ (finite_game cg1) (finite_game cg2).

Program Definition sum_cg (cg1 cg2 : combinatorial_game)
                          : combinatorial_game :=
  {| position := position cg1 * position cg2;
     moves p pos := map (fun pos1' => (pos1', snd pos))
                        (moves cg1 p (fst pos)) ++
                    map (fun pos2' => (fst pos, pos2'))
                        (moves cg2 p (snd pos)) |}.
Next Obligation.
  match goal with
    | |- well_founded ?R =>
      assert (EQ : RelationClasses.relation_equivalence R cg_pair_order)
  end.
  (* ... *)
  rewrite EQ.
  apply cg_pair_order_wf.
Qed.

A problem with this definition is that it is not directly amenable to computation. We can overcome this problem by defining game sums directly over the game type. Since game is universal, we can hope this should be enough to define what a sum of games is generically. A naive adaptation doesn't work, as recursive calls to sum don't have a single decreasing argument, e.g.

Fail Fixpoint sum (g1 g2 : game) : game :=
  Game (map_game game_as_cg g1 Left (fun g1' P => sum g1' g2) ++
        map_game game_as_cg g2 Left (fun g2' P => sum g1 g2'))
       (map_game game_as_cg g1 Right (fun g1' P => sum g1' g2) ++
        map_game game_as_cg g2 Right (fun g2' P => sum g1 g2')).
(* Error: Cannot guess decreasing argument of fix. *)

One solution is again to pair both arguments and use the Fix combinator with cg_pair_order_wf. Manipulating proof terms in the recursive calls can be made less awkward by using the refine tactic:

Definition sum (g1 g2 : game) : game.
  refine (
    Fix cg_pair_order_wf (fun _ => game)
        (fun gs =>
           match gs with
           | (g1, g2) => fun sum =>
             let sum_fst g1' P := sum (g1', g2) _ in
             let sum_snd g2' P := sum (g1, g2') _ in
             Game (map_game game_as_cg g1 Left sum_fst ++
                   map_game game_as_cg g2 Left sum_snd)
                  (map_game game_as_cg g1 Right sum_fst ++
                   map_game game_as_cg g2 Right sum_snd)
           end) (g1, g2));
  clear - P; constructor; eauto.
Defined.

As with all definitions involving Fix, we must now prove a lemma that shows how sum unfolds. The proof is very similar to the one of embed_in_game_eq, and is thus omitted.

Lemma sum_eq (g1 g2 : game) :
  sum g1 g2 =
  Game (map (fun g1' => sum g1' g2) (left_moves g1) ++
        map (fun g2' => sum g1 g2') (left_moves g2))
       (map (fun g1' => sum g1' g2) (right_moves g1) ++
        map (fun g2' => sum g1 g2') (right_moves g2)).

The name sum suggests that combinatorial games could behave like numbers. We won't discuss this correspondence in much detail for now, but some interesting identities do show up already:

Lemma zero_plus_zero : sum zero zero = zero.

Lemma one_plus_zero : sum one zero = one.

Showing that sum correctly computes what it should is not difficult: we proceed by well-founded induction combining simple lemmas about the behavior of sum, embed_in_game, and map. We need an auxiliary result that allows us to apply our inductive hypothesis:

Lemma map_ext_strong :
  forall {A B}
         (l : list A)
         (f g : A -> B)
         (EXT : forall x, In x l -> f x = g x),
    map f l = map g l.

The statement of lemma just says that embed_in_game exchanges sum and sum_cg.

Lemma sum_is_sum (cg1 cg2 : combinatorial_game)
                 (pos1 : position cg1) (pos2 : position cg2) :
  embed_in_game (sum_cg cg1 cg2) (pos1, pos2) =
  sum (embed_in_game cg1 pos1) (embed_in_game cg2 pos2).
Proof.
  remember (pos1, pos2) as pos.
  replace pos1 with (fst pos) by (destruct pos; simpl; congruence).
  replace pos2 with (snd pos) by (destruct pos; simpl; congruence).
  clear.
  induction pos as [[pos1 pos2] IH]
                using (well_founded_ind cg_pair_order_wf).
  rewrite embed_in_game_eq, sum_eq. simpl.
  repeat rewrite (embed_in_game_moves _ _ Left).
  repeat rewrite (embed_in_game_moves _ _ Right).
  repeat rewrite map_app. repeat rewrite map_map.
  do 2 f_equal;
  apply map_ext_strong; intros pos IN; apply IH; constructor; eexists; eauto.
Qed.

In the next posts, we will see how to use this machinery when decomposing games as sums and comparing subgames.