Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. We present a general design and implementation that provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.

@article{paperbot609,
  title = {Equations reloaded: high-level dependently-typed functional programming and proving in Coq},
  author = {Matthieu Sozeau and Cyprien Mangin},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  year = {2019},
  doi = {10.1145/3341690}
}