Georges Gonthier

Assia Mahboubi

S S Ufhfq Erh F F F F F F F F F F F F F F F F F F F F F F F F F F F F F Ss

An introduction to small scale reection in Coq

his tutoril presents the sre)et extension to the goq systemF his extension onsists of n extension to the goq lnguge of sriptD nd of set of lirriesD originting from the forml proof of the pour golor theoremF his tutoril proposes guided tour in some of the si lirries distriuted in the sre)et pkgeF st fouses on the pplition of the smll sle re)etion methodology to the formliztion of (nite ojets in intuitionisti type theoryF Key-words: CoqD SSReflectD re)etionD type theory * This work has been

1 Introduction 3

2 Instructions for the exercises 5

3 A script language for structured proofs 7

QFI equents s stks F F F F F F F F F F F F F F F F F F F F F F F F F F U QFP gontrol )ow F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F IH QFPFI sndenttion nd ullets F F F F F F F F F F F F F F F F F F F IH QFPFP ermintors F F F F F F F F F F F F F F F F F F F F F F F F F F II QFQ qol seletors F F F F F F F F F F F F F F F F F F F F F F F F F F F F F IR QFR porwrd hiningD kwrd hining F F F F F F F F F F F F F F F F IS QFS wore SSReflect feturesD on n exmple F F F F F F F F F F F F F IV 4 Small scale reection, rst examples 21 RFI he two sides of dedution F F F F F F F F F F F F F F F F F F F F F PI RFIFI snterpreting ssumptions F F F F F F F F F F F F F F F F F F PP RFIFP peilizing ssumptions F F F F F F F F F F F F F F F F F F F PQ RFIFQ snterpreting gols F F F F F F F F F F F F F F F F F F F F F F F PR RFIFR he reflect predite F F F F F F F F F F F F F F F F F F F F PR RFIFS snterpreting equivlenes F F F F F F F F F F F F F F F F F F PS RFIFT roving reflect equivlenes F F F F F F F F F F F F F F F F PT RFP ixerisesX sequenes F F F F F F F F F F F F F F F F F F F F F F F F F PU RFQ ixerisesX foolen equlities F F F F F F F F F F F F F F F F F F F F PW
5 Type inference using canonical structures 31 SFI gnonil trutures F F F F F F F F F F F F F F F F F F F F F F F F F QI SFP gnonil onstrutions F F F F F F F F F F F F F F F F F F F F F F F QS SFQ redtypesX nonil strutures for nottions F F F F F F F F F F F QU 6 Finite objects in SSReflect 39

TFI pinite types F F F F F F F F F F F F F F F F F F F F F F F F F F F F F F QW TFIFI pinite types onstrutions F F F F F F F F F F F F F F F F F F QW TFIFP grdinlityD set opertions F F F F F F F F F F F F F F F F F F RH TFIFQ oolen qunti(ers F F F F F F F F F F F F F F F F F F F F F F RP TFIFR ixmpleX depth (rst serh lgorithm F F F F F F F F F F RQ TFP igm types with deidle spei(tions F F F F F F F F F F F F F RV TFQ pinite funtionsD (nite sets F F F F F F F F F F F F F F F F F F F F F F SI 1 Introduction mllEsle re)etion is forml proof methodology sed on the pervsive use of omputtion with symoli representtionsF ymoli representtions re usully hidden in trditionl omputtionl re)etion @eFgFD s used in the R CoqheIH ringD or romegaAX they re generted onEtheE)y y some heuristi lgorithm nd diretly fed to some deision or simpli(tion proedure whose output is trnslted k to 4logil4 form efore eing displyed to the userF fy ontrstD in smllEsle re)etion symoli representtions re uiquitousY the sttements of mny topElevel lemmsD nd of most proof sugolsD expliE itly ontin symoli representtionsY trnsltion etween logil nd symoli representtions is performed under the expliitD (neEgrined ontrol of the proof sriptF he e0ieny of smllEsle re)etion hinges on the ft tht (xing prtiE ulr symoli representtion strongly direts the ehvior of theoremEproverX vogil se nlysis is done y enumerting the symols ording to their indutive typeX the representtion desries whih ses should e onsideredF wny logil funtions nd predites re represented y onrete funE tions on the symoli representtionD whih n e omputed one @prt ofA the symoli representtion of ojets is knownX the representtion desries wht should e done in eh seF hus y ontrolling the representtion we lso ontrol the utomted ehvE ior of the theorem proverD whih n e quite omplexD for exmple if prediE te is represented y sophistited deision proedureF he rel strength of smllEsle re)etionD howeverD is tht even very simple representtions provide useful proeduresF por exmpleD the truthEtle representtion of onnetivesD evluted leftEtoEright on the foolen representtion of propositionsD provides su0ient utomtion for most propositionl resoningF mllEsle re)etion de(nes sis for dividing the proof worklod etween the user nd the proverX the prover engine provides omputtion nd dtse funtions @vi prtil evlutionD nd de(nition nd type lookupD respetivelyAD nd the user sript guides the exeution of these funtionsD step y stepF ser sripts omprise three kinds of stepsX hedution steps diretly speify prt of the onstrution of the proofD either top down @soElled forwrd stepsAD or ottomEup @kwrd stepsAF e re)etion step tht swithes etween logil nd symoli representtion is just speil kind of dedutive stepF fookkeeping steps mnge the proof ontextD introduingD renmingD disE hrgingD or splitting onstnts nd ssumptionsF gseEsplitting on symE oli representtions is n e0ient wy to drive the prover engineD euse most of the dt required for the splitting n e retrieved from the repE resenttion typeD nd euse speilizing single representtion often triggers the evlution of severl representtion funtionsF ewriting steps use equtions to lolly hnge prts of the gol or sE sumptionsF ewriting is often used to omplement prtil evlutionD yE pssing unknown prmeters @eFgFD simplifying (b && false) to falseAF yviouslyD it9s lso used to implement equtionl resoning t the logil levelD for instneD swithing to di'erent representtionF S st is hrteristi of the smllEsle re)etion style tht the three kinds of steps re roughly equinumerousD nd interlevedY there re strong resons for thisD hief mong them the ft tht gols nd ontexts tend to grow rpidly through the prtil evlution of representtionsF his mkes it imprtil to emed most intermedite gols in the proof sript E the soElled delrtive style of proofD whih hinges on the exlusive use of forwrd stepsF his lso mens tht suterm seletionD espeilly in rewritingD is often n issueF he si Coq tti lnguge is not well dpted s suh to smllEsle re)etion proofsF st is hevily ised towrds kwrd stepsD with little support for forwrd stepsD or even sript lyoutF wny of the si ttis implement frgile ontext mnipultion heuristis whih hinder preise ookkeepingY on the other hnd the underEutilized 4intro ptterns4 provide exellent support for se splittingF sn the present doumentD we rie)y summrize in the two (rst setions some slient spets of the SSReflect extension to the Coq lnguge of sript whih origintes from the proof of the pour golor theorem qonHVF he SSReflect lnguge in itself n e onsidered s n lterntive idiom to the one proposed y the stndrd distriution of the Coq systemD introduing some improvements @term seletionD enhned rewritingD roustness of sriptsDFFFAF fut the min ontriution of the reserh line drwn y the suessful forml proof of the pour golor theorem lies in the smll sle re)etion methodologyF he two lst setions of this tutoril propose guided tour in the si lirries distriuted with the SSReflect extensionF he im of this presenttion is to set out the design ptterns whih govern the de(nition of ojetsD nd the struture of the theories developed on these ojetsD inluding the ruil use of type lsses nd nonil struturesF hue to time nd spe onstrintsD we only present omintori dt struturesD nd do not ddress the higherElevel lirries like the ones on (nite groups or on mtriesF his would deserve nother tutorilF e minly present here how the formliztion of nite ojets ene(ts from smll sle re)etionF et we hope tht this doument will help the reder to get strted with the lirryD nd to strt uilding further their own formliztion on top of itF 2 Instructions for the exercises his tutoril is intended for n udiene lredy experiened with the notion of forml proof nd with very si knowledge of the Coq systemF por instne we do not rell the si syntx nd priniples of the system or its elementry ttisF e still hope tht the tutoril n e followed y novieF he online referene mnul of the Coq system n e found on the Coq wesite heIHD s well s the html doumenttion of Coq stndrd lirriesF he reder might lso ene(t from further reding on the Coq systemD like fgHRF he ltest version of the SSReflect lnguge nd lirries n e downE loded hereX http://www.msr-inria.inria.fr/Projects/math-components/ he distriution ontins soures (les for the CoqheIH lnguge extenE sionD the SSReflect lirriesD nd detiled instrutions for the instlltion of the systemF he (rst prt of this tutoril is devoted to quik guided tour T of the SSReflect lngugeF e do not however inlude the full doumentE tion of the lngugeD ut we still try to remin s selfEontined s possileF st is nevertheless good prtie to keep the SSReflect mnulqw t hnd while reding the present tutorilD s we will sometimes refer to it for further explntionF ixerises should e done in (le strting with the following innttion1 X Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.

Require Import path choice fintype tuple finfun finset.

Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits.

whih lods the required lirries nd sets the impliit rguments options used throughout the lirries nd this tutorilF wost of the exerises onsist in provE ing results tht re lredy present in the lirries distriuted with SSReflectF hen n exerise onsists in de(ning onstnt whih is lredy present in the ontext @in the loded lirriesAD the user is sked to reEde(ne it using the sme nmeD pre(xed y tuto_ to void nme lshesF pei(tions to e formlly proved y the reder however usully feture the originl onstnts ville in the SSReflect lirriesF hen n exerise onsists in proving spei(E tions tht re lredy present in the ontextD the user is sked to reEprove the spei(tion using the sme nmeD pre(xed y tuto_F hese redundnt lemmsD whose proofs re left s exerisesD speify the tul SSReflect onstnts @nd not the tuto_Epre(xed onesAD so tht the user n ene(t from ll the dditionl results lredy present in SSReflect lirriesF ome exerises re not neessry intended to e easily dole y eginnerF hey most often omprise severl similr questionsD nd the reder should e le to understnd how to solve the lst questions fter hving red the solution of the (rst oneF olutions nd omments n e found t the following ddressX http://www.msr-inria.inria.fr/Projects/math-components/ olutions to the exerises sometimes give useful informtion for the rest of the setionF he reder is dvised to red the solution of n exerise efore trying the next oneF por dvned usersD further doumenttion is ville in eh SSReflect lirry .v (le hederF ih heder summrizes the min onepts nd nottions de(ned in the lirry nd gives some omments on the use of the ojets de(nedF ee for instne the heder of fintype.vF e enourge every reder of the present tutoril to susrie to the SS-Reflect user miling listF o susrieD send n emil entitled 9susrie9 toX ssreflect@msr-inria.inria.fr his miling list should e used for ny further question or omment on the exerises of this tutoril or on ny development using the SSReflect extenE sionF 3 A script language for structured proofs e sizle frtion of proof sripts onsists of steps tht do not 4prove4 nything newD ut insted perform menil ookkeeping tsks suh s seleting the nmes of onstnts nd ssumptions or splitting onjuntsF sndeedD SSReflect sripts pper to divide evenly etween ookkeepingD forml lger @rewritingAD nd tul dedutionF elthough they re logilly trivilD ookkeeping steps re exE tremely importnt euse they de(ne the struture of the dt)ow of proof sriptF his is espeilly true for re)etionEsed proofsD whih often involve lrge numers of onstnts nd ssumptionsF qood ookkeeping onsists in lE wys expliitly delring @iFeFD nmingA ll new onstnts nd ssumptions in the sriptD nd systemtilly pruning irrelevnt onstnts nd ssumptions in the ontextF his is essentil in the ontext of n intertive development enviE ronment @shiAD euse it filittes nvigting the proofD llowing to instntly 4jump k4 to the point t whih questionle ssumption ws ddedD nd to (nd relevnt ssumptions y rowsing the pruned ontextF hile novie or sul Coq users my (nd the utomti nme seletion feture of Coq onvenientD this feture severely undermines the redility nd mintinilE ity of proof sriptsD muh like utomti vrile delrtion in progrmming lngugesF he SSReflect ttis re therefore designed to support preise ookkeeping nd to eliminte nme genertion heuristisF he ookkeeping feE tures of SSReflect re implemented s ttils @or pseudoEttilsAD shred ross most SSReflect ttisD nd thus form the foundtion of the SSReflect proof lngugeF to e proved " the rest of the gol n e seen s prt of the proof ontext tht hppens to e elow the lineF roweverD lthough they re logilly equivlentD there re fundmentl difE ferenes etween onstnts nd fts on the one hndD nd vriles nd ssumpE tions on the othersF gonstnts nd fts re unorderedD ut named expliitly in the proof textY vriles nd ssumptions re orderedD ut unnamedX the disply nmes of vriles my hnge t ny time euse of αEonversionF imilrlyD si dedutive steps suh s apply n only operte on the gol euse the qllin terms tht ontrol their tion @eFgFD the type of the lemm used y applyA only provide unnmed ound vrilesF2 ine the proof sript n only refer diretly to the ontextD it must onstntly shift delrtions from the gol to the ontext nd onversely in etween dedutive stepsF sn SSReflect these moves re performed y two tacticals =>9 nd :9D so tht the ookkeeping required y dedutive step n e diretly ssoited to tht stepD nd tht ttis in n SSReflect sript orrespond to tul logil steps in the proof rther thn merely shu1e ftsF he =>9 ttil moves fts nd onstnts from elow the line to vriles nd hypotheses ove the lineX it performs introductionF he :9 ttil moves things the other wy roundX it performs dischargeF pigure IX e pure introdution step pigure PX e pure dishrge step tillD some isolted ookkeeping is unvoidleD suh s nming vriles nd ssumptions t the eginning of proofF SSReflect provides spei( move tti for this purposeY out one out of every six ttis is moveF xow move does essentilly nothingX it is mostly pleholder for =>9 nd :9F he =>9 ttil moves vrilesD lol de(nitionsD nd ssumptions to the ontextD while the :9 ttil moves fts nd onstnts to the golF por exmpleD the proof of3 W where move does nothingD ut => m n lenm hnges the vriles nd ssumpE tion of the gol in the onstnts m n : nat nd the ft lenm : n <= mD thus exposing the onlusion m -n + n = mD s displyed on (gure IF his is exE tly wht the speilized Coq tti intros m n lenm would doD ut =>9 is muh more generl @see qwAF he :9 ttil is the onverse of =>9X it removes fts nd onstnts from the ontext y turning them into vriles nd ssumptionsF hus s displyed on (gure PD the ttiX move: m lenm.

turns k m nd lenm into vrile nd n ssumptionD removing them from the proof ontextD nd hnging the gol to forall m, n <= m -> m -n + n = m.

whih n e proved y indution on n using elim nF feuse they re ttilsD :9 nd =>9 n e ominedD s in move: m lenm => p lenp.

simultneously renmes m nd lenm into p nd lenpD respetivelyD y (rst turning them into unnmed vrilesD then turning these vriles k into onstnts nd ftsF purthermoreD SSReflect rede(nes the si Coq ttis caseD elimD nd apply so tht they n tke etter dvntge of 9:9 nd =>9F hese Coq ttis require n rgument from the ontext ut operte on the golF heir SSReflect ounterprts use the (rst vrile or onstnt of the gol instedD so they re purely dedutiveX they do not use or hnge the proof ontextF here is no loss sine :9 n redily e used to supply the required vrileY for instne the proof of the subnK lemm ould ontinue with n indution on nX elim: n.

his tti removes n from the ontextD following the semnti of the 9:9 disE hrge ttilF ixperiene shows tht this feture helps ontrolling the otherE wise ever growing size of the ontextF his defult ehvior n nonetheless e turned o' y the vrintX elim: (n).

where the generlized ojet is not pure identi(er ny longerF fetter yetD this n e omined with previous move nd with the rnhing version of the => ttil @desried in qwAD to enpsulte the indutive step in single ommndX would renme m into pD ut leve n extr ssumption n <= p in the golF fsi ttis like apply nd elim n lso e used without the 9:9 ttilX for exmple we n diretly strt proof of subnK y indution on the top vrile m with elim=> [|m IHm] n le_n_m.

Control ow

3.2.1 Indentation and bullets he liner development of Coq sripts gives little informtion on the struture of the proof other thn the one provided y the progrmmer @tultionsD omE mentsFFFAF sn dditionD replying proof fter some hnges in the sttement to e proved will usully not disply enough informtion to distinguish etween the vrious rnhes of se nlysis for instneF o help the user with this orE gniztion of the proof sript t development timeD SSReflect provides some ullets to highlight the struture of rnhing proofsF he ville ullets re -D + nd *F gomined with tultionD this highlights four nested levels of rnhing @the deepest se we hve ever enountered is threeAF sndeedD the use of simplifying nd losing swithes @see setion QFSAD of termintors @see setion QFPFPA nd seletors @see setion QFQA is powerful enough to void needing more thn two levels of indenttion most of the timeF xote tht these indenttion levels nd ullets hve no forml meningX the ft tht n indented sript is tully well indented is only gurnteed if eh prgrph ends with losing tti like the termintors of setion QFPFPF rere is wht frgment of suh strutured sript n look likeX case E1:

(abezoutn _ _) => [[| k1] [| k2]].
-rewrite !muln0 !gexpn0 mulg1 => H1. move/eqP: (sym_equal F0); rewrite -H1 orderg1 eqn_mul1. by case/andP; move/eqP. -rewrite muln0 gexpn0 mulg1 => H1.

have F1: t %| t * S k2.+1 -1. apply: (@dvdn_trans (orderg x)); first by rewrite F0; exact: dvdn_mull. rewrite orderg_dvd; apply/eqP; apply: (mulgI x). rewrite -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //. by move: P1; case t. rewrite dvdn_subr in F1; last by exact: dvdn_mulr. + rewrite H1 F0 -{2}(muln1 (p ^l)); congr (_ * _). by apply/eqP; rewrite -dvdn1. + by move: P1; case:

(t) => [| [| s1]].
-rewrite muln0 gexpn0 mul1g => H1. ... he reder is not expeted to understnd wht this ode proves or doesF fut this gives )vor of wht orretly indented sript should look like nd illustrtes good use of the by pre(x termintor @see setion QFPFPAF

Terminators

gonsider the following dummy exmpleD where .+1 is nottion for the suessor opertion on nturl numers @iFeF the S onstrutor of the nat indutive typeAX he proof of foo goes y indutionD thnks to line 5F vine 6 solves the (rst gol genertedD nd the rest of the sript solves the seond nd lst golF xow if we reply the proof fter hnging vlue 0 into 1 in the de(nition of fD line 6 does not solve the (rst se ny moreF fut y identD line 7 D whih is ment to pply only to the seond golD is now legl opertion on the (rst golF rene the sript reks on line 8D whih is not relevnt to the gol t hndF his phenomenon n e oserved on muh lrger slesD nd turns the mintenne of proof sripts into n extremely tedious tskF o further struture sriptsD SSReflect supplies terminating ttils to expliitly lose o' ttisF hen replying sriptsD we then hve the nie propE erty tht n error immeditely ours when losed tti fils to prove its sugolF st is hene reommended prtie tht the proof of ny sugol should end with tti whih fails if it does not solve the current goalF tndrd Coq lredy provides some ttis of this kindD like discriminateD contradiction or assumptionF SSReflect provides generi ttil whih turns ny tti into losing oneF sts generl syntx isX by tactic . ine it is de(ned using Coq9s toplevel tti lnguge LtacD the done tti n possily e ustomized y the userD for instne to inlude n auto ttiF o ensure omptiility with other users9 development it is however etter prtie to rede(ne n enrihed my_done tti if neededF enother nturl nd ommon wy of losing gol is to pply lemm whih is the exact one needed for the gol to e solvedF por instneX exact: MyLemma.

1 Fixpoint f n := if n is n'.+1 then (f n').+2 else 0. 2 3 Lemma foo forall n, f (2 * n) = f n + f n.

Lemma tauto2 : (

A -> B) -> (B -> C) -> A -> C. Proof. ... Qed. Lemma tauto3 : A /\ B <-> B /\ A. Proof. ... Qed.
End Tauto.

our proof sript should ome in ple of the dotsD etween Proof. nd Qed. our proof is (nished when the system rises messge sying soF hen the Qed ommnd reheks the proof term onstruted y your sriptF sn the followingD we only give the sttements of the lemms to e proved nd do not repet Proof nd Qed ny longerF he stndrd Coq setion mehnism llows to ftorize strtions gloE llyF rere in the setion prmeters A B C re (xedD nd they re dishrged fter the setion Tauto is losed y the ommnd End TautoF Exercise 3.2.2 rove the following sttementsX Section MoreBasics. Variables A B C : Prop. Variable P : nat -> Prop.

Lemma foo1 : ~(exists x, P x) -> forall x, ~P x. Lemma foo2 : (exists x, A -> P x) -> (forall x, ~P x) -> ~A.

End MoreBasics.

rintX ememer tht the intuitionisti negtion ~A is nottion for A -> FalseF elso rememer tht the proof of n existentil sttement is pir of the witness nd its proofD so you n destrut this pir y the case ommndF Exercise 3.2.3 he SSReflect ssrnat lirry ruilly rede(nes the omE prison predites nd opertions on nturl numersF sn prtiulrD omprE isons re foolen preditesD insted of the indutive versions provided y Coq stndrd lirryF se the Search nd Check ommnds @see setion U or qwAF por instne the ommnd Search _ (_ < _).

Goal selectors

hen omposing ttisD the two ttils first nd last let the user restrit the pplition of tti to only one of the sugols generted y the previous ttiF his overs the frequent ses where tti genertes two or more sugolsD one of whih n e esily disposed ofF his is n other powerful wy to linerize sriptsD sine it very often hppens tht trivil sugol n e solved y shorter ttiF por instneD the ttiX tactic 1 ; last by tactic 2 .

tries to solve the lst sugol generted y tactic 1 using the tactic 3.4 Forward chaining, backward chaining porwrd resoning strutures the sript y expliitly speifying some ssumpE tions to e dded to the proof ontextF st is losely ssoited with the delrE tive style of proofD sine n extensive use of these highlighted sttements mke the sript loser to @very detiledA text ook proofF porwrd hining ttis llow to stte n intermedite lemm nd strt piee of sript dedited to the proof of this sttementF he use of losing ttis @see setion QFPFPA nd of indenttion mkes the portion of the sript uilding the proof of the intermedite sttement synttilly expliitF

The have tactic.

he min SSReflect forwrd resoning tti is the have ttiF st n e used in two modesX one strts new @suAproof for n intermedite result in the min proofD nd the other provides proof term for this intermedite step expliitlyF sn the (rst modeD the syntx of have in its defetive form isX have: term .

his tti supports open syntx for term X no surrounding prenthesis re neededF epplied to gol GD it genertes (rst sugol requiring proof of term is the ontext of GF he di'erene with the stndrd Coq tti is tht the seond sugol generted is of the form term -> GD where term eomes the new top ssumptionD insted of eing introdued with fresh nmeF por instneD onsider the following golX where the sttement of n esy lemm n e followed y the short proof losing itD like inX have : forall x y, x + y = y + x by move=> x y; rewrite addnC.

he have tti n e omined with SSReflect9s wildrd mehnismX pleholder mterilized y 9_9 represents term whose type is strtedF por instneD the ttiX have: _ * 0 = 0.

is equivlent toX have: forall n : nat, n * 0 = 0.

sn the sme spiritD nonEinferred impliit rguments re strtedF por instneD the ttiX have: forall x y, (x, y) = (x, y + 0).

RR n°7392

IU opens new sugol to prove thtX forall (T : Type)(x : T)(y : nat), (x, y)= (x, y + 0) en lterntive use of the have tti is to provide the expliit proof term for the intermedite lemmD using ttis of the formX have [ ident ] := term .

his tti retes new ssumption of type tht of term F sf the optionl ident is presentD this ssumption is introdued under the nme ident F xote tht the ody of the onstnt is lost for the userF eginD non inferred impliit rguments nd expliit holes re strtedF por instneD the ttiX have H := forall x, (x, x) = (x, x). dds to the ontext H : Type -> PropF his is shemti exmple ut the feture is speilly useful when for instne the proof term involves lemm with some hidden impliit rgumentsF Variants: the suff and wlog tactics.

es is often the se in mthemtil textooksD forwrd resoning my e used in slightly di'erent vrintsF yne of these vrints is to show tht the intermedite step L esily implies the initil gol GF fy esily we men here tht the proof of L ⇒ G is shorter thn the one of L itselfF his kind of resoning step usully strts withX st su0es to show tht FFFF his is suh frequent wy of resoning tht SSReflect hs vrint of the have tti lled suffices @whose ridged nme is suffAF he have nd suff ttis re equivlent nd hve the sme syntx ut the order of the generted sugols is swppedF enother useful onstrut is redutionD showing tht prtiulr se is in ft generl enough to entil generl propertyF his kind of resoning step usully strts withX ithout loss of generlityD we n ssume tht FFFF pormllyD this orresponds to the proof of gol G y introduing ut wlog_statement-> GF rene the user shll provide proof for oth (wlog_statement-> G)-> G nd wlog_statement-> GF his proof pttern is speilly useful when symmetry rgument simpli(es proofF SSReflect implements this kind of resoning step through the without loss ttiD whose short nme is wlogF sn its defetive formX wlog: / term . IV move=> d q1 q2 r1 r2. wlog: q1 q2 r1 r2 / q1 <= q2. by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith .

rere we suppose without loss of generality tht q1 <= q2D nd generlize the onstnts @nd possily ftsA q1 q2 r1 r2F he (rst gol generted fter the wlog tti is heneX

(forall q3 q4 r3 r4 : nat, q3 <= q4 -> q3 * d + r3 = q4 * d + r4 -> r3 < d -> r4 < d -> (q3, r3) = (q4, r4)) -> q1 * d + r1 = q2 * d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2) the seond one eingX q1 <= q2 -> q1 * d + r1 = q2 * d + r2 -> r1 < d -> r2 < d -> (q1, r1) = (q2, r2)
3.5 More SSReflect features, on an example ome importnt fetures of the SSReflect lnguge re not doumented furE ther in the present tutoril ut detiled desription n e found in qwF e hve minly omittedX the suterm seletion mehnism through ourrenes nd ptterns the enhned rewrite tti the more omplex introdution nd dishrge ptterns hese fetures will e illustrted y the solutions of the exerises of the next setionsF e give here n ount of the filities they provide on detiled exmple orrowed from qHWF he div lirry de(nes n iuliden division lgorithm edivn nd prediE te edivn_spec de(ning its spei(tionF Exercise 3.5.1 row is edivn progrmmedc ht is its spei(tionc his wy of speifying funtions nd reltions is systemtilly used in SSRe-flectF st o'ers powerful tool for se nlysis in proofs thnks to Coq seond order uni(tion ility @see exerises QFSFR nd RFQFIAF felowD let us prove tht edivn omplies with edivn_specF Qed.

he proof strts with n unfolding of the onstnt edivnD whih is performed y the rewrite /edivn ttiF his tti is followed y n introdution stepX we introdue m nd then [|d] performs seEsplit on dF his se splitting introdution is followed y his llows ny oolen formul b to e used in ontext where Coq would expet propositionF st is then interpreted s (is_true b)D iFeFD the proposition b = trueF goerions re elided y the prettyEprinterD so they re essentilly trnsprent to the userF hese oerions were in ft lredy present in the sttement of the lst two lemms of exerise QFPFQF husD Prop nd bool re truly omplementryX the former supports roust nturl dedutionD the ltter llows ruteEfore evlutionF SSReflect supE plies generi mehnism to hve the est of the two worlds nd move freely from propositionl version of deidle predite to its oolen versionF es result one of the motos of the smll sle re)etion methodology isX if predE ite is deidleD it should e de(ned through oolen prediteD possily ompnied with logil spei(tionsF he ookkeeping filities presented in setion Q re rfted to ese simulE tneous introdutionGgenerliztion of fts nd singD nming FFF opertionsF he SSReflect extension lso provides wy to ese the omintion of stk opertion immeditely followed y n interpretation of the ft eing pushedD tht is to sy to pply lemm to this ft efore pssing it to tti for deompositionD pplition nd so onF his proves speilly useful when interpreting oolen predites into logil onesF 4.1.1 Interpreting assumptions snterpreting n ssumption in the ontext of proof onsists in pplying orE respondene lemm to this ssumption efore generlizingD ndGor deomposing itF uh orrespondene lemm is lled view lemmaF por instneD with the extensive use of oolen re)etionD it is quite frequent to need to deompose the logil interprettion of @the oolen expression ofA ftD rther thn the ft itselfF his n e hieved y omintion of move : _ => _ swithesD s in the following sriptD where || is stndrd Coq nottion for the oolen disjuntionX Variables P Q : bool -> Prop. Hypothesis P2Q : forall a b, P (a || b) -> Q a.

Goal forall a, P (a || a) -> True. move=> a HPa; move: {HPa}(P2Q _ _ HPa) => HQa.

whih trnsforms the hypothesis HPa : P a whih hs een introdued from the initil sttement into HQa : Q aF sn this exmpleD the view lemm is P2QF his opertion is so ommon tht the tti shell hs spei( syntx for itF he following sriptsX Goal forall a, P (a || a) -> True. move=> a HPa; move/P2Q: HPa => HQa. xote tht in this de(nitionD we use the nonymous rgument feture of the SSReflect lnguge @see qwAF he progrm omputing the size of suh sequene n e written sX Variable (T : Type). Fixpoint size (s : seq T) := if s is _ :: s' then (size s').+1 else 0.

tking ene(t of the onditionl pttern feture of the SSReflect lnguge @see qwAF Exercise 4.2.1 rogrm the funtion tuto_cat tenting two sequenesF rere we tke dvntge of the Coq system Implicit Types feture @see heIHAF his llows to ind vrile nmes to given typeF rene the ode of this exerise strts with the delrtionsX Section Exo_4_2_1.w Variable A : Type. Implicit Types s : seq A. Implicit Types x : A. whih opens setion for the ode of this exeriseD delres lol prmeter A nd sets the type of ound vriles starting with s @respF xA to e of type ( seq A) @respF AAF nless the ound vrile is lredy delred with n expliit type in whih seD this ltter type is onsideredF he tul cat funtion of the seq lirry is equipped with the ++ in(x nottionF rove the lemmX Lemma tuto_size_cat : forall s1 s2, size (s1 ++ s2) = size s1 + size s2.

xote tht vrile s1 nd s2 re utomtilly delred with type (seq A)D without ny expliit stD thnks to the previous Implicit Types delrtionF rogrm the funtion tuto_lastD suh tht (tuto_last x s) returns the lst element of the sequene s if s is not empty nd otherwise returns xF rove the lemmX Lemma tuto_last_cat : forall x s1 s2, last x (s1 ++ s2) = last (last x s1) s2.

rogrm the funtions tuto_take @respF tuto_dropAD of typeX nat -> seq A -> seq A suh tht (tuto_take n s) @respF (tuto_drop n s)A omputes the pre(x of s of size n @respF the post(x of s skipping the n (rst elementsAD with defult vlue s @respF the empty sequene [::]AF roveX Lemma tuto_cat_take_drop : forall (n0 : nat)(s : seq A), take n0 s ++ drop n0 s = s.

rogrm the tuto_rot funtion suh tht (tuto_rot n s) is the irulr perE muttion of s of order nF rove thtX Lemma tuto_rot_addn : forall m n (s : seq A), m + n <= size s -> rot (m + n) s = rot m (rot n s).

End Exo_4_2_1.

por this lst proofD you will need more lemms out the funtion progrmmed in this exeriseF se the SSReflect Search ommnd to (nd the sttements you needF ou n lso try to guess their nme ording to the SSReflect nming onventionsD nd Check your guesses @see setion UAF gomining sequenes with oolen predites mkes possile to strt provE ing some omintori resultsF QH type eing n indutive type with two onstrutor @one for eh sideAD one n perform se nlysis on proof of (eq_dec x y)D hene se nlysis on the equlity or disEequlity of the two elements x nd yF sn eh rnhD proof of the ssertion vlid in this rnh is ville s it should e n rgument of the orresponding onstrutorF mll sle re)etion fvors the use of boolean predites insted of suh sum_bool typesF sndeedD unlike sum typesD oolen predites hve the ompuE ttionl ehvior expeted to let redution hndle dedutive steps tht only rely on truth tle vluesF he SSReflect ount of DecidableType is nmed eqTypeD nd its theory is developed in the eqtype lirryF he eqType struture n e thought of5 sX Module Equality.

Definition axiom T e := forall x y : T, reflect (x = y) (e x y).

Record mixin_of (T : Type) := Mixin { op : rel T; _ : axiom op }.

Record type := Pack { sort :> Type; _ : mixin_of sort End Equality.

his n e thought of s kind of sigm type pking type with signture nd spei(tionsF he signture + spei(tion prt is lled mixinF he tul oolen omprison of n eqType struture n e essed through the de(ned eq_op opertorX eq_op : forall T : eqType, rel T whih enjoys some in(x nottionsX (eq_op x y) is denoted y (x == y)D nd (~~(x == y)) y (x != y)F his opertor is de(ned y destruting TD nd its mixinF woreoverD we lso de(ne the eqP onstntX eqP : forall T : eqType, Equality.axiom eq_op whih esses the re)etion lemm ssoited to the oolen omprisonF Lemma tuto_eqVneq : forall (T : eqType) (x y : T), {x = y} + {x != y}.

rintX gonsider using view mehnisms for equivleneD gol nd ssumption interprettionF emrk X try strting the proof of eqVneq y the ttiX move=> T x y; case: eqP.

ht hppens thenc emrkX en lterntive to the se nlysis on (eqVneq x y) is simply simple se nlysis on the oolen vlue of (x == y)F fut one n lso perform se nlysis on (eqP x y)X one rnh fetures Reflect_true eq_xy where (eq_xy : x = y) nd the other rnh Reflect_false neq_xy where (neq_xy : ~(x = y))F fesides giving omputtionl ontent to veiniz equlityD the oolen reE ltion emedded in n eqType struture lso gives its deidility of ourseF en importnt onsequene of this deidility is the uniqueness of their equlity proofsX Theorem eq_irrelevance : forall (T : eqType) (x y : T), forall (e1 e2 : x = y), e1 = e2.

he uniqueness of equlity proofs for the nat nd bool types is onsequene of this theoremF oolen proof irrelevne is of prtiulr interest for the de(nition of sigm types with oolen spei(tions @see setion TFPAF 5 Type inference using canonical structures 5.1 Canonical Structures he typeEtheoreti formliztion of n lgeri or omintoril struture omE prises representtion types @usully only oneAD onstnts nd opertions on the type@sAD nd xioms stis(ed y the opertionsF ithin the propositionsEsE types frmework of CoqD the interfe for ll of these omponents n e uniE formly desried y olletion of dependent typesX the type of opertions depends on the representtion typeD nd the sttement @lso typeA of xE ioms depends on oth the representtion type nd the tul opertionsF sn the exmples nd exerises we hve enountered so frD typesD opertionsD nd xioms hve een represented y olletions of unundled prmetersD using the VariablesD ParametersD nd Hypothesis ommndsF QP hile this unundling llows for mximl )exiilityD it lso indues prolifE ertion of rguments tht is rpidly overwhelmingF e typil lgeri strutureD suh s ringD involves hlf dozen onstnts nd even more xiomsF woreover suh strutures re often nestedD eFgFD for the gyleyErmilton theorem @see the charpoly lirryD out of the sope of this tutorilA one needs to onsider the ring of polynomils over the ring of mtries over generl ommuttive ringF he size of the terms involved grows s C n D where C is the verge numer of seprte omponents of strutureD nd n is the struture nesting depthF por gyleyErmilton we would hve C = 15 nd n = 3D nd thus terms lrge enough to mke theorem proving imprtilD given tht lgorithms in userElevel ttis re more often thn not nonlinerF husD t the very lestD relted opertions nd xioms should e pked using Coq9s dependent reords @ΣEtypesAF rere is toy exmple for ommuttive groupX xote tht the four (rst rguments of bool_zmodule_mixin should e respeE tively boolD falseD (@id bool) nd addb @see the role of the @ )g in nE nex UAF sn ftD they hve een utomtilly inferred from the type of the other rgumentsF he :> symol fter the carrier (eld indites tht the carrier : zmodule -> Type projetion is in ft delred on the )y s co-ercionF ememer oerions provide n expliit sutyping mehnism to the hen we de(ne n in(x nottionX Notation "x \+ y" := (@zmadd _ x y)(at level 50,left associativity).

where _ is pleholder for n inhitnt of zmodule to e inserted y the type inferene mehnismF xow we n onveniently stte nd prove the following resultX

Lemma zmaddAC : forall (m : zmodule)(x y z : m),

x \+ y \+ z = x \+ z \+ y.

Exercise 5.1.1 rove tht zmadd is ssoitive nd ommuttiveF rove lemm zmaddACF efer to qw for the doumenttion of the SSReflect rewrite tti @in prtiulr pttern seletionAF estrt lgeri strutures re motivted y the ftoriztion of nottions nd theoremsD whih re supposed to e shared y every instne of given strutureF sn our toy exmpleD we hene expet ddition over foolens to inherit from the in(x \+ nottionD nd from the lemm zmaddACF fut the following ommndX Check false \+ true.

fils with the following error messgeX

Error: The term "false" has type "bool" while it is expected to have type "carrier ?15". sndeedD the expression false + true is nottion for @zmadd _ true falseD where _ is pleholder for n rgument of type zmoduleF ype inferene should hene unify the type bool of rguments true nd false with (carrier ?) where ? hs type zmoduleF here is no wy for uni(tion to guess now the ? hole n e (lled with bool_zmoduleF rowever Coq supports wy to provide hints to the uni(tion lgorithm lled Canonical Structures iWUF st n e viewed s n instne of uniE (tion hints s presented muh more reently in egHWF his mehnism equips the system with type lss mehnism fVWF sn the ontext of proof ssistnt this feture notly enles proof inferene y type infereneF sn the Coq systemD n other type lsses mehnism à l fVW hs een implemented yHVD independently from the nonil strutures mehnismD ut on top of frmework for dependent type progrmmingF st is this ltE ter mehnism whih is tully usully referred to s 9Coq type lsses9F sn their urrent stteD the SSReflect lirries only mke use of the nonil strutures mehnismF QR qoing k to our previous exmpleD we n provide the uni(tion lgoE rithm with hint to guess tht if zmodule struture is required on boolD then our intention is tht it has to be bool_zmoduleX Canonical Structure bool_zmodule.

efter this delrtionD the Check (false + true) ommnd does not rise n error messge ny more ut nswersX false + true : bool_zmoduleF he nonil struture delrtion indeed stores some equtions in dtse known to the uni(tion lgorithmF hese equtions will guide the lgorithm in se some holes remin in uni(tion prolemF yne eqution is stored per nmed (eld in the strutureF sn our exmpleD delring bool_zmodule s nonil instne stores the hintX [ carrier ? bool ] ⇒ ? = bool_zmodule plus n dditionl hint for the spec projetionD whih will revel useless6 F he error messge rised t our (rst ttempt to type false + true omplined tht false hs type bool nd ws expeted to hve type (carrier ?)F xow fter the nonil struture delrtionD the (rst hint in the list gives solution to this prolemF gnonil strutures not only enle the shring of nottionsD ut lso tht of proofsX on the gol Goal forall x y z : bool, x (+) y (+) z = x (+) z (+) y.

where (+) is nottion for the onrete xor opertion addbD the ommndX apply: zmaddAC.

solves the gol7 F o void spurious folding nd unfolding of de(nitionsD it is reommended prtie to use generi nottions s often s possile on onrete instneF rene the previous gol would est e expressed sX Goal forall x y z : bool, x \+ y \+ z = x \+ z \+ y.

his simple exmple re)ets the struture of more intrite modulr swithesX he(nition of generi strt strutures like zmoduleF his n involve more sutle urry(tion nd dependent types to hieve full modulrityD inheritne nd shring @see for instne qqwHWAF hevelopment of generi theory for eh strutureD onsisting of lemms like zmaddACF opultion of the generi struturesF his onsists in the de(nition of instnes of the struturesD like bool_zmoduleF hese instnes re most often delred nonilF hevelopment of spei( theories of the instnesF hese lirries ene(t from the generi results @nd nottionsA estlished t the strt level thnks to the nonil struture hintsF Definition prod_eqMixin (T1 T2 : eqType) := EqMixin (@pair_eqP T1 T2). Canonical Structure prod_eqType (T1 T2 : eqType) := EqType (T1 * T2) prod_eqMixin.

his nonil struture de(nition stores the following eqution in the dtseX [ Equality.sort ? 1 prod @Equality.sort ? 2 A @Equality.sort ? 3 A] ⇒ ? 1 = prod_eqType ? 2 ? 3 where prod is the onstnt hidden y the in(x * nottion of type produtF e give here n exmple where this hint is usedD nd triggers further nonil struture infereneF ememer from setion RFQ tht the foolen omprison opertion of n eqType is nmed eq_opD nd supports the in(x nottion ==F efter hving solved exerise SFPFID try the following ommndX Check (true, 3) == (true && true, 1 + 2).

sf the nonil strutures of eqType hve een orretly de(ned on bool nd nat @they re in ft introdued respetively in lirries ssrbool nd ssrnatAD then the system should nswer boolF o type this expressionD the system hs to unfold the nottionD hene to type the termX eq_op _ (true, 3) (true && true, 1 + 2) where eq_op hs typeX eq_op : forall T : eqType, rel (Equality.sort T) s shown y the ommnd Check eq_op in Set Printing Coercions modeF ine the two lst rguments of the term to e typed re of type (bool * nat)F he system should hene unifyX (Equality.sort ?) with (prod bool nat) here is no wy of solving this uni(tion prolem without extr informtion oming from nonil struturesF gnonil struture inferene is triggered y hed onstntsX in this uni(tion prolemD the respetive hed symols Equality.sort nd prod of oth sides mth the hed symols of produt of eqType hintF his hint sys tht we n otin ? s (prod_eqType ?2 ?3) if we n solve the two new prolemsX unify bool with (Equality.sort ?2) nd nat with (Equality.sort ?3) end this should very muh look like the solution of exerise SFPFIF o rft nonil onstrutionsD lwys rememer tht their inferene is triggered y hed onstnts nd projetionsF nfortuntelyD the vernulr support for nonil strutures is rther elementryD in ft limited to theX Print Canonical Projections.

ommndD whih lists the hints present in the dtseF 6 Finite objects in SSReflect 6.1 Finite types 6.1.1 Finite types constructions equenes re used to de(ne types with (nite numer of inhitntsF e finType is not uilt out of distint onstrutors ut insted it onsists of sequene enumerting its elementsF his proves to e more e0ient for omiE ntori opertionsF e type (T : finType) hene emeds type with oolen equlity nd dupliteEfree sequene ontining ll the elements of the rrier typeF vet us equip the bool type with @nonilA struture of finType10 X Lemma bool_enumP : Finite. where the sequene [:: true; false] enumertes the inhitnts of the type @here ll the elements of the underlying eqTypeAD nd Finite.axiom is the spei(tionX Finite.axiom (T : eqType)(e : seq e) := forall x, count (@pred1 T x) e = 1.

whih ensures tht the sequene ontins extly one ourrene of eh elE ement of the underlying eqTypeF he sequene enumerting the elements of (T : finType) is (enum T)F fy onstrution it stis(es the Finite.axiom spei(tionX Lemma enumP : forall T : finType, Finite.axiom (Finite.enum T). Lemma tuto_negb_exists : forall (T : finType)(P : pred T), ~~(existsb x, P x) = (forallb x, ~~P x).

Exercise 6.1.10 rove tht on ny nonEempty suset desried y predite (P : pred T)D where (T : finType)D funtion F : T -> nat hs mxiE mum nd minimumF rintX the fintype lirry de(nes pick hoie opertorD whih is legl on type with (nite numer of inhitntsF rene [pick x | P] is Some xD for n x suh tht P holdsD or None if there is no suh xF his opertor is spei(ed y pickP spei(tion lemmF elsoD the ssrnat lirry de(nes the minimum ex_minn @respF mximum ex_maxnA of the vlues stisfying nonEempty @repsF ounded non emptyA predite p : pred natF se the Search ommnd to investigte the theory developed on these opertionsF 6.1.4 Example: a depth rst search algorithm sn this setionD we illustrte the formliztion of n lgorithmD its spei(tion nd the forml proof of its orretness on the se of depth (rst serh lE gorithm in grph13 F his ommented proof lso illustrtes the feture of the SSReflect lngugeD nd in prtiulr of the view mehnismD on n exmple of formliztion y oolen re)etionF e onsider grph given y the finType of its vertiesD nd its neighor funtionX Variables (T : finType) (e : T -> seq T). sn this grphD there is n edge etween two verties x nd y if nd only if y is in the imge of x y the neighor funtion eF rene the djeny reltion is de(ned yX Definition grel := [rel x y | y \in e x].

using the rket nottion for oolen reltionsF he depth rst search algorithm omputes ll the verties of grph whih re rehle from given initil vertex y pth in the grphF st proeeds y visiting reursively ll the neighors of the initil vertexD then the neighors of these neighorsD etF ine the underlying grph my feture ylesD it is neessry to mrk the verties visited y the lgorithm to void extrneous reursive lls nd in(nite loopsF gonsider the funtionX is violted y this ontextF e would hene like to reple the urrent gol y the surd oolen sttement tht ould e derived under suh ssumptionF e ommon nd onvenient wy of performing this step of oolen ontrdition is the followingX uppose tht you know tht oolen sttement B is provleD to reple the urrent gol y ~~BD just use the ttiX case/idPn: PB where f is proof of (is_true B)F sn our proofD this tti isX case/idPn: (max_card (predU1 y (mem a))).

xote tht (mem a) is the stndrd wy to trnsform sequene into prediteD whih is the hrteristi funtion of the set of elements in the sequeneF Exercise 6.1.12 yserve the e'et of the previous tti on the golF se the vernulr ommndX Show Proof.

to disply the urrent stte of the proof termF vook for the ourrene of idPnF hih funtion is this ourrene n rgument ofc row hs this funtion een inserted @see qwD setion VFPAc ry to deompose the lst tti into more elementry stepsD without using the utomti insertion of view hintsF he sugol is then losed y the following ttiX by rewrite -ltnNge cardU1 (negPf Hy) addSn addnC.

xote the by losing tti whih ensures this sugol is killed y this sriptF Exercise 6.1.13 se the ommndX Check cardU1.

ht is the type of eh sutermc hy is this sttement wellEtypedc rintX vook t the result of the ommndX Set Printing Coercions. Check cardU1. Unset Printing Coercions. Exercise 6.1.14 ht is the type of negPfc ht is the type of (negPf Hy)c hy is this lst sttement well typed @sme hint s exerise TFIFIQAc por the indutive seD the proof goes y se nlysis on x eing n element of aX case Hx: (x \in a). he ove nottion hides the generi onstrution ptterns whih utoE mtes the de(nition of subType instneF Exercise 6.2.1 he(ne the Record type tuto_tuple_of: nat -> Type -> Type suh tht (tuto_tuple_of n T) if the type of sequenes on type T of (xed length nF ememer tht we wnt oolen spei(tionD nd tht the type nat hs nonil struture of eqTypeF grft this de(nition so tht it lso delres oerion from tuto_tuple_of to seq @see exmple in setion SFIAF xow de(ne nonil struture of subType on the type tuple_ofF rove tht [::] n e equipped with nonil struture of tupleF rove tht cons is n opertion whih uilds tuple from tuple @nd hed elementAF rove thtX

Lemma tuto_cat_tupleP : forall T n1 n2 (t1 : n1.-tuple T) (t2 : n2.-tuple T), size (t1 ++ t2) == n1 + n2.

where (n.-tuple T) is nottion for tuples of elements in t of length nF he(ne nonil onstrution of tuple for the tention of two tuplesF rove tht similrly the sequene opertionsD dropD takeD rot @see exerise RFPFIA nonilly preserve the tuple struture of of their rgumentsF gnonil instnes of the subType struture ene(t from generi opertors nd lemms suh s the injetion of n element of the sigm type myType into the igger type TX RR n°7392 he seond uthor wishes to thnk fenjmin erner for suggesting some of the exerises proposed in this tutorilF e lso thnk vurene ideuD vuE rent héry nd inrio ssi for proof reding nd ommentsF e re speilly grteful to prnçois qrillotD fs pitters nd the nonymous referees for nuE merous omments whih hve signi (

  Lemma subnK : forall m n, n <= m -> m -n + n = m. might strt with move=> m n lenm.

  elim: n m lenm => [m |n IHn m lt_n_m]. whih reks down the proof into two sugolsD m -0 + 0 = m given m : natD nd m -S n + S n = m given m n : natD lt_n_m : S n <= mD nd IHn : forall m, n <= m -> m -n + n = m. en exmple of this strong reursion priniple eing generted on the )y is proposed in setion QFSF he 9:9 nd =>9 ttils n e explined very simply if one views the gol s stk of vriles nd ssumptions piled on onlusionX tactic : a b c pushes the ontext onstnts aD bD c s gol vriles before performing tacticF tactic => a b c pops the top three gol vriles s ontext onstnts aD bD cD after tactic hs een performedF hese pushes nd pops do not need to lne out s in the exmples oveD so move: m lenm => p.

  list of ttisD possily hined y semiEolumnsD tht follows by keyword is onsidered s prenthesized lok pplied to the urrent golF rene for exmple if the ttiX by

  lists ll the ville results on the omprison < on nturl numersF ht is the de(nition of the SSReflect leq prediteD denoted <= c ht is the de(nition of < c rove the following sttementsX Lemma tuto_subnn : forall n : nat, n -n = 0. Lemma tuto_subn_gt0 : forall m n, (0 < n -m) = (m < n). Lemma tuto_subnKC : forall m n : nat, m <= n -> m + (n -m) = n. Lemma tuto_subn_subA : forall m n p, p <= n -> m -(n -p) = m + p -n.

  Lemma find_ex_minn : forall P : nat -> bool, exists n, P n -> {m | P m & forall n, P n -> n >= m}. he ommndX have: forall n, P n -> n >= 0. leds to two sugolsD the (rst remining to e proved eingX forall n, P n -> n >= 0 nd the seondX (forall n, P n -> n >= 0) -> exists n, Pn -> {m | P m & forall n, P n -> n >= m}. sn this exmple howeverD sine the lemm is trivil for CoqD the preferred ommnd would eX have: forall n, P n -> n >= 0 by done.

  on gol GD it retes two sugolsD respetively term -> G nd ( term -> G)-> GF fut the wlog tti lso o'ers the possiility to generlize list of onstnts on top of the (rst term -> G sugolF rere is n exmple showing the eginning of the proof tht quotient nd reminder of nturl numer iuliden division re uniqueF Lemma quo_rem_unicity: forall d q1 q2 r1 r2 : nat, q1 * d + r1 = q2 * d + r2 -> r1 < d -> r2 < d -> (q1, r1) = ( q2, r2).

  Lemma edivnP : forall m d, edivn_spec m d (edivn m d). Proof. rewrite /edivn => m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m). elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn. rewrite subn_if_gt; case: (ltnP m d) => [// | le_dm]. RR n°7392rewrite -{1}(subnK le_dm) -addSn addnA -mulSnr; apply: IHn. apply: leq_trans le_mn; exact: leq_subr.

  pplies to oth rnhesD n e pled ritrrily mong introdution itemsD fter the introdution rrow =>F sts role here is to lose the (rst sugol generted y the seEsplitF his //= swith is tully omintion of //D whih loses ll the sugols tht n e trivilly losed nd /= whih simpli(es ll sugols @generted y[|d] se split in this spei( exE mpleAD like the simpl tti in CoqF o //= simpli(es ll sugols nd solves the trivil onesF hen in the only remining sugolD i.e. the seond oneD we reple the (rst ourrene of m with 0 * d.+1 + mD using rewrite -{1}[m]/(0 * d.+1 + m) his tti should e red s reple the (rst @{1}A ourrene of the pttern m @[m]A y the term (0 * d.+1 + m)F he pttern is here given s full term m ut it ould lso e term with holes like [_ * (x + _)]F his omintion of ourrene nd pttern seletion is lso ville for the re rewrite ttiF sn this seD the tti sueeds euse 0 * d.+1 + m is onvertile to mF he reson why we reple m with the more omplited 0* d.+1 + m will eome ler elowF fefore the seond line of the proofD the gol is edivn_spec (0 * d.+1 + m) d.+1 (edivn_rec d m 0) e now need proof y strong indution rther thn simple indutionX insted of using nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P n.+1) -> forall n : nat, P n we would like to invoke property resemling the generi strong indution prinipleX forall P : nat -> Prop, P 0 -> (forall n, (forall m, m <= n -> P m) -> P n.+1) -> forall n, P n hepending on the situtionD the strong indution priniple tht is required my vry slightlyD so there is no strong indution priniple tht suits every sitution @even in the spei( se of nturlsAF sn SSReflect this issue is ddressed y the ese to de(ne on the )y non struturl dEho indution shemesF his is performed y omining the elim tti with the generliztion ptterns nd the ourrene seletionF sn our seD in the seond line of the proofD (leqnn m) pushes the hypothesis (m <= m) on top of the proof stkD immeditely to the left of (leqnn m) 0 generlizes 0 in n ritrry nturl nF oD in order to prove wht we wntD we (rst prove more generl propertyF his ws the purpose of the mysterious rewrite in the (rst line of the proofF hen {-2}m generlizes every ourrene of m in the gol exept for the seond ourreneD whih is intended to orrespond to the upper ound n in the generi strong indution priniple oveF pinlly elim: m strts n indution on the upper ound mD whih mounts to the strong indution tht we neededF his indution step genertes two sugolsF hnks to [|n IHn] we introdue n upper ound nd the orresponding indution hypothesis in the seond sugolF xote tht these rkets hve di'erent e'et from the ones used in the (rst line of the proofF here is no miguityX rkets fter se split or n indution re used for prllel introdution while rkets fter other ttis whihD like move or rewriteD do not generte new sugols re sing rketsF Exercise 3.5.2 ht is the e'et of eh element in [|m] q //= c pinllyD rewrite ltnS rewrites strit inequlity < into nonEstrit inequlity <= thnks to the lemm ltnSF et the end of the third line of the proofD the gol is edivn_spec (q * d.+1 + m.+1) d.+1 match m.+1 -d with | 0 => (q, m.+1) | m'.+1 => edivn_rec d m' q.+1 end hnks to the lemm subn_if_gt @nd thnks to inequlity eing de(ned through sutrtion in SSReflectD see exerise QFPFQA we rewrite the match -with syntx into the Coq if-then-else syntxF he next proof step is case: (ltnP m d) whih gin performs se split etween (m < d) nd (d <= m)F Exercise 3.5.3 ht is the e'et of [// | le_dm]c gn you (nd n lternE tiveD )tter introdution pttern hving the sme e'etc Exercise 3.5.4 sn the previous sriptD reple case: (ltnP m d) y case: ltnPF ht hppensc ht is the sttement of ltnPc ht is the de(nition of ltn_xor_geqc yn the model of ltn_xor_geqD de(ne n indutive spei(tion tuto_compare_nat whih performs threeEse split ording to the order of two nturl numersF rove thtX Lemma tuto_ltngtP : forall m n, compare_nat m n (m < n) (n < m) (m == n). et the end of the fourth line of the proofD the gol is edivn_spec (q * d.+1 + m.+1) d.+1 (edivn_rec d (m -d) q.+1) he tti rewrite -{1}(subnK le_dm) rewritesD from right to leftD only the (rst ourrene @euse of the {1} speiE (tionA of the (rst pttern tht mthes the equlity of lemm subnK le_dmF hen rewrite -addSn (nds in the gol the (rst pttern tht mthes the equlity of lemm addSn nd rewrites in the gol ll ourrenes of this pttern using the equlity from right to left @hene the minus symolAF Exercise 3.5.5 ht does the rest of the sript doc 4 Small scale reection, rst examples 4.1 The two sides of deduction sn the glulus of sndutive gonstrutions grVVD wWQD there is n ovious distintion etween logil propositions nd foolen vluesF yn the one hndD logil propositions re ojets of sort Prop whih is the rrier of intuitionisti resoningF vogil onnetives in Prop re typesD whih give preise informtion on the struture of their proofsY this informtion is utomtilly exploited y Coq ttisF por exmpleD Coq knows tht proof of A \/ B is either proof of A or proof of BF he ttis left nd right hnge the gol A \/ B to A nd BD respetivelyY dullyD the tti case redues the gol A \/ B => G to two sugols A => G nd B => GF yn the other hndD bool is n indutive datatype with two onstrutors true nd falseF vogil onnetives on bool re computable functionsD de(ned y their truth tlesD using se nlysisX Definition (b1 || b2) := if b1 then true else b2. roperties of suh foolen onnetives re estlished using se nlysisX the tti by case: b solves the gol b || ~~b = true RR n°7392 An introduction to small scale reection in Coq PP where ~~denotes the oolen negtionD y repling b (rst y true nd then y falseY in either seD the resulting sugol redues y omputtion to the trivil true = trueF woreoverD foolens n e injeted into propositions using the oerion mehnismX Coercion is_true (b : bool) := b = true.

  Goal forall a, P (a || a) -> True. move=> a; move/P2Q=> HQa.re equivlent to the former oneF he former sript shows how to interpret ft @lredy in the ontextAD thnks to the dishrge ttil 9:9 nd the ltterD how to interpret the top ssumption of golF xote tht the numer of wildrds to e inserted in order to (nd the orret pplition of the view lemm to the hypothesis hs this time een utomtilly inferredF he view mehnism is omptile with the case ttiX Variables P Q: bool -> Prop. Hypothesis Q2P : forall a b, Q (a || b) -> P a \/ P b. Goal forall a b, Q (a || b) -> True. move=> a b; case/Q2P=> [HPa | HPb]. retes two new sugols whose ontexts do not ontin HQ : Q (a || b) ny moreD ut respetively HPa : P a nd HPb : P bF his view tti performsX move=> a b HQ; case: {HQ}(Q2P _ _ HQ) => [HPa | HPb]. he term on the right of the / view swith is the view lemmaF eny term oering to produt type n e used s view lemmF he exmples we hve seen so fr expliitly provided the diretion of the trnsltion to e performedF sn ftD view lemms need not e orientedF he view mehnism is le to detet whih pplition is relevnt for the urrent golF por instneD the sriptX Variables P Q: bool -> Prop. Hypothesis PQequiv : forall a b, P (a || b) <-> Q a. Goal forall a b, P (a || b) -> True. move=> a b; move/PQequiv=> HQab. hs the sme ehvior s the (rst exmple oveF he view mehnism n utomtilly insert view hint to trnsform the doule implition into the expeted simple implitionF he lst sript is in ft equivlent toX Goal forall a b, P (a || b) -> True. move=> a b; move/(iffLR (PQequiv _ _)). whereX Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q.4.1.2 Specializing assumptions he speil se when the head symbol of the view lemm is wildrd is used to interpret n ssumption y specializing itF he view mehnism hene o'ers the possiility to pply higherEorder ssumption to some given rgumentsF por exmpleD the sriptX Goal forall z, (forall x y, x + y = z -> z = x) -> z it is often onvenient to interpret gol y hnging it into n equivlent propositionF he view mehnism of SSReflect hs speil syntx apply/ for omining simultneous gol interprettion opertions nd ookkeeping steps in single ttiF ith the hypotheses of setion RFIFID the following sriptD where ~~denotes the oolen negtionX Goal forall a, P ((~~a) || a). move=> a; apply/PQequiv. trnsforms the gol into Q (~~a)D nd is equivlent toX Goal forall a, P ((~~a) || a). move=> a; apply: (iffRL (PQequiv _ _)).where iffLR is the nlogous of iffRL for the onverse implitionF eny SSReflect term whose type oeres to doule implition n e used s view for gol interprettionF xote tht the gol interprettion view mehnism supports oth apply nd exact ttisF es expetedD gol interprettion view ommnd exact/term should solve the urrent gol or it filsF 4.1.4 The reflect predicate sn prtieD doule implition is not the most e0ient wy to relte oolens nd logil interprettionsF he following indutive predite reflect indeed proves fr more powerfulX Inductive reflect (P: Prop): bool -> Type := | Reflect_true: P => reflect P true | Reflect_false: ~P => reflect P false.he sttement (reflect P b) sserts tht (is_true b) nd P re logilly equivlent propositionsF por instneD the following lemmX Lemma andP: forall b1 b2 : bool, reflect (b1 /\ b2) (b1 && b2).

  reltes the oolen onjuntion && to the logil one /\F xote tht in andPD b1 nd b2 re two oolen vriles nd the proposition b1 /\ b2 hides two oerionsF he onjuntion of b1 nd b2 n then e viewed s b1 /\ b2 or s b1 && b2F ixpressing logil equivlenes through this fmily of indutive types mkes possile to tke dvntge from rewritable equations ssoited to se nlysis of Coq9s indutive typesF ine the stndrd equivlene predite is de(ned in Coq sX genertes the two sugols (b -> P) nd (P -> b)D relizing the expeted douE le implition se splitF he iffP lemm of ourse epts ny reflect sttement s n rgumentF yn gol of the formX Goal reflect (P1 /\ P2) (b1 && b2).the ttiX apply: (iffP andP). genertes the two sugols (b1 /\ b2 -> P1 /\ P2) nd (P1 /\ P2 -> b1 && b2)F 4.2 Exercises: sequences por tehnil resonsD the SSReflect lirry de(nes lone of the stndrd Coq list typeX Inductive seq (T : Type) : Type := Nil | Cons of T & seq T.

  Exercise 4.3.1 rove the following lemmsX Lemma tuto_eqxx : forall (T : eqType) (x : T), x == x. Lemma tuto_predU1l : forall (T : eqType) (x y : T) (b : bool), x = y -> (x == y) || b. Lemma tuto_predD1P : forall (T : eqType) (x y : T) (b : bool), reflect (x <> y /\ b) ((x != y) && b).

  struture n e thought of s kind of sigm type pking rrier type with signture zmodule_mixinF por instneD foolens n e equipped with suh struture @with xor s ddition nd identity s oppositeAX Definition bool_zmoduleMixin := ZmoduleMixin addbA addbC addFb addbb. Definition bool_zmodule := Zmodule bool_zmoduleMixin.

  Coq systemF hey re silently inserted during type infereneF por instne the following delrtion is vlidX Variable b : bool_zmodule. is epted y the systemD even if bool_zmodule is not typeF he ommnd Check b. nswers b : bool_zmoduleD s expetedF et if the glol option of oerion disply is set y the vernulr ommndX Set Printing Coercions. the nswer of Check eomes b : carrier bool_zmoduleF yne this struE ture de(nedD it is possile to de(ne hndy nottions nd develop theory for instnes of the strutureF por instneD let us de(ne nottion for the ddiE tion opertion of zmoduleF e (rst need de(nition to ess the opertion through the nested reordsF Definition zmadd (Z : zmodule) := add (spec Z).

  axiom [:: true; false]. Proof. by case. Qed. Definition bool_finMixin := FinMixin bool_enumP. Canonical Structure bool_finType := FinType bool bool_finMixin.

  Exercise 6.1.1 helre nonil struture of finType on the unit typeF xowD nonil onstrutions n trnsmit struture of (nite type to depenE dent type whose prmeters re themselves (nite typesF por instneD n option type on (nite type is itself (nite typeF he onstrution of the @nonilA struture goes this wyX IF gonstrut the enumertion of the inhitnts of the (nite typeX Definition option_enum (T : finType) := None :: map some (Finite.enum T).PF rove tht it stis(es the (nite type spei(tionX Lemma option_enumP : forall T : finType, Finite.axiom (option_enum T).QF gonstrut the (nite type mixinXDefinition option_finMixin (T : finType) := FinMixin option_enumP.RQ qunti(tion is (niteA nd re provly equivlent to their logil onstrutive ounterprtsF Exercise 6.1.9 tte nd prove the re)etion lemms tuto_existsP nd tuto_forallP relting the Prop qunti(ers with their oolen versionsF rove the lemmsX Lemma tuto_negb_forall : forall (T : finType)(P : pred T), ~~(forallb x, P x) = (existsb x, ~~P x).

  Exercise 6.1.15 rove the (rst se where Hx : (x \in a)= trueF rintX hon9t forget to use the Search vernulr tti @see qw for the syntxAF por instneX Search _ [disjoint _ & _]. lists ll the ville results on disjointF Qed. e sigm type with oolen spei(tions still does not llow to convert elements shring the sme (rst projetionF rene the reflexivity ttiD whih heks the onvertiility of the two sidesD filsF et proof irrelevne holds for type boolX for ny (b : bool)D ll the proofs of (b = b) re the smeF ine the seond projetion of n element of type odds should proof of @something onvertile toA (true = true)D two elements of type odd shring the sme vlue re provly equlF rene the bool_irrelevance lemm ppliesD reduing the gol to proving the trivil equlity (2 = 2)F o tke dvntge of this notle propertyD the SSReflect eqType lirry provides n speil interfe for subTypesF e subType is de(ned on top of sigm type y typillyX he(ning sigm like typeD under the form of n d ho Record type of the formX Record myType (T : Type) := {myval :> T ; _ : P (myval) } where(P : T -> bool) is onrete prediteF his de(nition genertes n elimintion sheme myTypeTF se this sheme to delre nonil struture of subType of T for mysubTypeX Canonical Structure myTypeSubType := [subType for myval by myType_rect].

  T ) . . . , let y m := b m in . . . in P n -> . . . -> Che goal to e proved ppers elow the doule lineY ove the line is the context of the sequentD set of delrtions of constants c i D dened constants d i D nd facts F k tht n e used to prove the gol @usullyD T i , T j : Type nd

	3.1 Sequents as stacks
	huring the ourse of proof Coq lwys presents the user with sequent whose
	generl form is
	c i : T i
	. . .
	d j := e j : T j
	. . .
	F k : P k
	. . .
	forall (x : P k : PropAF he vrious kinds of delrtions n ome in ny orderF he top
	prt of the ontext onsists of delrtions produed y the Section ommnds
	VariableD LetD nd HypothesisF his section context is never 'eted y the
	SSReflect ttisX they only operte on the upper prt " the proof contextF
	es in the (gure oveD the gol often deomposes into series of @universllyA
	qunti(ed variables (x : T )D lol denitions let y m := b m inD nd assump-
	tions P n ->D nd conclusion C @s in the ontextD vrilesD de(nitionsD nd
	ssumptions n pper in ny orderAF he onlusion is wht tully needs
	RR n°7392

  equivlent toX [by tactic 1 | by tactic 2 | ...]. he ltter form mkes deugging esierF sn the previous proof of the foo lemmD we should reple line 6 yX by rewrite muln0.rene the sript nnot e exeuted further if wht follows the by ttil does not lose this suEseF he by ttil is implemented using the userEde(nedD nd extensile done ttiF his done tti tries to solve the urrent gol y some trivil mens nd fils if it doesn9t sueedF sndeedD the tti expressionX by tactic . defult implementtion of the done ttiD s n Ltac ttiD is to e found in the ssreflect.v (leF st looks like 4

	is equivlent toX
	tactic ; done.
	gonverselyD the tti
	by [ ].
	is equivlent toX
	done.

he expressionX by [ tactic 1 | [ tactic 2 | ...]. is he X Ltac done := trivial; hnf; intros; solve [ do ![solve [trivial | apply: sym_equal; trivial] | discriminate | contradiction | split] | case not_locked_false_eq_true; assumption | match goal with H : ~_ |-_ => solve [case H; trivial] end ].

  F pinllyD the ttis last nd first omine with the rnhing syntx of LtacX if tti tactic 0 genertes n sugols on given golD then ttitactic 0 ; last k [tactic 1 |...|tactic m ] || tactic m+1 .

	IS
	tactic 1 ; first by tactic 2 .
	tries to solve the (rst sugol generted y tactic 1 using the tti tactic 2 D
	nd fils if it does not sueedsF
	SSReflect lso o'ers n extension of this filityD y supplying ttis to
	permute the sugols generted y ttiF he ttiX
	tactic ; last first.
	inverts the order of the sugols generted y tactic F st is equivlent toX
	tactic ; first last.
	wore generllyD the ttiX
	tactic ; last strict num first.
	2 D nd fils
	if it does not sueedsF sts nlogous

where strict num is nturl numer rgument hving vlue kD rottes the n sugols G 1 , . . . , G n generted y tactic y k positionsF he (rst sugol eomes G n+1-k nd the irulr order of sugols remins unhngedF gonverselyD the ttiX tactic ; first strict num last. rottes the n sugols G 1 , . . . , G n generted y tactic in order tht the (rst sugol eomes G k where k is nturl numerD pplies tactic 1 to the n -k + 1Eth golD FFFD tactic m to the n -k + 2 -mEth gol nd tactic m+1 to the othersF por instneD the sriptX Inductive test : nat -> Prop := C1 : forall n, test n | C2 : forall n, test n | C3 : forall n, test n | C4 : forall n, test n. Goal forall n, test n -> True. move=> n; case; last 2 [move=> k| move=> l]; idtac. retes gol with four sugolsD the (rst nd lst eing nat -> TrueD the seond nd third eing True with respetively k : nat nd l : nat in their ontextF

  ntly improved the originl version of this doumentF References egHW endre espertiD ilmer iiottiD gludio erdoti goenD nd inE rio ssiF rints in uni(tionF sn tefn ferghoferD ois xipkowD ghristin rnD nd wkrius enzelD editorsD Theorem Proving in Higher Order Logics, TPHOLs 2009 proceedingsD volume STUR of Lecture Notes in Computer ScienceD pges VR!WVF pringerD PHHWF fgHR ves fertot nd ierre gstérnF Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Construc-tionsF pringerEerlgD PHHRF grVV hF goqund nd qF ruetF he glulus of gonstrutionsF Information and ComputationD UT@PGQAD IWVVF qqwHW prnçois qrillotD qeorges qonthierD essi whouiD nd vurene ideuF kging mthemtil struturesF sn tefn ferghoferD ois xipkowD ghristin rnD nd wkrius enzelD editorsD Theorem Proving in Higher Order Logics, TPHOLs 2009 proceed-ingsD volume STUR of Lecture Notes in Computer ScienceD pges QPU! QRPF pringerD PHHWF qw qeorges qonthier nd essi whouiF A small scale reection extension for the Coq systemF sxse ehnil reportD http:// hal.inria.fr/inria-00258384F qonHV qeorges qonthierF porml proof E the pour golor heoremF Notices of the American Mathematical SocietyD SS@IIAXIQVP!IQWQD PHHVF qHW qeorges qonthier nd ve oux téphneF en sre)et utorilF ehnil eport EHQTUD sxseD PHHWF http://hal.inria.fr/ inria-00407778/en/F wWQ gF ulinEwohringF sndutive he(nitions in the ystem goq E ules nd ropertiesF sn wF fezem nd tFEpF qrooteD editorsD Proceedings of the conference Typed Lambda Calculi and ApplicationsD numer xiols yuryF pirstElss type lssesF sn ytE mne eït wohmedD gésr wuñozD nd o(ène hrD editorsD Theorem Proving in Higher Order Logics, TPHOLs 2008 proceedingsD volume SIUH of Lecture Notes in Computer ScienceD pges PUV!PWQF pringerD PHHVF heIH he goq hevelopment emF The Coq SystemF http://coq.inria. frD PHIHF fVW hilip dler nd tephen flottF row to mke dEho polymorE phism less d hoF sn 16'th Symposium on Principles of Programming LanguagesF egw ressD IWVWF

	An introduction to small scale reection in Coq	TH
	yHV	wtthieu ozeu nd
		TTR in vxgF pringer erlgD IWWQF elso vs reserh report WPERWD
		ix vyonF
	iWU	emokrne iiF yping lgorithm in type theory with inheritneF
		sn Principles of Programming Languages, POPL 1997 proceedingsD
		pges PWP!QHID IWWUF
	RR n°7392

RR n°7392

In versions ≤ 1.2 of SSReflect libraries, the library path was named paths. Hence replace the second line with: Require Import paths choice ...RR n°7392

Thus scripts that depend on bound variable names, e.g., via intros or with, are inherently fragile.

The name subnK means right cancellation rule for nat subtraction, see section 7.RR n°7392

The lemma not_locked_false_eq_true is needed to discriminate locked Boolean predicates. The do tactical is an iterator. See [GM] for more details.RR n°7392

For technical reasons, the structure is slightly dierent. More insight about the actual formalizations is given in [GGMR09] RR n°7392

This is why throughout the SSReflect library projections corresponding to specications are usually not named to avoid polluting the database with hints which will never be used.

For technical reasons, when working with Coq < v8.3, make sure to use the SSReflect rewrite and apply: tactics to trigger canonical structure inference.RR n°7392

Many variants of this notation are dened in the ssrbool library: with or without cast on the arguments, ...RR n°7392

In fact, the generic inE multirule should usually be extended each time a new membership predicate is dened. In the sequence library inE is for instance redened to include lemmas in_cons and mem_seq1.RR n°7392

In versions ≤ 1.2 of the SSReflect libraries, the last line should be Canonical Structure bool_finType:= FinType bool_finMixin RR n°7392

In versions ≤ 1.2 of the SSReflect libraries, the last line should be Canonical Structure option_finType:= FinType option_finMixin

This operator should not be confused with the above Finite.enum eld, which is a projection of the finType structure.RR n°7392

This formalization can be found in the SSReflect connect library.RR n°7392

In versions ≤ 1.2 of the SSReflect libraries, the last line should be Canonical Structure mySubType_eqType := EqType myType_eqMixin. RR n°7392

http://www.inria.fr ISSN 0249-6399

Acknowledgments

partially funded by the FORMATH project, nr. 243847, of the FET program within the 7th Framework program of the European Commission )exion à petite éhelle à l formlistion d9ojets (nis en théorie des types intuitionisteF Mots-clés : CoqD SSReflectD ré)exionD théorie des

PS

Definition iff (A B : Prop) := (A -> B) /\ (B -> A).

where /\ is the stndrd nottion for logil andX Inductive and (A B : Prop) : Prop := conj : A -> B -> and A B his mkes se nlysis very di'erent ording to the wy n equivlene property hs een de(nedF por instneD if we hve proved the lemmX Lemma andE: forall b1 b2, (b1 /\ b2) <-> (b1 && b2).

let us ompre the respetive ehviors of andE nd andP on golX Goal forall b1 b2, if (b1 && b2) then b1 else ~~(b1||b2).

ixpressing re)etion reltion through the reflect predite is hene very onvenient wy to del with lssil resoningD y se nlysisF sing the reflect predite moreover llows progrmming rih spei(tions inside its two onstrutorsD whih will e utomtilly tken into ount during destrution @see for instne exerises of setion RFQA F his formliztion style gives fr more e0ient spei(tions thn qunti(ed @douleA implitionsF e nming onvention in SSReflect is to post(x the nme of view lemms with PX orP reltes || nd \/D negP reltes ~~nd ~D etF hnges the gol a /\ b -> a into a && b -> a @see setion RFIFIAF he sme ttis n lso e used to perform the onverse opertionD hngE ing oolen onjuntion into logil oneF he view mehnism guesses the diretion of the trnsformtion to e used iFeFD the onstrutor of the reflect predite whih should e hosenF 4.1.5 Interpreting equivalences iquivlent oolen propositions re simply equal oolen termsF e speil onstrution helps the user to prove oolen equlities y onsidering them s logil doule implitions @etween their oered versionsAD while performing t the sme time logil opertions on oth sidesF he syntx of doule views isX apply/ term l / term r .

RR n°7392

An introduction to small scale reection in Coq PT he term term l is the view lemm pplied to the left hnd side of the equlityD term r is the one pplied to the right hnd sideF sn this ontextD the identity viewX Lemma idP : reflect b1 b1.

is usefulD for exmple the ttiX apply/idP/idP.

trnsforms the gol ~~(b1 || b2)= b3 into two sugolsD respetively ~~(b1 || b2)-> b3 nd b3 -> ~~(b1 || b2). he sme gol n e deomposed in severl wysD nd the user my hoose the most onvenient interprettionF por instneD the ttiX apply/norP/idP. pplied on the sme gol ~~(b1 || b2)= b3 genertes the sugols ~~b1 /\ ~~b2 -> b3 nd b3 -> ~~b1 /\ ~~b2F 4.1.6 Proving reflect equivalences etion RFIFR dvotes the use of the re)et predite to express logil equivE lene etween oolen predites nd their logil interprettionF o prove suh reflect equivlenesD we hd so fr no other hoie thn nive se nlysis on the vlue of the oolenF his is the proof method used for proving elementary reflect sttements like andPF roweverD when it omes to proving more omplexD composed sttementsD this remins vlid strtegyD ut very ine0ient oneF sn ftD it is never used in prtie for higher level equivlenesF he user of ourse expets to e le to prove suh n equivlene y the usul doule implitionF he swiss rmy knife to estlish reflect equivlenes is in ft the following trnsitivity resultX progrm funtion tuto_count whih omputes the numer of elements of sequene stisfying oolen prediteF rove thtX

Lemma tuto_count_predUI : forall a1 a2 s, count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.

where predU is the oolen predite union of its two rgumentsD nd predI is the oolen predite intersetion of its two rgumentsF rintX try to use the nat_congr ttiD n vt tti de(ned in the ssrnat lirryD to normlize rithmeti expressions nd perform ongrueneF vook for the de(nition of the filter funtionF rove thtX Lemma count_filter : forall a s, count a s = size (filter a s). Exercise 5.2.1 row would you de(ne nonil struture of eqType on type boolc on type natc ht is in eh se the eqution given s hint to the uni(tion lgorithmc xow dependent types my inherit some struture from their prmetersD when they re themselves equipped with some strutureF por instneD there is nonil wy of uilding foolen omprison of pirs of elements themselves omprle y foolen preditesF e sy tht the produt of two eqTypes hs nonil struture of eqTypeF sndeed the foolen testX Definition pair_eq (T1 T2 : eqType

is the expeted foolen omprisonF st is de(ned using the nottion for sted oolen reltionsX the nottion [rel x y : T | t] denotes the term (fun x y : T => t)D of type T -> T -> bool 8 F Exercise 5.2.2 rove the lemmX Lemma tuto_pair_eqP : forall T1 T2, Equality.axiom (pair_eq T1 T2).

xow we pose the following de(nitionsX QU 5.3 Predtypes: canonical structures for notations en importnt se where nonil strutures implement shred nottion is the in(x nottion for memershipF sn SSReflect lirriesD if P is oolen prediteD the sttement x stis(es P n e written pplitively s (P x) or using n expliit in(x onnetiveD s (x \in P)F sn the ltter seD P is lled olletive predite nd supports the nottionsX (x \in P) for x stis(es the olletive predite P (x \notin P) for x does not stisfy the olletive predite P e olletive predite is typilly memership predite for listsD (nite types or more generllyD ontinersF e given predtype T is expeted to support @t mostA single memership @olletiveA prediteD giving n unmiguous mening to the foolen expression (x \in A)D with (A : T)F hen there is not nturl wy of seeing given type s ontinerD it is not relevnt to equip it with predtype strutureF o equip type T with the two ove prenex nottionsD the user should delre nonil struture of predType on TF e re not desriing in detil the tehnil spet of the the predType struture de(nition hereF st is su0ient to understnd thtD just like n eqType struture undles type T with foolen reltion on TD whih is required to re)et the veiniz equlity on TD (predType T) strutures equips n other type with nonil foolen memership prediteF por instneD the prediteX mem_seq : forall T : eqType, seq T -> T -> bool tests the memership of n element of type (T : eqType) @see setion RFQA in ny sequene @see setion RFPA of elements of TF eny type (seq T)D with (T : eqType) is nonilly equipped with predType struture using this memership de(nitionF rene we n writeX Section SeqMem. Lemma tuto_mem_head : forall x s, x \in x :: s.

RR n°7392

An introduction to small scale reection in Coq QV xote tht while the re de(nition of memership does not require the sequene to e sed on type with foolen equlityD the entire SSReflect sequene lirry is gered towrds re)etionD in the sense of the three lemms proved in exerise SFQFIF st is sometimes desirle to hnge n in(x nottion (x \in P) into (P x)F por ny olletive prediteD this n e done using the generi rewrite multirule inEF e mulirule is Coq onstnt de(ned s list of rewrite lemmsF he ttiX rewrite inE. looks in the list inE for the (rst rewrite rule whih pplies to the urrent gol nd hene hnges the (rst ourrene of pttern (x \in P) into (P x) 9 F por more detils on mulirulesD plese refer to qwF Exercise 5.3.2 rove the following lemmsX Lemma tuto_mem_cat : forall x s1 s2, (x \in s1 ++ s2) = (x \in s1) || (x \in s2).

Lemma tuto_mem_behead: forall s, {subset behead s <= s}.

where the lst sttement stnds forX forall s x, x \in behead s -> x \in s rogrm y indution foolen test tuto_has: pred T -> seq T -> bool whih tests whether sequene fetures n element stisfying given foolen prediteF rove the following re)etion lemmX Lemma tuto_hasP : forall (a : pred T) s, reflect (exists2 x, x \in s & a x) (has a s).

where the stndrd Coq onstrutor exists2 spei(es witness for conjunction of preditesF rogrm y indution foolen test tuto_all: pred T -> seq T -> bool whih tests whether ll the elements of sequene stisfy given foolen prediteF rove the following re)etion lemmsX Lemma tuto_allP : forall (a : pred T) s, reflect (forall x, x \in s -> a x) (all a s).

Lemma tuto_allPn : forall (a : pred T) s, reflect (exists2 x, x \in s & ~~a x) (~~all a s). End SeqMem.

End OpsTheory. rintX oth these proofs should strt y the ttiX rewrite unlock.

to relese the sels proteting unwnted redutionsF his is imposed y the de(nition of subsetF ehnil detils out these sels n e found in qwD yet the reder n sfely skip this pointF rove the lemmsX Lemma tuto_subset_eqP : forall A B, reflect

6.1.3 boolean quantiers yn (nite typesD logil qunti(ers n e re)eted into oolen onesX indeedD universl sttement mounts to (nite onjuntion of testsD nd n existentil one mounts to oolen test on (nite numer of vluesF hen the oolen existentil onnetive (existsb x, A x) is de(ned y stting tht A is not emptyD in the sense of the pred0 prediteF he oolen universl onnetive (forallb x, A b) is de(ned y stting tht the omplement of e is emptyF hese oolen qunti(ers stisfy the rules of lssil logi @sine the domin of RR Fixpoint dfs (n : nat) (a : seq T) (x : T) {struct n} := if n is n'.+1 then if x \in a then a else foldl (dfs n') (x :: a) (e x) else a.

his funtion performs n steps of the depth (rst serhD strting from the vertex x with some lredy visited verties stored in the sequene aF yur gol is to prove the following spei(tionX Lemma dfs_pathP : forall x y, reflect (exists2 p, path grel x p & y = last x p) (y \in dfs #|T| [::] x).

his spei(tion ensures tht vertex y is rehle form the vertex x y pth in the grph if nd only if it is found in #|T| @the numer of verties in the grphA steps y the funtion dfsD strting from vertex x with n empty set of mrked vertiesF he ore of this proof is the invrint of the dfs funtionX Lemma dfsP : forall n x y (a : seq T), #|T| <= #|a| + n -> y \notin a -> reflect (dfs_path x y a) (y \in dfs n a x).

where the dfs_path predite is de(ned sX his tti introdues in eh sugol hypothesis Hya'D giving the respetive vlues true nd false to the oolen y \in a'F sn the (rst sugolD we know thtX (y \in foldl (dfs n) a' (e x)) = true euse of hypothesis Hya' nd of the lemm subset_dfsF he oolen y \in foldl (dfs n)a' (e x) n e rewritten to true using the ttiX rewrite (subsetP (subset_dfs n _ _) _ Hya').

xote tht the sme oerion is pplied s in exerise TFIFIRF Exercise 6.1.17 is the type whose inhitnts re even nturl numersF hey re implemented s pir whose (rst projetion is usully dttypeD lled the valueD nd the seond one proof tht the (rst element stisfy the de(nitionl prediteF igm types do not ehve s onveniently s desiredX let us prove tht 2 n e seen s n element of evens y two di'erent wysF he (rst one is strightforwrd nd the seond one mke n unneessry detourX Definition two_even1 : evens. Proof. by exists 2; exists 1. Defined.

Definition two_even2 : evens. Proof. by exists 2; rewrite -(addn0 2) addn0; exists 1. Defined.

Goal two_even1 = two_even2. reflexivity. Abort.

he error messge is due to the ft tht not ll the proofs of given theorem re equlF ry Print two_even1 nd Print two_even2 to ompre these two termsF ine we re ompring pirs of elements whose seond omponents re @non onvertileA proofsD there is no wy these two elements re onvertileF sn generlD there is not even ny reson why they should e provly equlF rowever the sitution is muh di'erent when the sigm type is de(ned y mens of oolen prediteF gonsider the de(nitionX @whih nswers the previous questionFFFA woreover the opertor Sub is generi onstrutor for elements of sutypeX (Sub x Px) where (x : T) nd Px is proof of (P x) onstruts the orreE sponding elements of the sutype of the elements of T stisfying property PF xote tht the predite P is guessed utomtilly y the onstrution if the return type is knownF Exercise 6.2.3 he(ne the element 2 of type (ordinal 3)F he(ne the type odds of odd integersD de(ne the orresponding subType odds_subType of natF he(ne the element of 3 : odds_subTypeF sf type T is equipped with oolen equlityD this equlity @or more preE isely its restritionA is lso vlid one for ny sigm type de(ned on TF en importnt role of the subType struture is to onvey in systemti wy struture of eqType 14 present on the lrger type T to ny sigm type de(ned SI on TF here is in ft systematic construction of eqType for sutypes de(ned on top of n eqTypeF pollowing the ove nottionsD if myType hs nonil struture of sutype on type T equipped with a canonical structure of eqTypeD then @nonilA struture of eqType n e delred for myType yX he(ning n eqMixin y the generi onstrution triggered y the following nottionX Definition myType_eqMixin := [eqMixin of myType by <:].

his nottion requires previous nonil struture of subType for myTypeF he(ning the @nonilA eqType struture 15 X Canonical Structure mySubType_eqType := EqType myType myType_eqMixin.

Exercise 6.2.4 he(ne nonil struture of eqType on odds @fF exerise TFPFQAF he(ne nonil struture of eqType on tupleF rove the lemmX Lemma tuto_map_tnth_enum : forall (t : n.-tuple T), map (tnth t) (enum 'I_n) = t.

nd its extensionlity orollryX Lemma tuto_eq_from_tnth : forall (t1 t2 : n.-tuple T), tnth t1 =1 tnth t2 -> t1 = t2.

End TuplesExercises.

Finite functions, nite sets

en importnt pplition of the tuple onstrutionD studied in the exerises of the previous setionD is the formliztion of funtions on (nite dominsF e funtion (f : aT -> rT)D where aT is type with (nite numer of inhitnts nd rT n ritrry typeD is ompletely determined y (nite ojetX the list of vlues respetively ssigned to the (nite sequene of elements of the dominF et de(ning suh funtion s re inhitnt of the rrow type (aT -> rT) is not enough to ene(t from this (nitenessF por instneD the glulus of sndutive gonstrutions eing essentilly non extensionlD we nnot use the ft thtX forall f1 f2 : aT -> rT, (forall x : aT, f1 x = f2 x) -> f1 = f2 even sine in the present seD testing tht (forall x : aT, f1 x = f2 x) only requires (nite numer of testsF his n prove speilly unomfortle for instne in omintori proofs or in quotient onstrutionsF he SSReflect finfun lirry implements de(nition of funtions with fintype domin nd n ritrry odominD s tuples of vluesX (f : finfun aT rT) where SP (aT : finType) is #|aT|.-tuple of vlues in rTF he elements of aT eing given s n @orderedA enumerting sequeneD the finfun lists their respetive vlues in the sme orderF xow these funtionsD oered to their funtionl typesD enjoy the equivlene etween intensionl nd extensionl equlityX Lemma ffunP : forall (aT : finType) rT (f1 f2 : {ffun aT rT}, f1 =1 f2 <-> f1 = f2.

en importnt speil se of (nite funtions is the oolen oneX they re hrE teristi funtions of susets of the se finTypeF ytherwise sidD they de(ne msk on the finType dominF his se is importnt enough to deserve the de(nition of speil sutypeX Inductive set_type (T : finType) := FinSet of {ffun pred T}. denoted y {set T} where T is required to hold nonil struture of finTypeF sn prtiulrD s for (nite funtionsD @veinizA intensionl nd extensionl equlE ities oinide for suh setsX Lemma tuto_minsetp : forall P A, minset P A -> P A.

Lemma tuto_minsetinf : forall P A B, minset P A -> P B -> B \subset A -> B = A.

where name is the nme of n open moduleF his ommnd returns the list of lemmsX

RR n°7392

An introduction to small scale reection in Coq ST whose conclusion ontins suterm mthing the optionl (rst pattern F ereverses the testD produing the list of lemms whose onlusion does not ontin ny suterm mthing the ptternY whose nme ontins the given stringsF epre(x reverses the testD proE duing the list of lemms whose nme does not ontin the stringF e string tht ontins symols or is followed y sope key D is interpreted s the onstnt whose nottion involves tht string @eFgFD + for addnAD if this is unmiguousY otherwise the dignosti inludes the output of the Locate stndrd vernulr ommndF whose sttementD inluding ssumptions nd types ontins suterm mthing the next ptternsF sf pttern is pre(xed y -D the test is reversedY ontined in the given list of modulesD exept the ones in the given modules pre(xed y -F xote thtX tterns with holes should e surrounded y prenthesesF erh lwys volunteers the expnsion of the nottionD voiding the need to exeute vote independentlyF woreoverD string frgment looks for ny nottion tht ontins frgment s sustringF sf the ssrbool lirry is importedD the ommndX Search "~~". Search (_ =1 _) "bij".

RR n°7392

An introduction to small scale reection in Coq SU lists ll the lemms whose onlusion fetures 9=19 nd whose nme ontins the string bijF he ommnd X

Search "bij" (_ =1 _).

lists ll the lemms whose sttementD inluding hypothesesD fetures 9=19 nd whose nme ontins the string bijF Exercise 7.0.3 se the Search ommnd to know the nme of the onstnt hidden ehind the * nottionF se the Print ommnd to see how this opertion is de(nedF ht is the onstnt denoted y ==>c row is it de(nedc ht re the lemms onluding with something of the form _ ==> truec ht is the nme of the lemm stting the ommuttivity of the && operE torc en other wy of guessing the nme of lemm is to infer itF tterns might indeed revel useless with the properties of opertors re stted under normlized form suh s (commutative andb)F he list of opertor properties used throughout SSReflect lirries n e found in the heder of the ssrfun lirry soure (leF vemms in the distriuted lirries respet the following nme poliyX Generalities wost of the time the nme of lemm n e red o' its sttementX lemm nmed fee_fie_foe will sy something out (fee .. ( fie ..(foe ..)..)..)D eFgF lemm size_cat in seq.vF e often use oneEletter su0x to resolve overloded nottionD eFgFD addnD addbD addr denote natD foolenD ring dditionD respetivelyF his poliy does not neessrily pply to onstnts tht should lwys e hidden ehind generi nottionD nd hndled y more generi theoryF pinllyD hndful of theorems hve historil nmeD eFgFD Cayley_Hamilton or factor_theoremF Structures and Records ih struture type strts with lower se letterD nd its onstrutor hs the sme nme ut with pitl (rst letterF ih instne of struture type hs nme formed with the nme of the rrier typeD followed y n undersore nd the one of the struture type like in seq_sub_subTypeD the struture of subType de(ned on seq_sub @see fintype.vAF xotle exeptions to this rule re nonil onstrutions tking ene(ts of modulr nme spesD like in ssralg.vF Suxes vemm whose onlusion is prediteD or n equlity for prediteX tht predite is su0x of the lemm nmeD like in addn_eq0 or rev_uniqF RR n°7392

An introduction to small scale reection in Coq SV vemms whose onlusion is stndrd property suh s \charD <|D etFX the property should e indited y su0x @like _charD _normalD etAD so the lemm nme should strt y desription of the rgument of the propertyD suh s its key propertyD or its hed onstntF hus we hve quotient_normalD not normal_quotientD etF his onvention does not pply to monotony rulesD for whih we either use the nme of the property with the su0x for the operE tor @eFgFD groupMAD or the nme of the opertor with the su0x for suset monotony @eFgFD mulgSAF