Chapter 17: The Program Tactic
Catherine Parent
The facilities described in this document pertain to a special aspect of
the Coq system: how to associate to a functional program, whose
specification is written in Gallina, a proof of its correctness.
This methodology is based on the Curry-Howard isomorphism between
functional programs and constructive proofs. This isomorphism allows
the synthesis of a functional program from the constructive part of its
proof of correctness. That is, it is possible to analyze a Coq proof,
to erase all its non-informative parts (roughly speaking, removing the
parts pertaining to sort Prop, considered as comments, to keep only the
parts pertaining to sort Set).
This realizability interpretation
was defined by Christine Paulin-Mohring in her PhD dissertation
[86], and
implemented as a program extraction facility in previous versions of
Coq by Benjamin Werner (see [39]).
However, the corresponding certified program
development methodology was very awkward: the user had to understand very
precisely the extraction mechanism in order to guide the proof construction
towards the desired algorithm. The facilities described in this chapter
attempt to do the reverse: i.e. to try and generate the proof of correctness
from the program itself, given as argument to a specialized tactic.
This work is based on the PhD dissertation of
Catherine Parent (see [81])