(** We have seen that Coq has mechanisms both for _programming_, using inductive data types (like [nat] or [list]) and functions over these types, and for _proving_ properties of these programs, using inductive propositions (like [ev] or [eq]), implication, and universal quantification. So far, we have treated these mechanisms as if they were quite separate, and for many purposes this is a good way to think. But we have also seen hints that Coqs programming and proving facilities are closely related. For example, the keyword [Inductive] is used to declare both data types and propositions, and [->] is used both to describe the type of functions on data and logical implication. This is not just a syntactic accident! In fact, programs and proofs in Coq are almost the same thing. In this chapter we will study how this works. We have already seen the fundamental idea: provability in Coq is represented by concrete _evidence_. When we construct the proof of a basic proposition, we are actually building a tree of evidence, which can be thought of as a data structure. If the proposition is an implication like [A -> B], then its proof will be an evidence _transformer_: a recipe for converting evidence for A into evidence for B. So at a fundamental level, proofs are simply programs that manipulate evidence. *) (** Q. If evidence is data, what are propositions themselves? A. They are types! Look again at the formal definition of the [beautiful] property. *)
Posted on: Fri, 19 Sep 2014 20:56:45 +0000
Trending Topics
Recently Viewed Topics
© 2015