PrefaceIntroductionI Functional ProgrammingBasicsEnumerated 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 problemA Simple EvaluatorMore On InductionII LogicProgramming with PropositionsLogical ConnectivesMore on InductionRelations as PropositionsThe Computational View of ProofsDependent TypesIII Operational SemanticsSemantics of While ProgramsA Small-Step Abstract MachineBasic Coq AutomationIV TypesA First Taste of TypesThe Simply Typed Lambda-CalculusProducts and RecordsSubtyping4 Programming with Types4.1 PolymorphismWe’ve been working a lot with lists of numbers, but clearly programs alsoneed to be able to manipulate lists whose elements are drawn from othertypes—lists of strings, lists of booleans, lists of lists, etc. We could define anew inductive datatype for each of these...Inductive boollist : Set :=| bool_nil : boollist| bool_cons : bool → boollist → boollist.... but this would quickly become tedious, partly because we have to makeup different constructor names for each datatype but mostly because wewould also need to define new versions of all our list manipulating functions(length, rev, etc.) for each new datatype definition.To avoid all this repetition, Coq supports polymorphic inductive type defi-nitions. For example, here is a polymorphic list data type.Inductive list (X:Set) : Set :=| nil : list X| cons : X → list X → list X.This is exactly like the definition of natlist on page 28 except that thenat argument to the cons constructor has been replaced by an arbitraryset X, a binding for X has been added to the first line, and the occurrencesof natlist in the types of the constructors have been replaced by list X.(We’re able to re-use the constructor names nil and cons because the earlierdefinition of natlist was inside of a Module definition that is now out ofscope.)With this definition, when we use the constructors nil and cons to buildlists, we need to specify what sort of lists we are building—that is, nil andcons are now polymorphic constructors.4.1 Polymorphism 39Check nil.Inil: forall X : Set, list XCheck cons.Icons: forall X : Set, X → list X → list XThe “forall X” in these types should be read as an additional argumentto the constructors that determines the expected types of the arguments thatfollow. When nil and cons are used, these arguments are supplied in thesame way as the others. For example, the list containing 2 and 1 is written(cons nat 2 (cons nat 1 (nil nat))).We can now go back and make polymorphic versions of all the list-processing functions that we wrote before. Here is length, for example.Fixpoint length (X:Set) (l:list X) {struct l} : nat :=match l with| nil => 0| cons h t => S (length X t)end.Note that the uses of nil and cons in match patterns do not require anytype annotations: we already know that the list l contains elements of typeX, so there’s no reason to include X in the pattern. (More formally, the set X is aparameter of the whole definition of list, not of the individual constructors.So when we pattern)Just as we did with nil and cons, to use length we apply it first to atype and then to its list argument:Example test_length1 :length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.To use our length with other kinds of lists, we simply instantiate it with anappropriate type parameter:Example test_length2 :length bool (cons bool true (nil bool)) = 1.Similarly, here is a polymorphic app function.Fixpoint app (X : Set) (l1 l2 : list X) {struct l1}: (list X) :=40 4 Programming with Typesmatch l1 with| nil => l2| cons h t => cons X h (app X t l2)end.Poly.v also gives polymorphic variants of snoc and rev.4.2 Implicit Type ArgumentsWhenever we use a polymorphic function, we need to pass it one or moresets in addition to its other arguments. For example, the recursive call in thebody of the length function above must pass along the set X. But this is abit heavy and verbose: Since the second argument to length is a list of Xs,it seems entirely obvious that the first argument can only be X—why shouldwe have to write it explicitly?Fortunately, Coq permits us to avoid this kind of redundancy. In place ofany type argument,1we can write the implicit argument _ , which can be read“Please figure out for yourself what set belongs here.” More precisely, whenCoq encounters a _ , it will attempt to unify all locally available information—the type of the function being applied, the types of the other arguments, andthe type expected by the context in which the application appears—to deter-mine what concrete set should replace the _.Using implicit arguments, the length function can be written like this:Fixpoint length0(X:Set) (l:list X) {struct l} : nat :=match l with| nil => 0| cons h t => S (length0_ t)end.In this instance, the savings of writing _ instead of X is small. But in othercases the difference is significant. For example, suppose we want to writedown a list containing the numbers 1, 2, and 3. Instead of writingDefinition l123 :=cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).we can use implicit arguments to write:Definition l1230:= cons _ 1 (cons _ 2 (cons _ 3 (nil _))).1. Actually, _ can be used in place of any argument, as long as there is enough local informa-tion that Coq can determine what value is intended; but this feature is mainly used for typearguments.4.3 Polymorphic Pairs 41Better yet, we can use implicit arguments in the right-hand side of Notationdeclarations to obtain the same abbreviations for constructing polymorphiclists as we had before for lists of numbers.Notation "x :: y" := (cons _ x y)(at level 60, right associativity).Notation "[ ]" := (nil _).Notation "[ x , .. , y ]" := (cons _ x .. (cons _ y []) ..).Notation "x ++ y" := (app _ x y)(at level 60, right associativity).Now our list can be written just the way we’d hope:Definition l12300:= [1,