Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets José Grimm To cite this version: José Grimm. Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets. [Research Report] RR-6999, 2009, pp.209. ￿inria-00408143v3￿ HAL Id: inria-00408143 https://hal.inria.fr/inria-00408143v3 Submitted on 30 Mar 2010 (v3), last revised 4 Dec 2018 (v7) HAL is a multi-disciplinary open access L’archive ouverte pluridisciplinaire HAL, est archive for the deposit and dissemination of sci- destinée au dépôt et à la diffusion de documents entific research documents, whether they are pub- scientifiques de niveau recherche, publiés ou non, lished or not. The documents may come from émanant des établissements d’enseignement et de teaching and research institutions in France or recherche français ou étrangers, des laboratoires abroad, or from public or private research centers. publics ou privés. INSTITUTNATIONALDERECHERCHEENINFORMATIQUEETENAUTOMATIQUE Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One Theory of Sets JoséGrimm N° 6999 — version 3 initialversionJuly2009—revisedversionMarch2010 Algorithmics,Programming,SoftwareandArchitecture (cid:13) G N apport E + R F de recherche(cid:13) 9-- 9 (cid:13) 9 6 R-- R A/ RI N I N R S I 9 9 3 6 9- 4 2 0 N S S I ImplementationofBourbaki’sElementsofMathematicsinCoq: PartOne TheoryofSets ∗ JoséGrimm Domain:Algorithmics,Programming,SoftwareandArchitecture Équipe-ProjetApics Rapportderecherche n°6999—version3—initialversionJuly2009—revisedversion March2010—209pages Abstract: WebelievethatitispossibletoputthewholeworkofBourbakiintoacomputer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms);inafirststepwewanttoimplementallninechaptersofthebookAlgebra. But thisrequiresatheoryofsets(withaxiomofchoice,etc.)morepowerfulthanwhatisprovided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and commentsalldefinitionsandtheoremsoftheChapter“TheoryofSets”.Thecode(including almostallexercises)isavailableontheWeb,underhttp://www-sop.inria.fr/apics/gaia. Version one was released in July 2009, version 2 in December 2009, version 3 in March 2010.Therearesmalldifferences,markedinfootnotes. Key-words: Gaia,Coq,Bourbaki,FormalMathematics,Proofs,Sets WorkdoneincollaborationwithAlbanQuadrat,basedonpreviousworkofCarlosSimpson(CNRS,Univer- sityofNice-SophiaAntipolis) ∗ Email:[email protected] CentrederechercheINRIASophiaAntipolis–Méditerranée 2004,routedesLucioles,BP93,06902SophiaAntipolisCedex Téléphone:+33492387777—Télécopie:+33492387765 ImplémentationdesÉlémentsdemathématiquesdeBourbakien Coq, partie1 Théoriedesensembles Résumé:Nouspensonsqu’ilestpossibledemettredansunordinateurl’ensembledel’œuvre de Bourbaki. L’un des objectifs du projet Gaia concerne l’algèbre homologique (théorie et algorithmes); dans une première étape nous voulons implémenter les neuf chapitres du livre Algèbre. Au préalable, il faut implémenter la théorie des ensembles. Nous utilisons l’AssistantdePreuveCoq;leschoixfondamentauxetaxiomessontceuxproposéesparCar- losSimpson. CerapportlisteetcommentetouteslesdéfinitionsetthéorèmesduChapitre théoriedesensembles. Presquetouslesexercisesontétérésolus. Lecodeestdisponiblesur lesiteWebhttp://www-sop.inria.fr/apics/gaia. Mots-clés: Gaia,Coq,Bourbaki,mathématiquesformelles,preuves,ensembles Bourbaki:TheoryofsetsinCoqI(v3) 3 Chapter 1 Introduction 1.1 Objectives Our objective (it will be called the Bourbaki Project in what follows) is to show that it ispossibletoimplementtheworkofN.Bourbaki, “ÉlémentsdeMathématiques”[3], intoa computer, and we have chosen the Coq Proof Assistant, see [4, 1]. All references are given to the English version “Elements of Mathematics”[2], which is a translation of the French version (the only major difference is that Bourbaki uses an axiom for the ordered pair in theEnglishversionandatheoremintheFrenchone). Westartwiththefirstbook: theory ofsets. Itisdividedintofourchapters, thefirstonedescribesformalmathematics(logical connectors,quantifiers,axioms,theorems). ChaptersIIandIIIformthebasisofthetheory; they define sets, unions, intersections, functions, products, equivalences, orders, integers, cardinals,limits.Thelastchapterdescribesstructures. Anexampleofstructureisthenotionofrealvectorspace: itisdefinedonasetE, uses theset(cid:82)ofrealnumbersasauxiliaryset,hassomecharacterization(therearetwolawson E, a zero, and a action of (cid:82) over E), and has an axiom (the properties of the the laws, the action,thezero,etc.). Acompleteexampleofastructureistheorder;givenasetA,wehave as characterization s ∈P(A×A) and the axiom “s◦s =s and s∩s−1 =∆ ”. We shall see in A thesecondpartofthisreportthatanorderingsatisfiesthisaxiom,butitnotclearifthiskind of construction is adapted to more complicated structure (for instance a left module on a ring). Given two sets A and A(cid:48), with orderings s and s(cid:48), we can define σ(A,A(cid:48),s,s(cid:48)), the set ofincreasingfunctionsfrom Ato A(cid:48). Anelementofthissetiscalledaσ-morphism. Inour implementation, the“setoffunctions f suchthat...” doesnotexists; wemayconsiderthe set of graphs of functions (this is well-defined), but we can also take another position: we reallyneedσtobeasetifwetrytodonon-trivialsetoperationsonit,forinstanceifwewant to define a bijection between σ and σ(cid:48); these are non-obvious problems, dealt with by the theoryofcategories. Thereishoweveranotherpracticalproblem;Bourbakiveryoftensays: letE beanorderedset; thisisashort-handforapair(A,s). Considernowamonoid(A,+). Constructinganorderedmonoidistrivial: thecharacterizationistheproductofthecharac- terizations, andtheaxiomistheconjunctionoftheaxioms. Theorderedmonoidcouldbe (A,(s,+)). If f isamorphismfors,andu∈A,thenthemappingx(cid:55)→ f(x+u)isamorphism fors,providedthat+iscompatiblewiths. IfwewanttoconvertthisintoatheoreminCoq, theeasiestsolutionistodefineanobjectXequivalentto(A,(s,+)),awaytoextractX(cid:48)=(A,s) andX(cid:48)(cid:48)=(A,+)fromX,anoperationsonAobtainedfromXorX(cid:48),andchangethedefinition ofσ: itshoulddependonX(cid:48) ratherthanon Aand s. Thecompatibilityconditionisthena propertyofX,σ(X,Y)andσ(X(cid:48),Y)areessentiallythesameobjects,if f ∈σ(X,Y)wecancon- RR n°6999 4 JoséGrimm sider f(cid:48)=x (cid:55)→ f(x+u),andshow f(cid:48)∈σ(X,Y). Fromthiswecandeducethemappingfrom σ(X(cid:48),Y)intoσ(X(cid:48),Y)associatedto f (cid:55)→f(cid:48). 1.2 Background WestartedwiththeworkofCarlosSimpson1,whohasimplementedtheGabriel-Zisman localization of categories in a sequence of files: set.v, func.v, ord.v, comb.v, cat.v, and gz.v. Onlythefirstthreefilesinthislistareusefulforourproject. Thefileord.zcontainsalotof interestingmaterial,butifwewanttocloselyfollowBourbaki,itisbettertorestarteverything fromscratch. Thefilefunc.v containsalotofinterestingconstructionsandtheorems, that canbeusefulwhendealingwithcategories. Forinstance,itallowsustodefinemorphisms on the category of left modules over a ring. The previous discussion about structures and morphismexplainswhyonlyhalfofthisfileisused. Thisreportisdividedintwoparts.ThefirstpartdealswithimplementationofChapterII, “Theoryofsets”,andthesecondpartwithchapterIII,“Orderedsets,cardinals;integers”of[2] EachofthesixsectionsofBourbakigivesachapterinthisreport(weusethesametitlesasin Bourbaki)butwestartwiththedescriptionofthetwofilesset.vandfunc.vbyCarlosSimpson (itisasequenceofmodules). TheircontentcoversmostofSections1and2(“Collectivizing relations”and“Orderedpairs”). 1.3 Notations Choosingtractablenotationsisadifficulttask. Wewouldliketofollowthedefinitionsof Bourbakiascloselyaspossible. Forinstancehedefinestheunionofafamily(Xι)ι∈I(Xι∈G). ClassicFrenchtypographyusesitaliclower-caseletters,anduprightupper-caseletters,but the current math tradition is to use italics for both upper- and lower-case letters for vari- ables; constantslikepr andCarduseuprightfont. Thesetofintegersissometimesnoted 1 (cid:78); but Bourbaki uses only N. Some characters may have variants (for instance, the previ- ousformulacontainsaFrakturvariantoftheletterG).IntheXMLversionofthisdocument wedonotusetheUnicodecharacterU+1D50A(becausenotmostbrowsersdonothavethe glyph),butacharacterwithvariant,sothatthereislittledifferencebetweenG,G,G,G,(cid:71),G. InthisdocumentweuseonlyonevariantoftheGreekalphabet(Unicodeprovidesnormal, italic,bold,bold-italic,sans-serifandsans-serifbolditalic;asaconsequence,theXMLver- sionshowsgenerallyaslantedversionofGreekcharacters,wherethePdfdocumentusesan uprightfont). WecaneasilyreplacelowerGreeklettersbytheirLatinequivalents(thereislittlediffer- ence between (Xι)ι∈I and (Xi)i∈I). We can replace these unreadable old German letters by moresignificantones. WemustalsoreplaceIbysomethingelse,becausethisisareserved keywordinCoq(andinisreservedtoo). Intheoriginalversion,C.Simpsonreservedthelet- ters A,BandE. Thus,aphraselike: let AandBbetwosubsetsofasetE, andI=A×B,all fouridentifiersarereservedlettersinSimpson’sframework. Notethat,traditionally,French mathematiciansuseromanuprightuppercaselettersanditalicslowercaselettersforvari- ables; QuantitiesnamedR,B,X,Y,andZbySimpsonhavebeenrenamedtoRo,Bo,Xo,Yoand Zo.QuantityAhasbeenremoved(itwasaprefixversionof&).QuantityEhasbeenrenamed 1http://math.unice.fr/~carlos/themes/verif.html INRIA Bourbaki:TheoryofsetsinCoqI(v3) 5 Bset then Set: this is the type of a Bourbaki set. It will still be denoted by E here. In our framework,thereservedsingle-letteridentifiersareIJLOPQSVW. CoqreservestheletterIasaproofofTrue, theletterOastheinteger0andtheletterS forthefunctionn(cid:55)→n+1onintegers. Anorderedpairwithvaluesx and y isatermz that hastwoprojectionspr z=x andpr z=y. Theconstructoriscalledbpair2 inCoq,andthe 1 2 destructorsarecalledpr1andpr2. WeshallreservethelettersJfortheconstructorandP,Q forthedestructors,sothatJ(Pz)(Qz)=zforallpairsz(seesection2.6fordetails). Bourbakihasasectiontitled“definitionofafunctionbymeansofaterm”. Anexample wouldbe x (cid:55)→(x,x)(x ∈(cid:78)). ThiscorrespondstotheCoqexpressionfunx:nat=>(x,x). Ac- cordingtotheCoqdocumentation,theexpression“definestheabstractionofthevariablex, oftypenat,overtheterm(x,x).Itdenotesafunctionofthevariablexthatevaluatestotheex- pression(x,x)”.Bourbakisays“amappingofAintoBisafunction f whosesourceisequalto AandwhosetargetisequaltoB”. Thedistinctionbetweenthetermsfunctionandmapping issubtle: thereisasectioncalled“setsofmappingsofonesetintoanother”; itcouldhave been: “setsoffunctionswhosesourceisequaltosomegivensetandwhosetargetisequal tosomeothergivenset”. Itisinterestingtonotethattheterm‘function’isusedonlyonce intheexercisestoChapterIII,inacasewhere‘mapping’cannotbeusedbecauseBourbaki doesnotspecifythesetB. Inwhatfollows,weshallusetheterm‘function’indifferentlyforS,orthemappingn(cid:55)→ n+1,ortheabstractionn=>Sn.GivenasetA,wecanconsiderthegraphg ofthismapping whennisrestrictedtoA. ThisconstructionissoimportantthatwereservetheletterLforit. GivenasetB,ifourmappingsendsAtoB,wecanconsiderthe(formal)functionf associated tothemappingwithsourceAandtargetB. WeshalldenotethisbyBL.Thesetwoobjects f and g havetheimportantpropertythat, ifn isin A, thereisanm denotedby f(n)or g(n) suchthatm =n+1(wehavetheadditionalpropertythat f(n)isinB). Ashortnotationis requiredforthemappingfrom(g,n)(cid:55)→g(n),or(f,n)(cid:55)→ f(n). WeshallusethelettersVand Wrespectively. Inthisdocument,weshallusestandardnotations,forinstancepr andpr 1 2 forPandQ,whentheyexist,calligraphicletterslikeV orW forsomeobjectslikeVandW, and a slanted font like is_function for the general case. Note that J x y is a Coq expression meaningtheapplicationofJtobothargumentsxandy. There a possibility to change the Coq parser and pretty printer so that (x,y) is read as pair x y, and { x : A | P } is read as the set of all x in A satisfying the predicate P. We shallnotusethisfeaturehere. Infact,thesearestandardnotationsinCoqfornotionsthat arerelatedbutnotexactlyidenticaltoours. 1.4 Descriptionofformalmathematics Termsandrelations. AmathematicaltheoryT isacollectionofwordsoverafinitealpha- bet formed of letters, logical signs and specific signs. Logical signs are (cid:228), τ, ∨, ¬ (the first twosignsarespecifictoBourbaki,theotherones,disjunctionandnegation,havetheirusual meaning).Specificsignsare=,∈,lettersarex,y,A,A(cid:48),A(cid:48)(cid:48),A(cid:48)(cid:48)(cid:48),and“atanyplaceinthetextit ispossibletointroducelettersotherthanthosewhichhaveappearedinpreviousarguments” [2,p. 15](anynumberofprimesignsisallowed;thisisnotincontradictionwiththefinite- ness of the alphabet). An assembly is a sequence of signs and links. Some assemblies are well-formedaccordingtosomegrammarrules.InBackus-Naurformtheyare: Term:=letter | τ (Relation) | SsignTerm ...Term letter 1 n 2Thisiscalled‘pair’inSimpsonandinversion1ofthisreport RR n°6999 6 JoséGrimm Relation:=¬Relation | ∨RelationRelation | RsignTerm ...Term 1 n Eachsignhastobefollowedbytheappropriatenumberofterms: (cid:228)takesnone,∈and=are followed by two signs, and one can extend Bourbaki to non-standard analysis [7] by intro- ducingaspecificsignst ofweight1qualifyingtherelationthatfollowstobestandard. Each signissubstantificas(cid:228)(ityieldsaterm)orrelationalas=(ityieldsarelation). We shall see below that τ (R) has to be interpreted as the expression where all occur- x rencesofxinRarereplacedby(cid:228)andlinkedtotheτ.Parenthesesareremoved.Thishasone advantage: thereisnox inτ (R),hencesubstitutionrulesbecometrivial. Forinstance,the x function x (cid:55)→x+y isconstructedbyusingτ, itisidenticaltothefunction z (cid:55)→z+y. Ifwe wanttoreplace y by z, weget x (cid:55)→x+z, butnot z (cid:55)→z+z. InCoq, thevariable y appears freeinx(cid:55)→x+y,andthevariablexappearsboundinthesameexpression.Renamingbound variablesiscalledα-conversion.Twoα-convertibletermsareconsideredequalinCoq. TheAppendixtoChapterIdescribesanalgorithmthatdecideswhetheranassemblyisa term,arelation,orisill-formed. Itworksintwostages. Inthefirststage,linksareignored. A classicalresultincomputerscienceisthatthereexistsaprogram(calledaparser)thatrec- ognizes all significant words (i.e., well-formed assemblies without links). We can associate anumbertoeachsign(forinstance262to’a’,111to’=’)andthustoeachassembly(forin- stance,262111262to’a=a’). ThiswillbecalledtheGödelnumberoftheassembly,see[5]for anexample.TwodistinctassemblieshavedistinctGödelnumbers.ThesetofGödelnumbers isarecursivelyenumerableset. GivenassembliesA ,A ,A ,etc,onecanformtheconcate- 1 2 3 nationA A A .... Ifeachassemblyisasignificantword,thereisauniquewaytorecoverA 1 2 3 i fromtheconcatenation,hencefromtheGödelnumberoftheconcatenation. Ademonstrativetext forBourbakiisasequenceofassemblies A A ...A , thatcontains 1 2 n (cid:48) (cid:48) (cid:48) (cid:48) aproof,whichisasubsequenceA A ...A ofrelations,whereeachA canbeshowntobe 1 2 m i truebyapplicationofabasicderivationrulethatusesonlyA(cid:48) for j <i.EachA(cid:48) isatheorem. j i (cid:48) (cid:48) (cid:48) Weshalluseavariant: aproof-pairisasequenceofrelationsA A ...A satisfyingthesame 1 2 m (cid:48) conditionsasabove,andatheoremisthelastrelationA inaproof-pair. Ifourbasicrules m are simple enough, the property of a number g to be the Gödel number of a proof-pair is primitiverecursive. Fromthis,onecandeducetheexistenceofatruestatementthathasno proof(thisisGödel’sTheorem). Anassembly Acontaininglinksisanalyzedbyusingantecedents, whichareassemblies of the form τ (R) (where x is some variable) that are identical to A if x is substituted in R x and links are added. The algorithm for deciding that an assembly with links is a term or a relationisrathercomplicated. Bourbakigivesthreeexamplesofassemblieswithlinks; the antecedentofthefirstoneisτ (x∈y)(thereisasinglelink);theantecedentofthesecondone x isτ (x∈A(cid:48) =⇒ x∈A(cid:48)(cid:48))(therearetwolinks);thethirdoneistheemptyset,seepicturebelow. x One can replace these links by the De Bruijn indices, so that the empty set would become τ¬¬¬∈τ¬¬∈121. This has two drawbacks: the first one is that 121 could be understood asoneintegerorasequenceofthreeintegers,thesecondisthatthisnotationassumesthat integersarealreadydefined. Theremedytothefirstproblemwouldbetoinsertaseparator (forinstanceasquare)andaremedytothesecondwouldbetouseabase-onerepresentation ofintegers;theemptysetwouldbeτ¬¬¬∈τ¬¬∈(cid:228)−(cid:228)−−(cid:228)−. Thescopeofthesecondτ isthescopeofitsoperator,thus¬¬∈(cid:228)(cid:228). Thismeansthatthetwosquaresareinthescope of both τ, are are linked to the second and first τ respectively. The third square is in the scopeofthefirstτonly,henceislinkedtothefirstτ. FormalmathematicsinBourbakiisso complicatedthatthe(cid:228)symbolis,inreality,neverused. INRIA Bourbaki:TheoryofsetsinCoqI(v3) 7 Denoteby(B|x)Atheassemblyobtainedbyreplacingx,whereveritoccursinA,bytheas- semblyB.Bourbakihassomecriteriaofsubstitutions,CS1,CS2,etc,thatarerulesaboutsub- stitutions. ForinstanceCS3saysthatτx(A)andτx(cid:48)(A(cid:48))areidenticalifA(cid:48) is(x(cid:48)|x)Aprovided thatx(cid:48) doesnotappearinA(informally: since x doesnotappearinτ (A),thenameofthe x variablex isirrelevant). FormativecriteriaCF1,CF2,etc.,giverulesaboutwell-formedness ofassemblies. ForinstanceCF8saysthat(T|x)AisatermorarelationwheneverAisaterm orarelation,T isaterm,xisaletter. Abbreviationsareallowed,sothat∨¬canbereplacedby =⇒,and¬∈canbereplaced by(cid:54)∈. Abbreviationsmaytakearguments,forinstance∧ABisthesameas¬∨¬A¬B. Aterm mayappearmorethanonce,forinstance ⇐⇒ ABisthesameas∧ =⇒ AB =⇒ BA,andafter expansion¬∨¬∨¬AB¬∨¬BA. Thelogicalconnectors¬,∨and∧arewritten~,\/,and/\ inCoq(weshalluse&insteadof∧,sinceitiseasiertotype). NotethatinCoq,A→Bisthe typeofafunctionfromAtoBbutalsomeansA =⇒ B. Thereisnolimitonthenumberof abbreviations(Bourbakiinvented(cid:59)asavariantofø).Unicodeprovidesalotofsymbols,but fewofthemareavailableinLATEXorinWebbrowsers. Starting with Section 2, Bourbaki switches to infix notation. For instance, whenever A andBarerelationssois∨¬¬∨¬A¬BA,byvirtueofCF5andCF9. Usingabbreviations,this relationcanbewrittenas =⇒ ∧ABA.Theinfixversionis(AandB) =⇒ A.Inordertoremove ambiguities,parenthesesarerequired,butBourbakisays:“Sometimesweshallleaveoutthe brackets”[2,p. 24],intheexampleabovethreepairsofbracketsareleftout. Insomecases Bourbaki writes A∪B∪C. This can be interpreted as (A∪B)∪C or A∪(B∪C). These are twodistinctobjectsthathappentobeequal:formally,therelation(A∪B)∪C=A∪(B∪C)is true. SimilarlyA∨B∨Cisambiguous,butithappens,accordingtoC24,that(A∨B)∨Cand A∨(B∨C)areequivalent(formally:relatedby ⇐⇒).InCoq,weuseunion2asprefixnotation for∪, sowemustchosebetween∪(∪AB)C or∪A(∪BC). Functioncallsareleft-associative, and brackets are required where indicated. We use \/ as infix notation for ∨, parentheses maybeomitted,theoperatorisrightassociative. Theoremsandproofs. Eachrelationcanbetrueorfalse. TosaythatP isfalseisthesame as to say that ¬P is true. To say that P is either true or false is to say that P∨¬P is true. A relation is true by assumption or deduction. A relation can be both true and false, case where the current theory is called contradictory (and useless, since every property is then true).TheremayberelationsPforwhichitisimpossibletodeducethatPistrueanditisalso impossibletodeducethatPisfalse(Gödel’stheorem).Apropertycanbeindependentofthe assumptions. ThismeansthatitisimpossibletodeduceP or¬P; inotherwords,addingP or¬P doesnotmakethetheorycontradictory. Anexampleistheaxiomoffoundation(see below),orthecontinuumhypothesis(everyuncountablesetcontainsasubsetwhichhasthe powerofthecontinuum). Some relations are true by assumption; these are called axioms. Anaxiom scheme is a rulethatproducesaxioms.ThelistofaxiomsandschemesusedbyBourbakiaregivenatthe endofthedocument. AtruerelationiscalledaTheorem(orProposition,Lemma,Remark, etc). Aconjectureisarelationbelievedtobetrue,forwhichnoproofiscurrentlyfound. As saidabove,inBourbaki,atheoremisarelationwithaproof,whichconsistsofasequenceof truestatements,thetheoremisoneofthem,andeachstatementRinthesequenceiseither RR n°6999