Pattern matching dependent types in Coq

A SkillsCast for this session is not available.

Pattern matching with dependent types in Coq can be awkward, while the same program 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.

The purpose of this talk is to demonstrate a small collection of tricks you can use to overcome the awkwardness of pattern matching with dependent types in Coq.

We’ll first review what it means to pattern match on inductive families, contrasting Coq with Agda, and examining 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.

The techniques described in this talk have been distilled from: Adam Chlipala, Certified Programming with Dependent Types, MIT Press, 2013. https://adam.chlipala.net/cpdt/

YOU MAY ALSO LIKE:

• Kiama: Domain-Specific Languages for Language Implementation in Scala (SkillsCast recorded in May 2013)
• co-log: Composable Contravariant Comonadic Logging Component (SkillsCast recorded in May 2019)
• Functional Programming in ... SQL? (SkillsCast recorded in May 2019)