Certified Programming with Dependent Types: src/Predicates.v comparison

comparison src/Predicates.v @ 302:7b38729be069

Tweak mark-up to support coqdoc 8.3

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 17 Jan 2011 15:12:30 -0500
parents	2c88fc1dbe33
children	d5787b70cf48

comparison

equal deleted inserted replaced

-:f4768d5a75eb
+:7b38729be069
 (** The so-called %``%#"#Curry-Howard Correspondence#"#%''% states a formal connection between functional programs and mathematical proofs.  In the last chapter, we snuck in a first introduction to this subject in Coq.  Witness the close similarity between the types [unit] and [True] from the standard library: *)
 Print unit.
 (** %\vspace{-.15in}% [[
 Inductive unit : Set :=  tt : unit
-]] *)
+]]
+*)
 Print True.
 (** %\vspace{-.15in}% [[
 Inductive True : Prop :=  I : True
-]] *)
+]]
+*)
 (** Recall that [unit] is the type with only one value, and [True] is the proposition that always holds.  Despite this superficial difference between the two concepts, in both cases we can use the same inductive definition mechanism.  The connection goes further than this.  We see that we arrive at the definition of [True] by replacing [unit] by [True], [tt] by [I], and [Set] by [Prop].  The first two of these differences are superficial changes of names, while the third difference is the crucial one for separating programs from proofs.  A term [T] of type [Set] is a type of programs, and a term of type [T] is a program.  A term [T] of type [Prop] is a logical proposition, and its proofs are of type [T].
 [unit] has one value, [tt].  [True] has one proof, [I].  Why distinguish between these two types?  Many people who have read about Curry-Howard in an abstract context and not put it to use in proof engineering answer that the two types in fact %\textit{%#<i>#should not#</i>#%}% be distinguished.  There is a certain aesthetic appeal to this point of view, but I want to argue that it is best to treat Curry-Howard very loosely in practical proving.  There are Coq-specific reasons for preferring the distinction, involving efficient compilation and avoidance of paradoxes in the presence of classical math, but I will argue that there is a more general principle that should lead us to avoid conflating programming and proving.
 (* begin thide *)
 unfold not.
 (** [[
 ============================
 2 + 2 = 5 -> False
-]] *)
+]]
+*)
 crush.
 (* end thide *)
 Qed.
 1 subgoal
 H : Q
 ============================
 Q \/ P
-]] *)
+]]
+*)
 left; assumption.
 (* end thide *)
 Qed.
 (** The conclusion is replaced with a version using the existential witness that we announced.
 [[
 ============================
 1 + 1 = 2
-]] *)
+]]
+*)
 reflexivity.
 (* end thide *)
 Qed.
 simpl.
 (** [[
 ============================
 even (S (S (n0 + m)))
-]] *)
+]]
+*)
 constructor.
 (** [[
 ============================
 even (n0 + m)
 At this point it is useful to use a theorem from the standard library, which we also proved with a different name in the last chapter.  We can search for a theorem that allows us to rewrite terms of the form [x + S y]. *)
 SearchRewrite (_ + S _).
 (** %\vspace{-.15in}% [[
 plus_n_Sm : forall n m : nat, S (n + m) = n + S m
-]] *)
+]]
+*)
 rewrite <- plus_n_Sm in H0.
 (** The induction hypothesis lets us complete the proof. *)
 %\item%#<li># If you follow the last hint, you may find yourself writing a proof that involves an expression with [eq_nat_dec] that you would like to simplify.  Running [destruct] on the particular call to [eq_nat_dec] should do the trick.  You can automate this advice with a piece of Ltac: [[
 match goal with
 | [ |- context[eq_nat_dec ?X ?Y] ] => destruct (eq_nat_dec X Y)
 end
-]] #</li>#
+]]
+#</li>#
 %\item%#<li># You probably do not want to use an inductive definition for compatibility of variable assignments and typings.#</li>#
 %\item%#<li># The [Tactics] module from this book contains a variant [crush'] of [crush].  [crush'] takes two arguments.  The first argument is a list of lemmas and other functions to be tried automatically in %``%#"#forward reasoning#"#%''% style, where we add new facts without being sure yet that they link into a proof of the conclusion.  The second argument is a list of predicates on which inversion should be attempted automatically.  For instance, running [crush' (lemma1, lemma2) pred] will search for chances to apply [lemma1] and [lemma2] to hypotheses that are already available, adding the new concluded fact if suitable hypotheses can be found.  Inversion will be attempted on any hypothesis using [pred], but only those inversions that narrow the field of possibilities to one possible rule will be kept.  The format of the list arguments to [crush'] is that you can pass an empty list as [tt], a singleton list as the unadorned single element, and a multiple-element list as a tuple of the elements.#</li>#
 %\item%#<li># If you want [crush'] to apply polymorphic lemmas, you may have to do a little extra work, if the type parameter is not a free variable of your proof context (so that [crush'] does not know to try it).  For instance, if you define a polymorphic map insert function [assign] of some type [forall T : Set, ...], and you want particular applications of [assign] added automatically with type parameter [U], you would need to include [assign] in the lemma list as [assign U] (if you have implicit arguments off) or [assign (T := U)] or [@assign U] (if you have implicit arguments on).#</li>#
 #</ol> </li>#%\end{enumerate}%

Mercurial > cpdt > repo

comparison src/Predicates.v @ 302:7b38729be069