Abstract
The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets interpreted in the domain of discourse. By allowing the interpretation function to be partial or even a relation one gets a more general method known as “partial reflection”. In this paper we show how one can take advantage of the partiality of the interpretation to uniformly define a family of tactics for equational reasoning that will work in different algebraic structures. The tactics then follow the hierarchy of those algebraic structures in a natural way.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Allen, S.F., Constable, R.L., Howe, D.J., Aitken, W.: The Semantics of Reflected Proof. In: Proceedings of the 5th Symposium on Logic in Computer Science, Philadelphia, Pennsylvania, June 1990, pp. 95–197. IEEE Computer Society Press, Los Alamitos (1990)
Barthe, G., van Raamsdonk, F.: Constructor subtyping in the Calculus of Inductive Constructions. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 17–34. Springer, Heidelberg (2000)
Constructive Coq Repository at Nijmegen, http://c-corn.cs.kun.nl/
The Coq Development Team. The Coq Proof Assistant Reference Manual, Version 8.0 (April 2004)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN: the Constructive Coq Repository at Nijmegen (to appear)
Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 85–95. Springer, Heidelberg (2000)
Delahaye, D., Mayero, M.: Field: une procédure de décision pour les nombres réels en Coq. Journées Francophones des Langages Applicatifs (January 2001)
Dybjer, P., Setzer, A.: Induction-recursion and initial algebras. Annals of Pure and Applied Logic 124, 1–47 (2003)
Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: The Algebraic Hierarchy of the FTA Project. Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, 271–286 (2002)
Geuvers, H., Wiedijk, F., Zwanenburg, J.: Equational Reasoning via Partial Reflection. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 162–178. Springer, Heidelberg (2000)
Harrison, J.: The HOL Light manual (1.1) (2000), http://www.cl.cam.ac.uk/users/jrh/hol-light/manual-1.1.ps.gz
Hickey, J., Nogin, A., Constable, R.L., Aydemir, B.E., Barzilay, E., Bryukhov, Y., Eaton, R., Granicz, A., Kopylov, A., Kreitz, C., Krupski, V.N., Lorigo, L., Schmitt, S., Witty, C., Yu, X.: MetaPRL – A Modular Logical Environment. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 287–303. Springer, Heidelberg (2003)
Hoffman, M., Streicher, T.: The Groupoid Interpretation of Type Theory. In: Sambin, G., Smith, J. (eds.) Proceedings of the meeting of Twenty-five years of constructive type theory, Venice. Oxford University Press, Oxford (1996)
Thomas Streicher. Semantical Investigations into Intensional Type Theory. LMU München, Habilitationsschrift (1993)
Yu, X., Nogin, A., Kopylov, A., Hickey, J.: Formalizing Abstract Algebra in Type Theory with Dependent Records. In: Basin, D., Wolff, B. (eds.) 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pp. 13–27. Universität Freiburg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cruz-Filipe, L., Wiedijk, F. (2004). Hierarchical Reflection. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2004. Lecture Notes in Computer Science, vol 3223. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30142-4_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-30142-4_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23017-5
Online ISBN: 978-3-540-30142-4
eBook Packages: Springer Book Archive