Abstract
Elimination rules tell us how we may exploit hypotheses in the course of a proof. Many common elimination rules, such as ∨-elim and the induction principles for inductively defined datatypes and relations, are parametric in their conclusion. We typically instantiate this parameter with the goal we are trying to prove, and acquire subproblems specialising this goal to particular circumstances in which the eliminated hypothesis holds. This paper describes a generic tactic, Elim, which supports this ubiquitous idiom in interactive proof and subsumes the functionality of the more specific ‘induction’ and ‘inversion’ tactics found in systems like Coq and Lego[6][7][15]. Elim also supports user-derived rules which follow the same style.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS’99, 1999.
Alan Bundy. The Automation Of Proof By Mathematical Induction. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science, 1999.
L’Équipe Coq. The Coq Proof Assistant Reference Manual. http://pauillac.inria.fr/coq/doc/main.html, Apr 2001.
Thierry Coquand. Pattern Matching with Dependent Types. In Proceedings of the Logical Framework workshop at Båstad, June 1992.
Thierry Coquand and Christine Paulin. Inductively defined types. In P. Martin-Löf and G. Mints, editors, COLOG-88. International Conference on Computer Logic, LNCS 417, pages 50–66. Springer-Verlag, 1990.
Cristina Cornes. Conception d’un langage de haut niveau de répresenatation de preuves. PhD thesis, Université Paris VII, 1997.
Cristina Cornes and Delphine Terrasse. Inverting Inductive Predicates in Coq. In Types for Proofs and Programs’95, LNCS 1158, Springer-Verlag, 1995.
N.G. de Bruijn. Telescopic Mappings in Typed Lambda-Calculus. Information and Computation, 91:189–204, 1991.
Peter Dybjer. Inductive Sets and Families inMartin-Löf’s Type Theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. CUP, 1991.
Martin Hofmann. Extensional concepts in intensional type theory. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1995.
Zhaohui Luo and Robert Pollack. LEGO Proof Development System: User’s Manual. Technical Report ECS-LFCS-92-211, Laboratory for Foundations of Computer Science, University of Edinburgh, May 1992.
Lena Magnusson. The implementation of ALF—A Proof Editor based on Martin-Löf’ s Monomorphic Type Theory with Explicit Substitutiton. PhD thesis, Chalmers University of Technology, Göteborg, 1994.
Per Martin-Löf. A theory of types. manuscript, 1971.
Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis·Napoli, 1984.
Conor McBride. Inverting inductively defined relations in LEGO. In E. Giménez and C. Paulin-Mohring, editors, Types for Proofs and Programs’96, LNCS 1512, pages 236–253, Springer-Verlag, 1998.
Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.
J. McKinna. Deliverables: A Categorical Approach to Program Development in Type Theory. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, 1992.
Dale Miller. A Logic Programming Language with Lambda-Abstraction, Function Variables and Simple Unification. Journal of Logic and Computation, 2(4):497–537, 1991.
Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321–358, 1992.
Christine Paulin-Mohring. Définitions Inductives en Théorie des Types d’Ordre Supérieur. Habilitation Thesis. Université Claude Bernard (Lyon I), 1996.
Robert Pollack. Implicit syntax.
Alan Robinson. A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM, 12:23–41, 1965.
Thomas Streicher. Investigations into intensional type theory. Habilitation Thesis, Ludwig Maximilian Universität, 1993.
P. Wadler. Views: A way for pattern matching to cohabit with data abstraction. In POPL’87. ACM, 1987.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
McBride, C. (2002). Elimination with a Motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds) Types for Proofs and Programs. TYPES 2000. Lecture Notes in Computer Science, vol 2277. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45842-5_13
Download citation
DOI: https://doi.org/10.1007/3-540-45842-5_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43287-6
Online ISBN: 978-3-540-45842-5
eBook Packages: Springer Book Archive