Unformatted text preview:

PrefaceIntroductionI Sets and FunctionsBasicsEnumerated TypesBooleansNumbersProof by SimplificationThe intros TacticProof by RewritingCase AnalysisNaming CasesInductionFormal vs. Informal ProofsProofs Within ProofsPairs and ListsFormal vs. Informal ProofsPairs of NumbersLists of NumbersReasoning About ListsOptionsThe apply TacticVarying the Induction HypothesisProgramming with TypesPolymorphismImplicit Type ArgumentsPolymorphic PairsPolymorphic OptionsProgramming With FunctionsHigher-Order FunctionsPartial applicationAnonymous FunctionsPolymorphic Lists, ContinuedThe unfold TacticFunctions as DataMore Coq TacticsInversionApplying Tactics in HypothesesUsing destruct on Compound ExpressionsThe remember TacticThe apply ... with ... TacticChallenge problemII LogicMore On InductionQuick ReviewProgramming with PropositionsInduction AxiomsInduction Principles for Other DatatypesA Closer Look at Induction HypothesesA Closer Look at the induction TacticGeneralizing the Induction HypothesisDependent TypesIII Operational SemanticsSemantics of While ProgramsA Small-Step Abstract MachineBasic Coq AutomationIV TypesA First Taste of TypesThe Simply Typed Lambda-CalculusProducts and RecordsSubtypingReferences7 More On InductionNOTE: This is a preliminary version of this chapter. A complete, revisedversion will be released on Wednesday.7.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.7.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 farOne 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 givennames 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-58 7 More On Inductionple, 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.”Definition 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).7.3 Induction Axioms 59The last of these is interesting. If we unfold all the definitions, here is what itmeans in concrete terms.Example 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


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?