A Series on StronglySpecified Functions in Coq
Using dependent types and the Prop
sort, it becomes possible to specify
functions whose arguments and results are constrained by properties. Using
such a “stronglyspecified” function requires to provide a proof that the
supplied arguments satisfy the expected properties, and allows for soundly
assuming the results are correct too. However, implementing such functions can
be challenging. In this series, we explore several approaches available to Coq
developers.

Implementing StronglySpecified Functions with the
refine
Tactic We see how to implement stronglyspecified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions' arguments and return value. It makes Coq type system very expressive.

Implementing StronglySpecified Functions with the
Program
Framework Program
is the heir of therefine
tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction.