Pattern matching with dependent types in Coq can be awkward, while equivalent programs in Agda might be straightforward and elegant. Yet despite the awkwardness, there may still be reasons to choose Coq for your next dependently-typed development, for example if you want a tactic language to develop domain-specific proof-search procedures.
In this talk, we show how to
match in Coq, using techniques described by Adam
Chlipala in his book, Certified Programming with Dependent Types.
We first review what it means to pattern-match on inductive families,
contrasting Coq with Agda, and examine what it is about Coq that complicates
pattern matching. Using a simple running example, we’ll show how to use Coq
match annotations to eliminate nonsense cases, and the convoy pattern for
refining the types of things already in scope. Finally, we’ll show that by
equipping an inductive family with some well-chosen combinators, it is often
possible to regain some semblance of elegance.