DOC PREVIEW
Penn CIS 500 - More On Induction

This preview shows page 1-2-3-4 out of 11 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 11 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

More On InductionQuick ReviewProgramming with PropositionsInduction AxiomsInduction Principles for Other DatatypesA Closer Look at Induction HypothesesA Closer Look at the induction TacticGeneralizing the Induction HypothesisEvidenceConstructing EvidenceManipulating Evidence7 More On Induction7.1 Quick ReviewWe’ve now seen a bunch of Coq’s fundamental tactics—enough, in fact, todo pretty much everything we’ll want for a while. We’ll introduce one or twomore as we go along through the next few lectures, and later in the coursewe’ll introduce some more powerful automation tactics that make Coq domore of the low-level work in many cases, but basically this is the set weneed. Figure 7-1 gives a summary.7.2 Programming with PropositionsA proposition is a statement expressing a factual claim. In Coq, propositionsare written as expressions of type Prop. Although we haven’t mentioned itexplicitly, we have already seen numerous examples of such expressions.Check (plus 2 2 = 4).Iplus 2 2 = 4: PropCheck (ble_nat 3 2 = false).Ible_nat 3 2 = false: PropBoth provable and unprovable claims are perfectly good propositions.Simply being a proposition is one thing; being provable is something else! Bothplus 2 2 = 4 and plus 2 2 = 5 are expressions of type Prop.One important role for propositions in Coq is as the subjects of Theorems,Examples, etc. But they can be used in many other ways. For example, wecan give a name to a proposition using a Definition, just as we have given7.2 Programming with Propositions 57intros move hypotheses/variables from goal to contextreflexivity finish the proof (when the goal looks like e = e)apply prove goal using a hypothesis, lemma, or con-structorapply... in H apply a hypothesis, lemma, or constructor to a hy-pothesis in the context (forward reasoning)apply... with... explicitly specify values for variables that cannotbe determined by pattern matchingsimpl simplify computations in the goalsimpl in H ... or a hypothesisrewrite use an equality to rewrite the goalrewrite ... in H ... or a hypothesisunfold replace a defined constant by its RHS in the goalunfold... in H ... or a hypothesisdestruct... as... case analysis on values of inductively definedtypesinduction... with... induction on values of inductively defined typesinversion reason by injectivity and distinctness of construc-torsremember (e) as x give a name (x) to an expression (e) so that we candestruct x without “losing” eassert (e) as H introduce a “local lemma” e and call it HFigure 7-1 Tactics we’ve seen so farnames to expressions of other sorts (numbers, functions, types, type func-tions, . . . ).Definition plus_fact : Prop := plus 2 2 = 4.Now we can use this name in any situation where a proposition isexpected—for example, as the subject of a theorem.Theorem plus_fact_is_true :plus_fact.(Because of the Definition, the proof of this theorem involves an unfoldin addition to the usual reflexivity.)So far, all the propositions we have seen are equality propositions. But wecan build on equality propositions to make other sorts of claims. For exam-ple, what does it mean to claim that “a number n is even”? We have alreadydefined a function that tests evenness, so one reasonable definition could be“n is even iff evenb n = true.”58 7 More On InductionDefinition even (n:nat) :=evenb n = true.This defines even as a parameterized proposition. It can be thought of as afunction that, when applied to a number n, yields a proposition claiming thatn is even.The type of even is nat→Prop. This type can be pronounced in two ways:either simply “even is a function from numbers to propositions” or, perhapsmore helpfully, “even is a family of propositions, indexed by a number n.”Functions returning propositions are completely first-class citizens in Coq;we can do all the same sorts of things with them as with any other kinds offunctions. We can, for example, use them in other definitions.Definition even_n__even_SSn (n:nat) :=(even n) → (even (S (S n))).We can define them to take multiple arguments...Definition between (n m o: nat) : Prop :=andb (ble_nat n o) (ble_nat o m) = true.... and then partially apply them.Definition teen : nat→Prop := between 13 19.And we can pass propositions—even parameterized propositions—as argu-ments to functions.Definition true_for_zero (P:nat→Prop) : Prop :=P 0.Definition preserved_by_S (P:nat→Prop) : Prop :=forall n0, P n0→ P (S n0).Definition true_for_all_numbers (P:nat→Prop) : Prop :=forall n, P n.Definition nat_induction (P:nat→Prop) : Prop :=(true_for_zero P)→ (preserved_by_S P)→ (true_for_all_numbers P).The last of these is interesting. If we unfold all the definitions, here is what itmeans in concrete terms.7.3 Induction Axioms 59Example nat_induction_example : forall (P:nat→Prop),nat_induction P= ( (P 0)→ (forall n0, P n0→ P (S n0))→ (forall n, P n)).That is, nat_induction expresses exactly the principle of induction for nat-ural numbers that we’ve been using for most of our proofs about numbers.Indeed, we can use the induction tactic to prove very straightforwardlythat nat_induction P holds for all P.Theorem our_nat_induction_works : forall (P:nat→Prop),nat_induction P.7.3 Induction AxiomsIn fact, the connection between nat_induction and Coq’s built-in princi-ple of induction is even closer than this suggests: modulo bound variablenames, they are precisely the same!Check nat_ind.Inat_ind : forall P : nat → Prop,P 0→ (forall n : nat, P n → P (S n))→ forall n : nat, P nThe first “:” here can be pronounced “...records the truth of the proposi-tion...” In general, every time we declare a new datatype t with Inductive,Coq automatically generates an axiom t_ind (i.e., a theorem whose truth isassumed rather than being proved from other axioms). This axiom expressesthe induction principle for t. The induction tactic is a straightforwardwrapper that, at its core, simply performs apply t_ind.To see this more clearly, let’s experiment a little with using apply nat_inddirectly, instead of induction, to carry out some proofs. First, here is a di-rect proof of the validity of our formulation of the induction principle. Theproof amounts to observing that, after unfolding the names we defined, ourprinciple coincides with the built-in one.Theorem our_nat_induction_works0:forall P, nat_induction P.Proof.intros P.60 7 More On Inductionunfold nat_induction, true_for_zero,preserved_by_S,


View Full Document

Penn CIS 500 - More On Induction

Download More On Induction
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view More On Induction and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view More On Induction 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?