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

comparison src/Predicates.v @ 442:89c67796754e

Undo some overzealous vspace tweaks

author	Adam Chlipala <adam@chlipala.net>
date	Wed, 01 Aug 2012 16:09:37 -0400
parents	f923024bd284
children	2740b8a23cce

comparison

equal deleted inserted replaced

-:cbfd23b4364d
+:89c67796754e
 Print True.
 (** %\vspace{-.15in}%[[
 Inductive True : Prop :=  I : True
 ]]
-%\smallskip{}%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].  Chapter 12 goes into more detail about the theoretical differences between [Prop] and [Set].  For now, we will simply follow common intuitions about what a proof is.
+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].  Chapter 12 goes into more detail about the theoretical differences between [Prop] and [Set].  For now, we will simply follow common intuitions about what a proof is.
 The type [unit] has one value, [tt].  The type [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 _should not_ 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.
 The essence of the argument is roughly this: to an engineer, not all functions of type [A -> B] are created equal, but all proofs of a proposition [P -> Q] are.  This idea is known as%\index{proof irrelevance}% _proof irrelevance_, and its formalizations in logics prevent us from distinguishing between alternate proofs of the same proposition.  Proof irrelevance is compatible with, but not derivable in, Gallina.  Apart from this theoretical concern, I will argue that it is most effective to do engineering with Coq by employing different techniques for programs versus proofs.  Most of this book is organized around that distinction, describing how to program, by applying standard functional programming techniques in the presence of dependent types; and how to prove, by writing custom Ltac decision procedures.
 Print False.
 (** %\vspace{-.15in}%[[
 Inductive False : Prop :=
 ]]
-%\smallskip{}%We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number.  Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *)
+We can conclude anything from [False], doing case analysis on a proof of [False] in the same way we might do case analysis on, say, a natural number.  Since there are no cases to consider, any such case analysis succeeds immediately in proving the goal. *)
 Theorem False_imp : False -> 2 + 2 = 5.
 (* begin thide *)
 destruct 1.
 (* end thide *)
 (** %\vspace{-.15in}% [[
 not = fun A : Prop => A -> False
 : Prop -> Prop
 ]]
-%\smallskip{}%We see that [not] is just shorthand for implication of [False].  We can use that fact explicitly in proofs.  The syntax [~ P] expands to [not P]. *)
+We see that [not] is just shorthand for implication of [False].  We can use that fact explicitly in proofs.  The syntax [~ P] expands to [not P]. *)
 Theorem arith_neq' : ~ (2 + 2 = 5).
 (* begin thide *)
 unfold not.
 (** [[
 Print and.
 (** %\vspace{-.15in}%[[
 Inductive and (A : Prop) (B : Prop) : Prop :=  conj : A -> B -> A /\ B
 ]]
-%\smallskip{}%The interested reader can check that [and] has a Curry-Howard equivalent called %\index{Gallina terms!prod}%[prod], the type of pairs.  However, it is generally most convenient to reason about conjunction using tactics.  An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks.  The operator [/\] is an infix shorthand for [and]. *)
+The interested reader can check that [and] has a Curry-Howard equivalent called %\index{Gallina terms!prod}%[prod], the type of pairs.  However, it is generally most convenient to reason about conjunction using tactics.  An explicit proof of commutativity of [and] illustrates the usual suspects for such tasks.  The operator [/\] is an infix shorthand for [and]. *)
 Theorem and_comm : P /\ Q -> Q /\ P.
 (* begin thide *)
 (** We start by case analysis on the proof of [P /\ Q]. *)
 (** %\vspace{-.15in}%[[
 Inductive or (A : Prop) (B : Prop) : Prop :=
 or_introl : A -> A \/ B | or_intror : B -> A \/ B
 ]]
-%\smallskip{}%We see that there are two ways to prov a disjunction: prove the first disjunct or prove the second.  The Curry-Howard analogue of this is the Coq %\index{Gallina terms!sum}%[sum] type.  We can demonstrate the main tactics here with another proof of commutativity. *)
+We see that there are two ways to prov a disjunction: prove the first disjunct or prove the second.  The Curry-Howard analogue of this is the Coq %\index{Gallina terms!sum}%[sum] type.  We can demonstrate the main tactics here with another proof of commutativity. *)
 Theorem or_comm : P \/ Q -> Q \/ P.
 (* begin thide *)
 (** As in the proof for [and], we begin with case analysis, though this time we are met by two cases instead of one. *)
 (** %\vspace{-.15in}%[[
 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
 ex_intro : forall x : A, P x -> ex P
 ]]
-%\smallskip{}%The family [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s.  We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x].  As usual, there are tactics that save us from worrying about the low-level details most of the time.  We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic.  For our purposes, it is. *)
+The family [ex] is parameterized by the type [A] that we quantify over, and by a predicate [P] over [A]s.  We prove an existential by exhibiting some [x] of type [A], along with a proof of [P x].  As usual, there are tactics that save us from worrying about the low-level details most of the time.  We use the equality operator [=], which, depending on the settings in which they learned logic, different people will say either is or is not part of first-order logic.  For our purposes, it is. *)
 Theorem exist1 : exists x : nat, x + 1 = 2.
 (* begin thide *)
 (** remove printing exists *)
 (** We can start this proof with a tactic %\index{tactics!exists}%[exists], which should not be confused with the formula constructor shorthand of the same name.  (In the PDF version of this document, the reverse %`%#'#E#'#%'% appears instead of the text "exists" in formulas.) *)
 Print eq.
 (** %\vspace{-.15in}%[[
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 ]]
-%\smallskip{}%Behind the scenes, uses of infix [=] are expanded to instances of [eq].  We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type.  The type of [eq] allows us to state any equalities, even those that are provably false.  However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal.  This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition.  Another way of stating that definition is: equality is defined as the least reflexive relation.
+Behind the scenes, uses of infix [=] are expanded to instances of [eq].  We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type.  The type of [eq] allows us to state any equalities, even those that are provably false.  However, examining the type of equality's sole constructor [eq_refl], we see that we can only _prove_ equality when its two arguments are syntactically equal.  This definition turns out to capture all of the basic properties of equality, and the equality-manipulating tactics that we have seen so far, like [reflexivity] and [rewrite], are implemented treating [eq] as just another inductive type with a well-chosen definition.  Another way of stating that definition is: equality is defined as the least reflexive relation.
 Returning to the example of [isZero], we can see how to work with hypotheses that use this predicate. *)
 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n.
 (* begin thide *)
 (** %\vspace{-.15in}% [[
 isZero_ind
 : forall P : nat -> Prop, P 0 -> forall n : nat, isZero n -> P n
 ]]
-%\smallskip{}%In our last proof script, [destruct] chose to instantiate [P] as [fun n => S n + S n = S (S (S (S n)))].  You can verify for yourself that this specialization of the principle applies to the goal and that the hypothesis [P 0] then matches the subgoal we saw generated.  If you are doing a proof and encounter a strange transmutation like this, there is a good chance that you should go back and replace a use of [destruct] with [inversion]. *)
+In our last proof script, [destruct] chose to instantiate [P] as [fun n => S n + S n = S (S (S (S n)))].  You can verify for yourself that this specialization of the principle applies to the goal and that the hypothesis [P 0] then matches the subgoal we saw generated.  If you are doing a proof and encounter a strange transmutation like this, there is a good chance that you should go back and replace a use of [destruct] with [inversion]. *)
 (* begin hide *)
 (* In-class exercises *)

Mercurial > cpdt > repo

comparison src/Predicates.v @ 442:89c67796754e