We describe a new technique for optimizing first-order functional programs. Programs are represented as graph grammars, and optimization proceeds by counterexample: when a graph generated by the grammar is found to contain an unnecessary computation, the optimizer attempts to reformulates the grammar so that it never again generates any graph that contains that counterexample. This kind of program reformulation corresponds to an interesting problem on context-free grammars. Our reformulation technique is derived from an (approximate) solution to this CFG problem. An optimizer called Thinner is the proof of concept for this technique. Thinner is a fully automatic, source-to-source optimizer for a Lisp-like language of purely functional, first-order programs. Thinner rediscovers a wide variety of common compiler optimizations. It also finds other more exotic transformations, including the well-known Fibonacci reformulation and the Knuth-Morris-Pratt optimization.