Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
A Bi-directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions .pdf Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012. DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974. The paper describes the refinement algorithm for the Calculus of (Co)Inductive Constructions (CIC) implemented in the interactive theorem prover Matita. The refinement algorithm is in charge of giving a meaning to the terms, types and proof terms directly written by the user or generated by using tactics, decision procedures or general automation. The terms are written in an “external syntax” meant to be user friendly that allows omission of information, untyped binders and a certain liberal use of user defined sub-typing. The refiner modifies the terms to obtain related well typed terms in the internal syntax understood by the kernel of the ITP. In particular, it acts as a type inference algorithm when all the binders are untyped. The proposed algorithm is bi-directional: given a term in external syntax and a type expected for the term, it propagates as much typing information as possible towards the leaves of the term. Traditional mono-directional algorithms, instead, proceed in a bottom- up way by inferring the type of a sub-term and comparing (unifying) it with the type expected by its context only at the end. We propose some novel bi-directional rules for CIC that are particularly effective. Among the benefits of bi-directionality we have better error message reporting and better inference of dependent types. Moreover, thanks to bi-directionality, the coercion system for sub-typing is more effective and type inference generates simpler unification problems that are more likely to be solved by the inherently incomplete higher order unification algorithms implemented. Finally we introduce in the external syntax the notion of vector of placeholders that enables to omit at once an arbitrary number of arguments. Vectors of placeholders allow a trivial implementation of implicit arguments and greatly simplify the implementation of primitive and simple tactics.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
The Matita Interactive Theorem Prover .pdf In Automated Deduction – CADE-23, LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978-3-642-22437-9, Pages 64-69, Volume 6803, Year 2011 64-69.

Claudio Sacerdoti Coen, Enrico Tassi
Nonuniform Coercions via Unification Hints .pdf In Proceedings Types for Proofs and Programs, Revised Selected Papers, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (EPTCS), ISSN:2075-2180, DOI:10.4204/EPTCS.53.2, vol. 53, 19-26, March 2011. We introduce the notion of nonuniform coercion, which is the promotion of a value of one type to an enriched value of a different type via a nonuniform procedure. Nonuniform coercions are a generalization of the (uniform) coercions known in the literature and they arise naturally when formalizing mathematics in an higher order interactive theorem prover using convenient devices like canonical structures, type classes or unification hints. We also show how nonuniform coercions can be naturally implemented at the user level in an interactive theorem prover that allows unification hints.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Hints in Unification .pdf In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, August 17-20, 2009. LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978-3-642-03358-2, vol. 5674. 84-98. Several mechanisms such as Canonical Structures, Type Classes, or Pullbacks have been recently introduced with the aim to improve the power and flexibility of the type inference algorithm for interactive theorem provers. We claim that all these mechanisms are particular instances of a simpler and more general technique, just consisting in providing suitable hints to the unification procedure underlying type inference. This allows a simple, modular and not intrusive implementation of all the above mentioned techniques, opening at the same time innovative and unexpected perspectives on its possible applications.

Andrea Asperti, Enrico Tassi
Smart Matching .pdf Published in the proceedings of MKM2010, LNCS, Volume 6167/2010, Year 2010, Pages 263-277, DOI 10.1007/978-3-642-14128-7_23, ISBN 978-3-642-14127-0. One of the most annoying aspects in the formalization of mathematics is the need of transforming notions to match a given, existing result. This kind of transformations, often based on a conspicuous background knowledge in the given scientific domain (mostly expressed in the form of equalities or isomorphisms), are usually implicit in the mathematical discourse, and it would be highly desirable to obtain a similar behavior in interactive provers. The paper describes the superposition-based implementation of this feature inside the Matita interactive theorem prover, focusing in particular on the so called smart application tactic, supporting smart matching between a goal and a given result.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
A New Type For Tactics .pdf To appear in the proceedings of ACM SIGSAM PLMMS 2009, ISBN 978-1-60558-735-6. Published as technical report UBLCS-2009-14. The type of tactics in all (procedural) proof assistants is (a variant of) the one introduced in LCF. We discuss why this is inconvenient and we propose a new type for tactics that 1) allows the implementation of more clever tactics; 2) improves the implementation of declarative languages on top of procedural ones; 3) allows for better proof structuring; 4) improves proof automation; 5) allows tactics to rearrange and delay the goals to be proved (e.g. in case of side conditions or PVS subtyping judgements).

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
A Compact Kernel for the Calculus of Inductive Constructions .pdf Published in the Journal Sadhana, The paper describes the new kernel for the Calculus of Inductive Constructions (CIC) implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has been completely revisited since the first release, resulting in a remarkably compact implementation of about 2300 lines of OCaml code. The work is meant for people interested in implementation aspects of Interactive Provers, and is not self contained. In particular, it requires good acquaintance with Type Theory and functional programming languages.

Andrea Asperti, Enrico Tassi
Higher order proof reconstruction from paramodulation-based refutations: the unit equality case .pdf Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a first order automatic proof searching procedure, in a restricted equational framework. The automatic procedure is based on superposition rules for the unit equality case. Proof transformation techniques aimed to improve the readability of the final proof are discussed.

Claudio Sacerdoti Coen, Stefano Zacchiroli
Spurious Disambiguation Error Detection .pdf Accepted for publication in the proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae we want to present only errors related to the interpretation meant by the user, hiding errors related to other interpretations (spurious errors). We propose a heuristic to recognize spurious errors, which has been integrated with our former efficient disambiguation algorithm.

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Crafting a Proof Assistant .pdf Accepted for publication in the Proceedings of Types 2006: Conference of the Types Project. Nottingham, UK -- April 18-21, 2006. Proof assistants are complex applications whose develop- ment has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the devel- opment of Matita: a new interactive theorem prover based—as Coq—on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct com- parison between different systems and to highlight the common func- tionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
User Interaction with the Matita Proof Assistant .pdf Accepted for publication in Journal of Automated Reasoning, Special Issue on User Interfaces for Theorem Proving. Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, mostly characterized by the organization of the library as a search- able knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.

Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Tinycals: step by step tacticals .pdf In Proceedings of UITP 2006: User Interfaces for Theorem Provers. Seattle, WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007), Pages 125 - 142, ISSN:1571-0661 Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of tinycals as well as their implementation in the Matita proof assistant.

Luca Padovani, Stefano Zacchiroli
From notation to semantics: there and back again .pdf Accepted for publication in the proceedings of MKM 2006: The 5th International Conference on Mathematical Knowledge Management. Wokingham, UK -- August 11-12, 2006. Mathematical notation is a structured, open, and ambiguous language. In order to support mathematical notation in MKM applications one must necessarily take into account presentational as well as semantic aspects. The former are required to create a familiar, comfortable, and usable interface to interact with. The latter are necessary in order to process the information meaningfully. In this paper we investigate a framework for dealing with mathematical notation in a meaningful, extensible way, and we show an effective instantiation of its architecture to the field of interactive theorem proving. The framework builds upon well-known concepts and widely-used technologies and it can be easily adopted by other MKM applications.

Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
A content based mathematical search engine: Whelp .pdf In Proceedings of TYPES 2004 conference Types for Proofs and Programs. Paris, France -- December 15-18, 2004. LNCS 3839/2004, Springer-Verlag Heidelberg, ISBN 3-540-31428-8, pp. 17-32 The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The prototype, called Whelp, exploits a metadata approach for indexing the information that looks far more flexible than traditional indexing techniques for structured expressions like substitution, discrimination, or context trees. The prototype has been instantiated to the standard library of the Coq proof assistant extended with many user contributions.

Claudio Sacerdoti Coen, Stefano Zacchiroli
Efficient Ambiguous Parsing of Mathematical Formulae .pdf In Proceedings of MKM 2004 Third International Conference on Mathematical Knowledge Management. September 19th - 21st, 2004 Bialowieza - Poland. LNCS 3119/2004, Springer-Verlag Heidelberg, ISBN 3-540-23029-7, pp. 347-362 Mathematical notation has the characteristic of being ambiguous: operators can be overloaded and information that can be deduced is often omitted. Mathematicians are used to this ambiguity and can easily disambiguate a formula making use of the context and of their ability to find the right interpretation. Software applications that have to deal with formulae usually avoid these issues by fixing an unambiguous input notation. This solution is annoying for mathematicians because of the resulting tricky syntaxes and becomes a show stopper to the simultaneous adoption of tools characterized by different input languages. In this paper we present an efficient algorithm suitable for ambiguous parsing of mathematical formulae. The only requirement of the algorithm is the existence of a validity predicate over abstract syntax trees of incomplete formulae with placeholders. This requirement can be easily fulfilled in the applicative area of interactive proof assistants, and in several other areas of Mathematical Knowledge Management.