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

comparison src/Predicates.v @ 55:8d7a97b3bb91

Chapter read-through

author	Adam Chlipala <adamc@hcoop.net>
date	Sun, 28 Sep 2008 13:50:21 -0400
parents	31622083ad5d
children	1946586b9da7

comparison

equal deleted inserted replaced

-:31622083ad5d
+:8d7a97b3bb91
 (** In Coq, the most basic propositional connective is implication, written [->], which we have already used in almost every proof.  Rather than being defined inductively, implication is built into Coq as the function type constructor.
 We have also already seen the definition of [True].  For a demonstration of a lower-level way of establishing proofs of inductive predicates, we turn to this trivial theorem. *)
 Theorem obvious : True.
+(* begin thide *)
 apply I.
+(* end thide *)
 Qed.
 (** We may always use the [apply] tactic to take a proof step based on applying a particular constructor of the inductive predicate that we are trying to establish.  Sometimes there is only one constructor that could possibly apply, in which case a shortcut is available: *)
+(* begin thide *)
 Theorem obvious' : True.
 constructor.
 Qed.
+(* end thide *)
 (** There is also a predicate [False], which is the Curry-Howard mirror image of [Empty_set] from the last chapter. *)
 Print False.
 (** [[
 ]] *)
 (** 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 *)
 Qed.
 (** In a consistent context, we can never build a proof of [False].  In inconsistent contexts that appear in the courses of proofs, it is usually easiest to proceed by demonstrating that inconsistency with an explicit proof of [False]. *)
 Theorem arith_neq : 2 + 2 = 5 -> 9 + 9 = 835.
+(* begin thide *)
 intro.
 (** At this point, we have an inconsistent hypothesis [2 + 2 = 5], so the specific conclusion is not important.  We use the [elimtype] tactic to state a proposition, telling Coq that we wish to construct a proof of the new proposition and then prove the original goal by case analysis on the structure of the new auxiliary proof.  Since [False] has no constructors, [elimtype False] simply leaves us with the obligation to prove [False]. *)
 elimtype False.
 ]] *)
 (** For now, we will leave the details of this proof about arithmetic to [crush]. *)
 crush.
+(* end thide *)
 Qed.
 (** A related notion to [False] is logical negation. *)
 Print not.
 ]] *)
 (** 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.
 (** [[
 ============================
 2 + 2 = 5 -> False
 ]] *)
 crush.
+(* end thide *)
 Qed.
 (** We also have conjunction, which we introduced in the last chapter. *)
 Print and.
 ]] *)
 (** The interested reader can check that [and] has a Curry-Howard doppleganger called [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.  [/\] 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]. *)
 destruct 1.
 (** [[
 (** In each case, the conclusion is among our hypotheses, so the [assumption] tactic finishes the process. *)
 assumption.
 assumption.
+(* end thide *)
 Qed.
 (** Coq disjunction is called [or] and abbreviated with the infix operator [\/]. *)
 Print or.
 ]] *)
 (** We see that there are two ways to prove a disjunction: prove the first disjunct or prove the second.  The Curry-Howard analogue of this is the Coq [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. *)
 destruct 1.
 (** [[
 2 subgoals
 ============================
 Q \/ P
 ]] *)
 left; assumption.
+(* end thide *)
 Qed.
 (* begin hide *)
 (* In-class exercises *)
 (** It would be a shame to have to plod manually through all proofs about propositional logic.  Luckily, there is no need.  One of the most basic Coq automation tactics is [tauto], which is a complete decision procedure for constructive propositional logic.  (More on what "constructive" means in the next section.)  We can use [tauto] to dispatch all of the purely propositional theorems we have proved so far. *)
 Theorem or_comm' : P \/ Q -> Q \/ P.
+(* begin thide *)
 tauto.
+(* end thide *)
 Qed.
 (** Sometimes propositional reasoning forms important plumbing for the proof of a theorem, but we still need to apply some other smarts about, say, arithmetic.  [intuition] is a generalization of [tauto] that proves everything it can using propositional reasoning.  When some goals remain, it uses propositional laws to simplify them as far as possible.  Consider this example, which uses the list concatenation operator [++] from the standard library. *)
 Theorem arith_comm : forall ls1 ls2 : list nat,
 length ls1 = length ls2 \/ length ls1 + length ls2 = 6
 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2.
+(* begin thide *)
 intuition.
 (** A lot of the proof structure has been generated for us by [intuition], but the final proof depends on a fact about lists.  The remaining subgoal hints at what cleverness we need to inject. *)
 (** [[
 ]] *)
 (** Now the subgoal follows by purely propositional reasoning.  That is, we could replace [length ls1 + length ls2 = 6] with [P] and [length ls1 = length ls2] with [Q] and arrive at a tautology of propositional logic. *)
 tauto.
+(* end thide *)
 Qed.
 (** [intuition] is one of the main bits of glue in the implementation of [crush], so, with a little help, we can get a short automated proof of the theorem. *)
+(* begin thide *)
 Theorem arith_comm' : forall ls1 ls2 : list nat,
 length ls1 = length ls2 \/ length ls1 + length ls2 = 6
 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2.
 Hint Rewrite app_length : cpdt.
 crush.
 Qed.
+(* end thide *)
 End Propositional.
 (** * What Does It Mean to Be Constructive? *)
 ]] *)
 (** [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. *)
 Theorem exist1 : exists x : nat, x + 1 = 2.
+(* begin thide *)
 (** remove printing exists*)
-(** We can start this proof with a tactic [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.") *)
+(** We can start this proof with a tactic [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.) *)
 exists 1.
 (** The conclusion is replaced with a version using the existential witness that we announced. *)
 (** [[
 ============================
 1 + 1 = 2
 ]] *)
 reflexivity.
+(* end thide *)
 Qed.
 (** printing exists $\exists$ *)
 (** We can also use tactics to reason about existential hypotheses. *)
 Theorem exist2 : forall n m : nat, (exists x : nat, n + x = m) -> n <= m.
+(* begin thide *)
 (** We start by case analysis on the proof of the existential fact. *)
 destruct 1.
 (** [[
 n : nat
 ]] *)
 (** The goal has been replaced by a form where there is a new free variable [x], and where we have a new hypothesis that the body of the existential holds with [x] substituted for the old bound variable.  From here, the proof is just about arithmetic and is easy to automate. *)
 crush.
+(* end thide *)
 Qed.
 (* begin hide *)
 (* In-class exercises *)
 Inductive isZero : nat -> Prop :=
 | IsZero : isZero 0.
 Theorem isZero_zero : isZero 0.
+(* begin thide *)
 constructor.
+(* end thide *)
 Qed.
 (** We can call [isZero] a %\textit{%#<i>#judgment#</i>#%}%, in the sense often used in the semantics of programming languages.  Judgments are typically defined in the style of %\textit{%#<i>#natural deduction#</i>#%}%, where we write a number of %\textit{%#<i>#inference rules#</i>#%}% with premises appearing above a solid line and a conclusion appearing below the line.  In this example, the sole constructor [IsZero] of [isZero] can be thought of as the single inference rule for deducing [isZero], with nothing above the line and [isZero 0] below it.  The proof of [isZero_zero] demonstrates how we can apply an inference rule.
 The definition of [isZero] differs in an important way from all of the other inductive definitions that we have seen in this and the previous chapter.  Instead of writing just [Set] or [Prop] after the colon, here we write [nat -> Prop].  We saw examples of parameterized types like [list], but there the parameters appeared with names %\textit{%#<i>#before#</i>#%}% the colon.  Every constructor of a parameterized inductive type must have a range type that uses the same parameter, whereas the form we use here enables us to use different arguments to the type for different constructors.
 (** [eq] is the type we get behind the scenes when uses of infix [=] are expanded.  We see that [eq] has both a parameter [x] that is fixed and an extra unnamed argument of the same type.  It is crucial that the second argument is untied to the parameter in the type of [eq]; otherwise, we would have to prove that two values are equal even to be able to state the possibility of equality, which would more or less defeat the purpose of having an equality proposition.  However, examining the type of equality's sole constructor [refl_equal], we see that we can only %\textit{%#<i>#prove#</i>#%}% 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.
 Returning to the example of [isZero], we can see how to make use of hypotheses that use this predicate. *)
 Theorem isZero_plus : forall n m : nat, isZero m -> n + m = n.
+(* begin thide *)
 (** We want to proceed by cases on the proof of the assumption about [isZero]. *)
 destruct 1.
 (** [[
 n : nat
 ]] *)
 (** Since [isZero] has only one constructor, we are presented with only one subgoal.  The argument [m] to [isZero] is replaced with that type's argument from the single constructor [IsZero].  From this point, the proof is trivial. *)
 crush.
+(* end thide *)
 Qed.
 (** Another example seems at first like it should admit an analogous proof, but in fact provides a demonstration of one of the most basic gotchas of Coq proving. *)
 Theorem isZero_contra : isZero 1 -> False.
+(* begin thide *)
 (** Let us try a proof by cases on the assumption, as in the last proof. *)
 destruct 1.
 (** [[
 ============================
 Why does Coq use this restriction?  We will discuss the issue in detail in a future chapter, when we see the dependently-typed programming techniques that would allow us to write this proof term manually.  For now, we just say that the algorithmic problem of "logically complete case analysis" is undecidable when phrased in Coq's logic.  A few tactics and design patterns that we will present in this chapter suffice in almost all cases.  For the current example, what we want is a tactic called [inversion], which corresponds to the concept of inversion that is frequently used with natural deduction proof systems. *)
 Undo.
 inversion 1.
+(* end thide *)
 Qed.
 (** What does [inversion] do?  Think of it as a version of [destruct] that does its best to take advantage of the structure of arguments to inductive types.  In this case, [inversion] completed the proof immediately, because it was able to detect that we were using [isZero] with an impossible argument.
 Sometimes using [destruct] when you should have used [inversion] can lead to confusing results.  To illustrate, consider an alternate proof attempt for the last theorem. *)
 (** Think of [even] as another judgment defined by natural deduction rules.  [EvenO] is a rule with nothing above the line and [even O] below the line, and [EvenSS] is a rule with [even n] above the line and [even (S (S n))] below.
 The proof techniques of the last section are easily adapted. *)
 Theorem even_0 : even 0.
+(* begin thide *)
 constructor.
+(* end thide *)
 Qed.
 Theorem even_4 : even 4.
+(* begin thide *)
 constructor; constructor; constructor.
+(* end thide *)
 Qed.
 (** It is not hard to see that sequences of constructor applications like the above can get tedious.  We can avoid them using Coq's hint facility. *)
+(* begin thide *)
 Hint Constructors even.
 Theorem even_4' : even 4.
 auto.
 Qed.
+(* end thide *)
 Theorem even_1_contra : even 1 -> False.
+(* begin thide *)
 inversion 1.
+(* end thide *)
 Qed.
 Theorem even_3_contra : even 3 -> False.
+(* begin thide *)
 inversion 1.
 (** [[
 H : even 3
 n : nat
 ]] *)
 (** [inversion] can be a little overzealous at times, as we can see here with the introduction of the unused variable [n] and an equality hypothesis about it.  For more complicated predicates, though, adding such assumptions is critical to dealing with the undecidability of general inversion. *)
 inversion H1.
+(* end thide *)
 Qed.
 (** We can also do inductive proofs about [even]. *)
 Theorem even_plus : forall n m, even n -> even m -> even (n + m).
+(* begin thide *)
 (** It seems a reasonable first choice to proceed by induction on [n]. *)
 induction n; crush.
 (** [[
 n : nat
 (** In fact, [crush] can handle all of the details of the proof once we declare the induction strategy. *)
 Restart.
 induction 1; crush.
+(* end thide *)
 Qed.
 (** Induction on recursive predicates has similar pitfalls to those we encountered with inversion in the last section. *)
 Theorem even_contra : forall n, even (S (n + n)) -> False.
+(* begin thide *)
 induction 1.
 (** [[
 n : nat
 ============================
 rewrite <- plus_n_Sm in H0.
 (** The induction hypothesis lets us complete the proof. *)
 apply IHeven with n0; assumption.
-(** As usual, we can rewrite the proof to avoid referencing any locally-generated names, which makes our proof script more robust to changes in the theorem statement. *)
+(** As usual, we can rewrite the proof to avoid referencing any locally-generated names, which makes our proof script more readable and more robust to changes in the theorem statement. *)
 Restart.
 Hint Rewrite <- plus_n_Sm : cpdt.
 induction 1; crush;
 match goal with
 end; crush; eauto.
 Qed.
 (** We write the proof in a way that avoids the use of local variable or hypothesis names, using the [match] tactic form to do pattern-matching on the goal.  We use unification variables prefixed by question marks in the pattern, and we take advantage of the possibility to mention a unification variable twice in one pattern, to enforce equality between occurrences.  The hint to rewrite with [plus_n_Sm] in a particular direction saves us from having to figure out the right place to apply that theorem, and we also take critical advantage of a new tactic, [eauto].
-[crush] uses the tactic [intuition], which, when it runs out of tricks to try using only propositional logic, by default tries the tactic [auto], which we saw in an earlier example.  [auto] attempts Prolog-style logic programming, searching through all proof trees up to a certain depth that are built only out of hints that have been registered with [Hint] commands.  Compared to Prolog, [auto] places an important restriction: it never introduces new unification variables during search.  That is, every time a rule is applied during proof search, all of its arguments must be deducible by studying the form of the goal.  [eauto] relaxes this restriction, at the cost of possibly exponentially greater running time.  In this particular case, we know that [eauto] has only a small space of proofs to search, so it makes sense to run it.  It is common in effectively-automated Coq proofs to see a bag of standard tactics applied to pick off the "easy" subgoals, finishing off with [eauto] to handle the tricky parts that can benefit from ad-hoc exhaustive search.
+[crush] uses the tactic [intuition], which, when it runs out of tricks to try using only propositional logic, by default tries the tactic [auto], which we saw in an earlier example.  [auto] attempts Prolog-style logic programming, searching through all proof trees up to a certain depth that are built only out of hints that have been registered with [Hint] commands.  Compared to Prolog, [auto] places an important restriction: it never introduces new unification variables during search.  That is, every time a rule is applied during proof search, all of its arguments must be deducible by studying the form of the goal.  [eauto] relaxes this restriction, at the cost of possibly exponentially greater running time.  In this particular case, we know that [eauto] has only a small space of proofs to search, so it makes sense to run it.  It is common in effectively-automated Coq proofs to see a bag of standard tactics applied to pick off the "easy" subgoals, finishing with [eauto] to handle the tricky parts that can benefit from ad-hoc exhaustive search.
 The original theorem now follows trivially from our lemma. *)
 Theorem even_contra : forall n, even (S (n + n)) -> False.
 intros; eapply even_contra'; eauto.
 ]] *)
 (** We are out of luck here.  The inductive hypothesis is trivially true, since its assumption is false.  In the version of this proof that succeeded, [IHeven] had an explicit quantification over [n].  This is because the quantification of [n] %\textit{%#<i>#appeared after the thing we are inducting on#</i>#%}% in the theorem statement.  In general, quantified variables and hypotheses that appear before the induction object in the theorem statement stay fixed throughout the inductive proof.  Variables and hypotheses that are quantified after the induction object may be varied explicitly in uses of inductive hypotheses.
 Why should Coq implement [induction] this way?  One answer is that it avoids burdening this basic tactic with additional heuristic smarts, but that is not the whole picture.  Imagine that [induction] analyzed dependencies among variables and reordered quantifiers to preserve as much freedom as possible in later uses of inductive hypotheses.  This could make the inductive hypotheses more complex, which could in turn cause particular automation machinery to fail when it would have succeeded before.  In general, we want to avoid quantifiers in our proofs whenever we can, and that goal is furthered by the refactoring that the [induction] tactic forces us to do. *)
+(* end thide *)
 Abort.
 (* begin hide *)
 (* In-class exercises *)

Mercurial > cpdt > repo

comparison src/Predicates.v @ 55:8d7a97b3bb91