This paper proposes a new approach to writing
and verifying divide-and-conquer programs in
Coq. Using ideas from advanced
lambda-encodings, combinators are derived in
Coq for divide-and-conquer recursion: from
outer recursions, one may initiate inner
recursions that can construct data upon which
the outer recursions may legally recurse.
Termination is enforced by the type system of
Coq, using just the types of the Calculus of
Constructions. In particular, the method does
not rely on Coq's native structural
recursion. The method is demonstrated on
several examples, including mergesort,
quicksort, Harper's regular-expression
matcher, and others. An indexed version is
also derived, implementing divide-and-conquer
induction.