(**Itisconvenienttobeabletotestdefinitionsbeforestartingtoprovethingsaboutthem.Wecanverifythatoursemanticsissensiblebyevaluatingsomesampleuses,usingthecommand%\index{Vernacularcommands!Eval}%[Eval].Thiscommandtakesanargumentexpressinga%\index{reductionstrategy}\emph{%#<i>#reductionstrategy#</i>#%}%,oran%``%#"#order of evaluation.#"#%''%UnlikewithML,whichhardcodesan%\emph{%#<i>#eager#</i>#%}%reductionstrategy,orHaskell,whichhardcodesa%\emph{%#<i>#lazy#</i>#%}%strategy,inCoqwearefreetochoosebetweentheseandmanyotherordersofevaluation,becauseallCoqprogramsterminate.Infact,Coqsilentlychecked%\index{terminationchecking}%terminationofour[Fixpoint]definitionabove,usingasimpleheuristicbasedonmonotonicallydecreasingsizeofargumentsacrossrecursivecalls.
(**Thoughapencil-and-paperproofmightclockoutatthispoint,writing%``%#"#by a routine induction on [e],#"#%''%itturnsoutnottomakesensetoattackthisproofdirectly.Weneedtousethestandardtrickof%\emph{%#<i>#strengtheningtheinductionhypothesis#</i>#%}%.Wedothatbyprovinganauxiliarylemma:
(**Thoughapencil-and-paperproofmightclockoutatthispoint,writing%``%#"#by a routine induction on [e],#"#%''%itturnsoutnottomakesensetoattackthisproofdirectly.Weneedtousethestandardtrickof%\index{strengtheningtheinductionhypothesis}\emph{%#<i>#strengtheningtheinductionhypothesis#</i>#%}%.Wedothatbyprovinganauxiliarylemma,usingthecommand[Lemma]thatisasynonymfor[Theorem],conventionallyusedforlessimportanttheoremsthatappearintheproofsofprimarytheorems.%\index{Vernacularcommands!Lemma}%*)