Modelling algebraic structures and morphisms in ACL2

Noname manuscript No. (will be inserted by the editor) Modelling Algebraic Structures and Morphisms in ACL2 J´onathan Heras ·Francisco Jes´us Mart´ın–Mateos ·Vico Pascual Received: date / Accepted: date Abstract In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we provide a guideline to implement a set of tools that facilitates the formalisations related to algebraic structures — as a result, an algebraic hierarchy ranging from setoids to vector spaces has been developed. The resultant tools can be used to simplify the development of generic theories about algebraic structures. In particular, the benefits of using the tools presented in this paper, compared to a from-scratch approach, are especially relevant when working with complex mathematical structures; for example, the structures employed in Algebraic Topology. This work shows that ACL2 can be a suitable tool for formalising algebraic concepts coming, for instance, from computer algebra systems. Keywords Mathematical structures, ACL2, Algebraic hierarchy, Proof engineering, Computer Algebra systems, Formal verification. This works was partially supported by Ministerio de Educaci´on y Ciencia, project MTM2009-13842-C02-01, and by the European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath). J. Heras (corresponding author) and V. Pascual Department of Mathematics and Computer Science, University of La Rioja, Edificio Vives, Luis de Ulloa, s/n. 26004 Logro˜no, Spain. Tel.: (+34) 941299461 Fax: +34 941299460 E-mail: [email protected], [email protected] F.J. Mart´ın–Mateos Computational Logic Group, Dept. of Computer Science and Artificial Intelligence, University of Seville, E.T.S.I. Inform´atica, Avda. Reina Mercedes, s/n. 41012 Sevilla, Spain. E-mail: [email protected] 2 J´onathan Heras et al. 1 Introduction Computer Algebra Systems (CAS) are powerful tools used, almost on a daily basis, by researchers on different areas. The performance of these systems keeps improving thanks to the introduction of new algorithms and the use of more efficient structures. The correctness of these new algorithms and structures is usually provided by theoretical means; however, bugs can be introduced during their implementation — e.g. a bug in the computation of some determinants with big integers was found in Mathematica [22]. Interactive Theorem Provers (ITPs) have been broadly employed to increase the confidence in CAS using different approaches; some examples are: the formalisation of CAS algorithms [5,18,53], the creation of environments to develop certified programs for symbolic computation [55], the implementation of ITPs on top of CAS and viceversa [11,40], and the communication between CAS and ITPs to ensure the correctness of some computations [1,10,16,31]. An instrumental component in most CAS are algebraic structures since they are the basis for several constructions. Therefore, it makes sense to use ITPs to certify the correctness of the implementation of those structures. The implementation of algebraic structures in ITPs is a well-known problem; and most ITPs offer a set of tools to deal with it. In the literature, several implementations of algebraic structures have been produced for different systems, and with different aims — most of these implementations were developed in the form of algebraic hierarchies. Coq is probably the most prolific system in this sense. Up to the best of our knowledge, 4 different approaches have been considered in this system to formalise algebraic structures. An algebraic hierarchy that tries to imitate the hierarchy of the Axiom computer algebra system [38] was implemented in [56]. The formalisation of the Fundamental Theorem of Algebra, see [26], employed the hierarchy presented in [25]. The SSReflect hierarchy, introduced in [24], has played a key role in the formalisation of the Feit-Thompson theorem [27]. Another hierarchy was developed in [63] having as final goal the formalisation of practical exact real arithmetic. Two Ph.D. theses have been devoted, at least partially, to this topic. A hierarchy for the Nuprl system appeared in Jackson’s thesis [37], and was the basis for proving some results about abstract algebra — this hierarchy had as final aim the connection with the Weyl computer algebra system [66]. Bailey implemented in his Ph.D. thesis [7] an algebraic hierarchy that was used to formalise part of Galois theory in Lego. There are also different approaches in the family of HOL theorem provers. A basic theory of groups was developed in HOL using the hierarchy presented in [29]. As can be seen in [9], the Isabelle/HOL system provides a library to formalise abstract algebra which has been successfully used to prove, for instance, Sylow theorems. In addition, there is also a hierarchy for relation and Kleene algebras in Isabelle [6, 23], and a hierarchy that models Axiom’s hierarchy [8]. Modelling Algebraic Structures and Morphisms in ACL2 3 We can also find a classical set-theoretic treatment of algebra in Mizar. The different structures, like group, ring and field are defined in several papers by various authors [39]. A report about some formalisation issues faced during these developments can be seen in [60]. Abstract algebra has been also formalised in constructive set theory using the MetaPRL system [65]. These algebraic hierarchies are interesting on their own (they have been used to formalise an impressive number of results); but, most of them are not directly related to CAS. However, there are some hierarchies that have been applied to study CAS [8,37,56]. An interesting example is the use of different hierarchies to formalise several constructions coming from the Kenzo computer algebra system [21]. Kenzo is a Common Lisp system devoted to Algebraic Topology which was developed by Francis Sergeraert. The Kenzo system has obtained some results not confirmed nor refuted by neither theoretical or computational means [61], and also has been used to refute some computations obtained by theoretical means [57, 58]. This implies that increasing user’s trust in this system is a relevant issue. Several ITPs have been used to formalise different instrumental results implemented in Kenzo. The Basic Perturbation Lemma [59] was formalised in Isabelle/HOL (see [3]) using the algebraic hierarchy presented in [9]. In the same line, the Effective Homology of the Bicomplexes was formalised in Coq (see [20]) extending the algebraic hierarchy of [25]. These formalisations were related to algorithms and not to the real programs implemented in Kenzo. The problem of extracting programs from the Isabelle/HOL proofs was studied [4], but even there, the programs are generated in ML, far from Kenzo. The ACL2 theorem prover is oriented to prove properties of programs written in (a subset) of Common Lisp; and, it has been successfully employed to study some critical fragments of actual Kenzo code [2,35,36,50] — due to the restrictions of the ACL2 language, some well-known and safe transformations were required (e.g. loops were replaced by tail-recursive functions). The works presented in [2,35,36,50] did not concern algebraic structures, but ACL2 has also been used to formalise constructions (the Normalisation theorem and the Eilenberg-Zilberg theorem [59]) involving algebraic structures implemented in Kenzo, see [44,47]. In contrast to the works in Isabelle and Coq, the algebraic structures involved in the ACL2 formalisations were developed from scratch instead of using, as a basis, a previously developed algebraic hierarchy. The formalisations presented in [44, 47] show that it is possible to reason about algebraic concepts in ACL2; however, the first-order quantifier-free logic of ACL2 stands in the way of a widespread use of this ITP to work with algebraic structures. In this paper, we show how this weakness can be overcome thanks to two of ACL2’s great strengths: programmable extensibility and proof automation. In particular, we provide a guideline to implement a set of tools that makes working with algebraic structures in ACL2 easier — as a result, a hierarchy of algebraic structures ranging from setoids to vector spaces has been developed. Using these tools as a basis, we can easily develop generic theories that model statements like “Let Abe an Salgebraic structure, then . . .”. This 4 J´onathan Heras et al. can be applied, for instance, to define generic constructions (e.g. the definition of the direct product from two generic groups) — generic constructions are instrumental in CAS, since they simplify the creation of new objects from others that have been previously defined [62]. Once that ACL2’s weakness is overcome, the use of ACL2 by CAS developers is justified for two reasons. First, the learning curve in ACL2 is not as steep as in other ITPs since ACL2’s prover is semi-automatic, and its language (Common Lisp) is the same as in several CAS (e.g. Kenzo, Axiom [38], Maxima [52], Reduce [32] and Weyl [66]). In addition, since the language is the same, ACL2 formalisations are closer to actual CAS code than formalisations in other ITPs — this might require some code-transformations and proofs by successive refinements, as for instance applied in [50]. The rest of this paper is organized as follows. In the next section, we present a brief introduction to the ACL2 system and the tools employed in our development. Section 3 is devoted to present how algebraic structures can be modelled from scratch in ACL2 (this is the approach followed in [44,47]), and the difficulties that are associated with this process. To overcome those problems, we present a guideline to implement a set of tools for algebraic structures in Section 4. These tools are the basis to simplify the development of generic theories about algebraic structures, as explained in Section 5. In Section 6, the ideas presented in Sections 4 and 5 are extrapolated to the formalisation of a construction implemented in the Kenzo system: the cone of a chain complex morphism; additionally, this section shows a comparison of different approaches to tackle this formalisation. Finally, Section 7 concludes the paper. 2 A Brief Introduction to ACL2 ACL2 [41,43] is a programming language, a logic, and a theorem prover supporting reasoning in the logic. The ACL2 programming language is an extension of an applicative subset of Common Lisp. The ACL2 logic is a first-order logic with equality, used for specifying properties and reasoning about the functions defined in the programming language. All the variables in the formulas allowed by the ACL2 system are implicitly universally quantified. The syntax of its terms and formulas is that of Common Lisp, and it includes axioms for propositional logic, equality, and for a number of predefined Common Lisp functions and data types. Rules of inference of the logic include those for propositional calculus, equality and instantiation. One important rule of inference is the principle of induction, that allows proofs by well-founded induction on the ordinal ε0. The logic has a constructive definition of the ordinals up to ε0, in terms of lists and natural numbers. The system also includes the usual well-founded order relation defined on this set of ordinals. By the principle of definition, new function definitions are admitted as axioms only if there exists a measure and a well-founded relation with respect Modelling Algebraic Structures and Morphisms in ACL2 5 to which the arguments of each recursive call decrease, thus ensuring that the function terminates. In this way, new definitions do not introduce inconsistencies. Usually, the system can prove automatically termination properties using both a predefined ordinal measure and the built-in well-founded relation on ordinals. Nevertheless, if the termination proof is not trivial, the user has to explicitly provide a measure on the arguments and a well-founded relation with respect to which this measure decreases. In addition, new function definitions must be total on the language of terms, so when functions are naturally defined only working on a subset of terms, some behaviour must also be defined on arguments outside of that subset. An additional way to introduce new function symbols in the logic is by means of the encapsulate mechanism [42]. Instead of giving their definitional body, only certain properties are assumed about them; to ensure consistency, witness functions (which are functions local to an encapsulate block) having the same properties have to be exhibited. Inside an encapsulate, the properties stated need to be proved for the local witnesses, and outside, they work as assumed axioms. A derived rule of inference, called functional instantiation [41], provides a limited higher-order-like reasoning mechanism instantiating the function symbols of a previously proved theorem. This rule replaces function symbols with other functions, provided it can be proved that the new functions satisfy the constraints or the definitional axioms of the replaced functions (depending on whether they were introduced by an encapsulate or by the principle of definition, respectively). The ACL2 theorem prover mechanises the ACL2 logic, and is particularly successful obtaining mechanical proofs, mainly, based on simplification and induction. The role of the user in this mechanisation is important: usually a non-trivial result is not proved in a first attempt, and the user has to lead the prover to a successful proof providing a set of lemmas, inspired by the failed proof, that the prover uses mainly as rewriting rules. In this work, we extensively use macros [41], a mechanism for creating specialised notation, and for abbreviating commonly occurring expressions in ACL2. Macros are functions on s-expressions whose output is interpreted as an ACL2 command containing terms and formulas computed from the input. We will skip many details and some of the function definitions will be omitted. The interested reader can consult the complete source code at http: //www.unirioja.es/cu/joheras/ahomsia/. In addition, a detailed explanation of the implementation of the tools presented in this paper can be read in [34]. 3 Defining Algebraic Structures in ACL2 From Scratch In this section, we explain how algebraic structures can be modelled from scratch in ACL2, and the problems associated with this process. As a running example, we consider the definition of setoids [12]. 6 J´onathan Heras et al. Asetoid X= (X, ∼X) is a set Xtogether with an equivalence relation ∼X on it. Setoids are commonly used in the mechanised development of algebraic structures (see [7,9,25,29,56,63]) mainly for two reasons. From a mathematical point of view, we can form the quotient of a set by changing its equivalence relation — we will provide an example in Section 5. Moreover, the representation of a set in a computer needs the encoding of the equality of such a set (this was deeply studied in [45]), and setoids can be used with this aim. A setoid can be represented by means of two functions: the characteristic function of the underlying set (the invariant), and a binary function encoding the equivalence relation. ACL2 provides a way to define equivalence rules [28], but those equivalence rules must be total (i.e. they must be equivalence rules on the whole universe of ACL2 terms); so, we cannot use them in the case of setoids since the equivalence rules of setoids are restricted to the domain of a concrete set. Example 1 The setoid whose underlying set is the integers, and whose equivalence relation makes integers with same absolute value equivalent can be modelled as follows. We use the ACL2 integerp function as invariant (integerp is a recogniser for integer numbers that returns true if its argument is an integer, and nil otherwise), and the eq-abs function as equivalence relation. (defun eq-abs (a b) (equal (abs a) (abs b))) To prove that these two functions form a setoid, it is necessary to prove the theorems (events whose successful evaluation extends the ACL2 logic) ensuring that eq-abs is an equivalence relation on the set characterised by integerp. For instance, the reflexivity property is given by the following theorem. (defthm eq-abs-x-x (implies (integerp x) (eq-abs x x))) Example 1 illustrates how concrete setoids can be modelled in ACL2; however, this representation is not enough to deal with the scenarios that involve generic setoids (e.g. the proof of universal properties). In order to tackle this problem, we should use the encapsulate mechanism (see Section 2 or [42]). This tool can be used to define a generic setoid; namely, we can define two generic functions X-inv (the invariant function) and X-eq (the equivalence relation) assuming the properties of setoids. The definition of a generic setoid can be seen as an equational algebraic specification of this mathematical structure where the type information is missed. Using the functions introduced in the encapsulate to define the generic setoid (X-inv and X-eq), we could prove universal properties that, afterwards, could be instantiated for concrete setoids using the functional instantiation mechanism [41]. Example 2 Based on the encapsulate that defines the generic functions X-inv and X-eq satisfying the definitional axioms of setoids, we can prove the following general property about setoids: Modelling Algebraic Structures and Morphisms in ACL2 7 (defthm symmetry-transitive (implies (and (X-inv x) (X-inv y) (X-inv z) (X-eq y x) (X-eq y z)) (X-eq x z))) and, subsequently, instantiate it for the integers setoid defined in Example 1. The encapsulate mechanism is not only the basis to prove universal properties, but it also can be used to define generic constructions. Example 3 Given two setoids X= (X, ∼X) and Y= (Y, ∼Y), the Cartesian product of Xand Y, denoted by X × Y, is given by X × Y = (X×Y, ∼X×Y) where X×Yis the Cartesian product of sets, and (x1, y1)∼X×Y(x2, y2) if x1∼Xx2and y1∼Yy2. To model this generic construction in ACL2, we start by using the encapsulate mechanism to define two “generic setoids” whose components are (X-inv,X-eq) and (Y-inv,Y-eq) respectively. From these 4 functions, we can construct the two functions (invariant and equality) that encode the Cartesian product: (defun X-Y-inv (pair) (and (= (len pair) 2) (X-inv (first pair)) (Y-inv (second pair)))) (defun X-Y-eq (pair1 pair2) (and (X-eq (first pair1) (first pair2)) (Y-eq (second pair1) (second pair2)))) Finally, we need to prove the definitional axioms of setoids for the functions X-Y-inv and X-Y-eq. Once that this is done, the generic Cartesian product construction can be instantiated for any two concrete setoids. This example and Example 2 illustrate how the encapsulate mechanism can be used to simulate higher-order logic in ACL2. This from-scratch approach to define concrete and generic setoids, prove universal properties, and create generic constructions can be extrapolated to deal with any algebraic structure in ACL2. Nevertheless, there are several problems associated with this approach: P.1. The functions that are used to define an algebraic structure does not form an entity, but they are defined separately. P.2. The definitional axioms for the objects have to be stated manually and for each instance of an algebraic structure — this can be especially timeconsuming and error-prone when there are several definitional axioms or several instances. P.3. Related to the previous problems, algebraic structures share some properties and components (e.g Abelian groups are groups with an additional property), but this fact cannot be directly captured with the from-scratch representation of algebraic structures. 8 J´onathan Heras et al. P.4. The use of encapsulates to create generic instances of algebraic structures can be also a time-consuming and an error-prone task for the user when the structure is complex, or when several encapsulates have to be defined. P.5. The development of generic theories (e.g. the proof of generic properties, or the construction of generic objects from generic definitions) involves several repetitive steps that could be simplified. The next sections will be devoted to explain how these problems have been solved. 4 A Set of Tools to Model Algebraic Structures and Morphisms In this section, we provide a guideline to define a set of tools that fulfils three goals: the creation of entities gathering the components of an algebraic structure, the simplification of the statement of the definitional axioms of an algebraic structure, and the simplification of the definition of generic instances of an algebraic structure — these goals correspond to Problems P.1–P.4, Problem P.5 will be tackled in the next section. We present how this set of tools can be defined for an algebraic structure; and, subsequently, how the same ideas can be extrapolated to implement a hierarchy of algebraic structures. 4.1 Tools to Model an Algebraic Structure Let us present the creation of the three different tools for a given algebraic structure. As a running example, we retake the definition of setoids presented in Section 3. Gathering the components of an algebraic structure. Most ITPs use records (called class or record in Isabelle [30, 54], Class or Record in Coq [15], struct in Mizar [60] and so on) to pack the operations of algebraic structures. In ACL2, we use the same approach gathering the operations of a structure in a record defined by means of the defstructure macro [13]. Given a structure Swith operations op1, . . . , opn, a record called Swith slots op1,. . .,opn is defined. Since ACL2 is an untyped system, there is no type information attached to the field names of the record. A concrete Sinstance whose components are given by the functions f1, . . . , fnis created using the macro make-S (a macro automatically generated when the record is defined) having as arguments the names of the functions implementing f1, . . . , fn(those functions must have been previously introduced in ACL2) — since ACL2 is not a higher-order system, this is the only way of treating functions as data. Instances of a given structure will be stored in a constant for latter use (a constant in ACL2 is a symbol beginning and ending with the character *). This approach models more accurately an algebraic structure than having the functions separately (Problem P.1), and provides a name to the structure Modelling Algebraic Structures and Morphisms in ACL2 9 (we could gather the components of a structure in a list, but that approach would not assign a name to the structure). Example 4 In the case of setoids, we define a record called setoid with two fields (inv and eq) that will store respectively the names of the invariant function and the intended equivalence relation. (defstructure setoid inv eq) Using this representation, if we want to create the setoid from Example 1, we construct an instance of the setoid record, where the values of the inv and eq slots are respectively the names integerp and eq-abs. Moreover, this instance is assigned to a constant, called *Zabs*, for latter use in our development. (defconst *Zabs* (make-setoid :inv ’integerp :eq ’eq-abs)) Simplifying the statement of definitional axioms. In some ITPs (e.g. Coq or Isabelle), records not only pack the operations of the structure, but also include the axioms about such operations. On the contrary, in ITPs like Mizar, the axioms are external to the record. In ACL2, we follow the latter approach — the macro defstructure allows us to attach assertions to a record, but this is not possible if the slots of the record have a functional nature, as in our case. In order to facilitate the statement of the event that ensures the definitional axioms of an algebraic structure S(Problem P.2), we define a function called S-algebraic-structure, and a macro called check-S-p. The function S-algebraic-structure takes as argument an Sinstance, and produces a “textual” (quoted in Lisp terminology) conjunction of formulas with the definitional axioms of the Sstructure for the functions of the Sinstance. The macro check-S-p takes as argument a constant, *S*, storing an Sinstance; and, it internally invokes the function S-algebraic-structure generating a defthm event, called *S*-is-an-S, that checks whether the Sinstance stored in *S* satisfies the definitional axioms of an Sstructure. The check-S-p can be seen as a characteristic function for the type of Sstructures. Example 5 In our running example about setoids, we define a function called setoid-algebraic-structure that takes as argument a setoid instance and produces a conjunction of formulas stating that the eq component of the setoid instance is an equivalence relation on the set characterised by the inv component of the setoid instance — i.e. the definitional axioms of setoids. Additionally, we define the macro check-setoid-p, that can be used to certify that a constant storing a setoid instance is really a setoid. For instance, given the constant storing the setoid from Example 4 (*Zabs*), the macro invocation (check-setoid-p *Zabs*) 16 J´onathan Heras et al. Once the generic subset is defined, we construct a magma instance where N-inv is the invariant, M-eq is the equivalence relation, and M-binary-op is the binary operation; and store the result in the constant *N*. (defconst *N* (create-magma ’N-inv ’M-eq ’M-binary-op)) Finally, we use the macro check-magma-p to certify that *N* is a magma: (check-magma-p *N*). ACL2 finds the proof of the event generated by this macro call without any external help. 5.3 Definition of Homology Groups We consider now a more involved example: the definition of homology groups in the context of Homological Algebra — an introduction to this mathematical subject can be seen in [64]. Definition 1 Let f:G1→G2and g:G2→G3be Abelian group morphisms such that ∀x∈G1, gf(x)∼G30G3(where 0G3is the neutral element of G3); then, the homology group of (f, g), denoted by H(f,g), is the Abelian group H(f,g)= ker(g)/im(f). The condition ∀x∈G1, gf(x)∼G30G3, known as nilpotency condition, makes the above definition meaningful, since im(f)⊆ker(g). This definition involves several constructions of Universal Algebra such as subalgebras, morphisms and quotients [17]. Given f:G1→G2and g:G2→G3Abelian group morphisms such that ∀x∈G1, gf(x)∼G30G3; we can use our tools to define H(f,g)and prove that it is an Abelian group. First of all, we define three generic Abelian groups (*G1*,*G2* and *G3*) using the defgeneric-Abelian-group macro. (defgeneric-Abelian-group G1) (defgeneric-Abelian-group G2) (defgeneric-Abelian-group G3) The components of these generic Abelian groups are: G<i>-inv, the invariant function of the underlying setoid of the group, G<i>-eq, the equivalence relation of the group, G<i>-binary-op, the binary operation, G<i>-id-elem, the identity element, and G<i>-inverse, the inverse function, with <i>=1,2,3. Now, using the encapsulate principle, we define two generic Abelian group morphisms f:G1→G2and g:G2→G3such that the nilpotency condition is satisfied. (encapsulate ;Signatures (((f *) => *) ((g *) => *)) Modelling Algebraic Structures and Morphisms in ACL2 17 ;Generic Abelian Group Morphisms Definition (defconst *f* (make-Abelian-group-morphism :source *G1* :target *G2* :map ’f)) (defconst *g* (make-Abelian-group-morphism :source *G2* :target *G3* :map ’g)) ;Abelian Group Morphism Axioms (check-Abelian-group-morphism-p *f*) (check-Abelian-group-morphism-p *g*) ;Nilpotency condition (defthm nilpotency-condition (implies (G1-inv x) (G3-eq (g (f x)) (G3-id-elem)))) ) The above encapsulate must be read as follows. First of all, we provide the signatures of the functions fand g, the notation ((f *) => *) means that the function fhas an argument, that belongs to the universe of ACL2 terms, as input and returns another term as output — the encapsulate also requires witnesses for the functions fand g, but we do not include them here since they are not relevant. Subsequently, we define the constants *f* and *g* that store the two generic Abelian group morphisms. Afterwards, using the check-Abelian-group-morphism-p macro, we impose the axioms of Abelian group morphism to *f* and *g*. Finally, we impose the nilpotency condition. The macro defgeneric-Abelian-group-morphism cannot be used here since we do not only want to build generic Abelian group morphisms, but also impose the nilpotency condition. As in the case of the subalgebra criterion, we could define a defgeneric macro that constructs two Abelian group morphisms satisfying the nilpotency condition, and that is parameterised by three Abelian groups. Such a macro would reduce the above encapsulate to just one macro call. Once that we have defined the Abelian group morphisms fand g, we can introduce ker(g), im(f) and, subsequently, the quotient ker(g)/im(f). The set ker(g) = {x∈G2:g(x)∼G30G3}(the invariant of such a set is encoded in ACL2 by means of a function called ker-g-inv) is both a subset of the underlying set of G2, and it is closed with respect to the group operations of G2. These are the conditions of the subalgebra criterion for Abelian groups (cf. Subsection 5.2); therefore, we can instantiate such a result for our concrete case and define the Abelian group ker(g). (defconst *ker-g* (create-Abelian-group ’ker-g-inv ’G2-eq ’G2-binary-op ’G2-id-elem ’G2-inverse)) 18 J´onathan Heras et al. Now, we define im(f) = {x∈G2:∃y∈G1, f(y)∼G2x}as a subgroup of G2using the same idea presented for ker(g). The existential quantifier in the definition of the invariant function of im(f) is introduced using defun-sk — the method supported by ACL2 to provide first-order quantification via Skolem functions [48]. (defun-sk im-f-inv (x) (exists (y) (and (G2-inv x) (G1-inv y) (G2-eq (f y) x)))) Then, using im-f-inv and the operations of *G2*, we encode the Abelian group im(f) using an Abelian-group instance. Afterwards, we can tackle the definition of the homology group H(f,g)as the quotient ker(g)/im(f). Quotienting a structure of our hierarchy is achieved by changing the equivalence relation of the underlying setoid of the structure with another equivalence relation compatible with the operations of the structure. This result has been proved for each structure of our hierarchy following a similar process to the subalgebra criterion (cf. Subsection 5.2). In addition, we have proved that if im(f) is a subgroup of ker(g), then im(f) induces an equivalence relation on ker(g) given in ACL2 by the following definition. (defun im-f-eq (x y) (im-f-inv (G2-binary-op x (G2-inverse y)))) Therefore, H(f,g)is defined using ker-g-inv as invariant, im-f-eq as equivalence relation, G2-binary-op as binary operation, G2-id-elem as the identity element, and G2-inverse as the inverse operation. (defconst *homology-fg* (create-Abelian-group ’ker-g-inv ’im-f-eq ’G2-binary-op ’G2-id-elem ’G2-inverse)) The last step consists in certifying that *homology-fg* satisfies the definitional axioms of an Abelian group. (check-Abelian-group-p *homology-fg*) ACL2 does not find the proof of the event generated by the above macro call in the first attempt, and some auxiliary lemmas, suggested by the failed proof, are necessary. The way of facing that proof is the usual when trying to prove a result with ACL2: inspect the failed proof attempt and provide the necessary lemmas and hints, this is known in ACL2 as “the Method” [41]. Using this procedure, we have proved that *homology-fg* is an Abelian group. 5.4 A General Proof-Scheme for Generic Theories The three examples presented throughout this section follow a common proofscheme. Such a proof-scheme can be applied to several generic theories about Modelling Algebraic Structures and Morphisms in ACL2 19 algebraic structures. In particular, given the generic objects S1, . . . , Sn, and the generic operations op1, . . . , opmsatisfying the properties P1, . . . , Pk, we can prove in ACL2 that T= ( cop1,..., copt) (where cop1,..., coptare operations derived from the components of S1, . . . , Sn, and/or the operations op1, . . . , opm) satisfies the definitional axioms of a Tstructure as follows. S.1. Definition of the objects S1, . . . , Snusing defgeneric macros. S.2. Definition of the generic operations op1, . . . , opmsatisfying the properties P1, . . . , Pkusing the encapsulate mechanism. S.3. Definition of the functions cop1,..., coptfrom the operations of Steps S.1 and S.2. S.4. Construction of a Tinstance with operations cop1,..., copt. S.5. Proof that the instance satisfies the definitional axioms of a Tstructure using the macro check-T-p — this proof might require some user intervention. Some of these steps might be unnecessary depending on the concrete problem. For instance, Step S.2 is not required in the Cartesian product construction (cf. Subsection 5.1) since all the components of the Cartesian product are defined from the components of the generic setoid; and, Step S.3 is unnecessary in the subalgebra criterion (cf. Subsection 5.2) since all the components of the new magma were introduced previously. Once a generic theory is completed, it can be instantiated for concrete instances using the functional instantiation mechanism. As an example, the subalgebra criterion for Abelian groups (see Subsection 5.2) has been instantiated for ker(f) and im(g) in the definition of homology groups. 6 A Case Study: Formalising the Cone Construction In the previous sections, we have presented a set of tools to work with the algebraic structures and morphisms of the hierarchy depicted in Figure 1; in addition, we have shown how these tools can facilitate the development of generic theories. The same ideas can be applied to more complex structures, and it is in those cases when the biggest impact occurs. In this section, we study how the techniques previously presented can be extrapolated to an Algebraic Topology construction implemented in the Kenzo system: the cone of a chain complex morphism [51] — a representative example of Kenzo’s constructions. Chain complexes and chain complex morphisms, as many other structures implemented in Kenzo (like simplicial sets), are defined as indexed families of structures; hence, the first step in the formalisation of the cone construction is the representation of indexed families of structures in ACL2. We will finish this section with a comparison of different approaches to formalise the cone construction. 20 J´onathan Heras et al. 6.1 Indexed Families of Structures The structures used in Algebraic Topology, such as chain complexes or simplicial sets, are based on families indexed on a set, called the index set. The method that we have followed to represent these families is based on the approach presented in [46]. Roughly speaking, the representation of a graded structure indexed on a set is achieved thanks to the introduction of an additional parameter, that ranges the elements of the index set, in each operation of the structure. This method differs from the usual approach followed in other ITPs to represent indexed families of structures: a function that takes as input an index, and returns a structure as output (see [20]) — this approach is not feasible in the first-order setting of ACL2. Then, in order to deal with families of structures in ACL2, we have created a hierarchy of graded structures that mirrors the hierarchy presented in the left side of Figure 1. As in the non-graded hierarchy (cf. Subsection 4.2), we have defined three tools for each structure of the graded-hierarchy, but these tools have some particularities that we explain as follows. Gathering the components of a graded algebraic structure. For each structure of the graded hierarchy, we have defined a record that gathers the operations of the structure — the relations between structures are captured using the same ideas presented in Subsection 4.2. In this new hierarchy, the basic object is the graded setoid. The record associated with this graded structure contains three fields: graded-inv,graded-eq and index-sets. When we define a concrete graded setoid, the value of the graded-inv and graded-eq slots will be respectively a function symbol of arity 2 (representing the underlying graded set of the setoid) and a function symbol of arity 3 (encoding the intended equivalence relation). The value of the index-sets slot will be a list with a sole element: a function name that represents the characteristic function of the index set of the graded setoid. Using the same record, we can also work with n-graded setoids (i.e. a family of setoids indexed on nsets). In the general case, the arities of graded-inv and graded-eq functions will be n+1 and n+2 respectively; and, the value of the index-sets slot will be a list whose elements are nfunction names encoding the ncharacteristic functions of the nsets. If the value of index-sets is an empty list, we have an object “equivalent” to a setoid instance as presented in Section 4. The index-sets slot will be inherited from the graded-setoid structure to the rest of the graded structures of the hierarchy. Simplifying the statement of definitional axioms. In addition to the records in charge of representing each graded structure, we have defined the macros that provide their definitional axioms (check-S-p macros). As we have just explained, the same record is used to encode an n-graded structure for different values of n(this value is determined by the length of the list stored in the index-set slot of the underlying graded setoid); hence, the check-S-p macros have been defined to produce a term depending on the value of n. Modelling Algebraic Structures and Morphisms in ACL2 21 Simplifying the definition of generic instances. Finally, we have introduced a number of macros to define generic instances of an indexed family of structures (defgeneric-S macros). These macros are parameterised by a list of function names. This list encodes the characteristic functions of the underlying index sets of the generic indexed family of structures. 6.2 Chain Complexes and the Cone Construction The graded-hierarchy of algebraic structures is the basis to define a set of tools to work with chain complexes and chain complex morphisms. Definition 2 Achain complex,C∗, is a family C∗= (Cn, dCn)n∈Zwhere (Cn)n∈Zis a family of R-modules indexed on the integers and (dCn)n∈Z(the differential map) is a family of R-module endomorphisms of degree −1 (dCn: Cn→Cn−1) such that dCn−1dCn= 0 (this property is known as nilpotency condition). Let C∗= (Cn, dCn)n∈Zand D∗= (Dn, dDn)n∈Zbe two chain complexes, achain complex morphism from C∗to D∗is a family of R-module morphisms f= (fn)n∈Zsuch that dDnfn=fn−1dCnfor each n∈Z. We include some comments about the records that encode chain complexes and chain complex morphisms. The instrumental notion in the definition of chain complexes is that of graded R-module. This graded structure is-a graded Abelian group that uses a ring as part of its definition; then, the graded and non-graded hierarchy are necessary to define a graded R-module. From this graded structure, we can represent chain complexes using the following record. (defstructure chain-complex graded-R-module diff) The value of graded-R-module will be a graded-R-module instance, C, indexed on the set of integer numbers, and diff will be a function symbol of arity 2 encoding the differential map, whose mathematical signature is diff:Z× C → C — i.e. the differential map is uncurried, the subscript of the differential map is now one of the inputs (uncurrying is a common mechanism to simulate higher-order using first-order tools). Chain complexes are used to define chain complex morphisms; in particular, the representation of chain complex morphisms is given by the record (defstructure chain-complex-morphism source target map) where the value of both source and target slots will be chain-complex instances, and the value of map will be a function symbol whose arity is 2 — as in the case of the differential map in chain complexes, the map of the chain complex morphism is uncurried. As in the rest of the structures and morphisms presented throughout the paper, we have defined three tools for chain complexes (and chain complex 22 J´onathan Heras et al. morphisms): the record that we have just presented to gather the operations of the structure, a macro to check whether the definitional axioms of chain complexes (or chain complex morphisms) are fulfilled, and a macro to create generic chain complex (or chain complex morphism) instances. The behaviour of the macros is analogous to the macros presented previously. Once that we have introduced the set of tools to work with chain complexes and chain complex morphisms, we can follow the steps of the proof-scheme presented in Subsection 5.4 to create generic theories about these notions. In particular, we consider a construction implemented in Kenzo: the cone of a chain complex morphism [59] — this construction is important in Homological Algebra and plays an important role, for instance, in the proof of the Short Exact Sequences theorems [59]. Definition 3 Let C∗= (Cn, dCn)n∈Zand D∗= (Dn, dDn)n∈Zbe two chain complexes and φ:D∗→C∗be a chain complex morphism. Then, the cone of φ, denoted by Cone(φ)=(An, dAn)n∈Z, is defined as: An:= Cn+1 ⊕Dn(an element x∈Anis a pair such that its first component belongs to Cn+1 and the second component to Dn); and dAn:Cn+1 ⊕Dn→Cn⊕Dn−1 (cn+1, dn)7→ (dCn+1(cn+1) + φ(dn),−dDn(dn)). In order to define this construction in ACL2, we start by defining a generic chain complex morphism φ(Step S.1). (defgeneric-chain-complex-morphism PHI) The above macro call produces the constant *PHI* (storing a generic chain complex morphism), and the theorem that ensures that the components of *PHI* satisfy the chain complex morphism axioms. From the components of *PHI*, we introduce the chain complex operations (9 operations are necessary to define a chain complex) defining the cone construction (Step S.3). Using these operations, we create a chain-complex instance that is assigned to a new constant, called *Cone-PHI*, for latter use (Step S.4) — in this case, Step S.2 is not required since we have the necessary tools to define the generic objects without explicitly using the encapsulate mechanism. Subsequently, we use the check-chain-complex-p macro with *Cone-PHI* as argument to prove the event which ensures that the definitional axioms of chain complex are satisfied by this instance (Step S.5). ACL2 is not able to find the proof of the event generated by this macro in the first attempt. In particular, the user needs to guide the proof for the 9 “trickiest” definitional axioms of chain complexes; the trivial definitional axioms (40 axioms) are automatically proven by ACL2. This means that the user can focus on the difficult parts of the proof; additionally, the proof of these results is guided by the suggestions generated during the failed proof. Once that these lemmas are proved, and in order to make the instantiation of the cone construction for concrete chain complex morphisms easier, we Modelling Algebraic Structures and Morphisms in ACL2 23 Definition of generic Definition of Proof of the correctness chain complex morphism cone construction of the construction from-scratch 19 function symbols 9 definitions 49 theorems 19 witnesses 84 axioms half-way 19 function symbols 9 definitions 1 macro call 19 witnesses 1 record 84 axioms hierarchical 1 macro call 9 definitions 1 macro call 1 record Table 1 Comparison between the different approaches. The approach presented in this paper is called hierarchical. The columns represent the three steps required in the development of a generic theory: (1) the definition of generic function symbols, (2) the definition of functions from the generic function symbols, and (3) the derivation of theorems from the generic function symbols. have used the generic instantiation tool [49] — a procedure which allows us to instantiate generic theories in a simple way. Other Kenzo constructions — e.g. the Easy Perturbation Lemma, the cone equivalence theorem, and the SES theorems [59] — have been formalised using the same ideas presented for the cone construction, see [33]. 6.3 A Comparison with other Approaches In the above development, we have taken advantage of the tools presented throughout this paper. However, the same formalisation could be performed from scratch, but not without difficulty, as we will see as follows. First of all, we should employ the encapsulate mechanism to define the generic chain complex morphism φ. The definition of this generic object involves 19 function symbols (to define the operations of the chain complex morphism) the corresponding 19 witnesses and 84 axioms (to ensure that the 19 function symbols fulfil the properties that characterise the chain complex morphism operations). Afterwards, from the function symbols of the generic chain complex morphism, we should introduce the operations that define the chain complex associated with the cone construction; as we said previously, this means 9 new definitions. Finally, we state the 49 events that claim that the 9 operations introduced in the previous step satisfy the definitional axioms of chain complexes. The non-trivial events are the same as before; then, the same auxiliary lemmas are necessary to prove 9 of them. Table 1 shows a comparison between the two approaches. In addition, we also consider a half-way method presented in [33] where the macros in charge of certifying that an object satisfies the axioms that characterise an algebraic structure were defined (check-S-p macros), but not the functionality to generate generic instances of concrete structures (defgeneric-S macros). Since the result that we are proving is always the same, there are some figures that are repeated in all the cases (the number of definitions of the cone construction and the auxiliary lemmas). 24 J´onathan Heras et al. To sum up, the use of the tools presented in this paper means a great improvement with respect to the other two approaches: –it solves Problems P.1–P.5 (cf. Section 3) that arise in the other two approaches, –the amount of definitions and theorems is considerably reduced; then, both the number of lines of our development and the chance of forgetting some results decrease, –the developments are more readable thanks to the use of macros, an important issue when we are documenting our work, and –the user only has to focus on the difficult parts of the proofs. We finish this section with a comparison between the ACL2 formalisation of the cone construction and the Coq formalisation of the same result [19]. As we explained in the Introduction, the gap between the ACL2 formalisation and the Kenzo code is much smaller than the one between Coq and Kenzo. In addition, there are several parts of the proof which are automatised by ACL2 and, therefore, the user only has to focus on the difficult parts; on the contrary, in the Coq formalisation all the steps must be given by the user. Moreover, in the cases where ACL2 is not able to finish the proof on its own, the user receives feedback from the system, a valuable information that can help him to complete the proof. This shows that ACL2 is as valid as Coq to formalise results coming from the Kenzo system. 7 Conclusions and Further work In this paper, we have presented a guideline to develop tools that simplify the formalisations related to algebraic structures in ACL2. This guideline has been employed to create a hierarchy of algebraic structures — a task, that as far as we are aware, had not been undertaken up to now for this system. The resultant tools facilitate the development of generic theories about algebraic structures; this has been illustrated with several examples requiring different constructions (such as subalgebras, morphisms and quotients) coming from Universal Algebra. We have also shown that it is possible to extrapolate the same ideas to deal with more complex algebraic structures; for example, structures implemented in the Kenzo computer algebra system. The benefits of using our tools and ideas have been illustrated throughout the paper, and are especially noticeable when working with complex algebraic structures or several instances of a structure. Using these tools, the limitation of ACL2’s first-order setting can be overcome thanks to the strengths of this system. With the acquired experience, the method presented in this paper could be extrapolated to other algebraic structures; for instance, Tarski Kleene Algebras which has been previously studied in Isabelle [6,23]. We are also interested in the formalisation of the generic theory of Universal Algebra, see [14, 63], but this would require further work in issues like the definition of categories. Modelling Algebraic Structures and Morphisms in ACL2 25 In addition, as we have seen in Section 4, the definition of morphism between structures always follows the same pattern; so, it would be desirable to have a tool able to automatise, at least part of, the process to generate the tools related to morphisms between structures. Our main research line for the future is the application of the tools that we have presented here to verify actual computer algebra systems. We are mainly interested in the Kenzo system, where the methodologies and tools presented in this paper can reduce the formalisation effort in works like [44,47]. References 1. A. Adams et al. Computer algebra meets automated theorem proving: Integrating Maple and PVS. In 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), volume 2152 of Lecture Notes in Computer Science, pages 27–42, 2001. 2. M. Andr´es, L. Lamb´an, J. Rubio, and J. L. Ruiz-Reina. Formalizing Simplicial Topology in ACL2. In 7th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2007), pages 34–39, 2007. 3. J. Aransay, C. Ballarin, and J. Rubio. A mechanized proof of the Basic Perturbation Lemma. Journal of Automated Reasoning, 40(4):271–292, 2008. 4. J. Aransay, C. Ballarin, and J. Rubio. Generating certified code from formal proofs: a case study in homological algebra. Formal Aspects of Computing, 22(2):193–213, 2010. 5. J. Aransay and J. Divas´on. Formalization and execution of Linear Algebra: from theorems to algorithms. In 23rd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2013), Lecture Notes in Computer Science (In Press), 2013. 6. A. Armstrong, G. Struth, and T. Weber. Programming and Automating Mathematics in the Tarski-Kleene Hierarchy. Journal of Logical and Algebraic Methods in Programming, 83(2):87–102, 2014. 7. A. Bailey. The machine-checked literate formalisation of algebra in type theory. PhD thesis, Manchester University, 1999. 8. C. Ballarin. Algebraic structures in Axiom and Isabelle: attempt at a comparison. In Programming Languages for Mechanized Mathematics (PLMMS 2007), number 07-10 in RISC-Linz Report Series, pages 75–80, 2007. 9. C. Ballarin, J. Aransay, S. Hohe, F. Kammller, and L. Paulson. The Isabelle/HOL Algebra Library, 2013. http://isabelle.in.tum.de/library/HOL/HOL-Algebra/document. pdf. 10. C. Ballarin, K. Homann, and J. Calmet. Theorems and algorithms: an interface between Isabelle and Maple. In 20th International Symposium on Symbolic and Algebraic Computation (ISSAC 1995), pages 150–157. ACM PRESS, 1995. 11. A. Bauer, E. M. Clarke, and X. Zhao. Analytica — an experiment in combining theorem proving and symbolic computation. Journal of Automated Reasoning, 21(3):295–325, 1998. 12. E. A. Bishop. Foundations of constructive analysis. McGraw-Hill Publishing Company, Ltd., 1967. 13. B. Brock. defstructure for ACL2 version 2.0. Technical report, Computational Logic, Inc., 1997. www.cs.utexas.edu/users/moore/publications/others/ defstructure-brock.ps. 14. V. Capretta. Universal Algebra in Type Theory. In 12th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in Computer Science, pages 131–148, 1999. 15. P. Cast´eran and M. Sozeau. A Gentle Introduction to Type Classes and Relations in Coq. Technical report, INRIA, 2014. http://hal.inria.fr/hal-00702455.