A mechanized proof of Higman’s lemma by open induction. (English) Zbl 1446.68188

Schuster, Peter M. (ed.) et al., Well-quasi orders in computation, logic, language and reasoning. A unifying concept of proof theory, automata theory, formal languages and descriptive set theory. Based on the minisymposium on well-quasi orders: from theory to applications within the Jahrestagung der Deutschen Mathematiker-Vereinigung (DMV), Hamburg, Germany, September 21–25, 2015 and the Dagstuhl seminar 16031 on well quasi-orders in computer science, Schloss Dagstuhl, Germany, January 17–22, 2016. Cham: Springer. Trends Log. Stud. Log. Libr. 53, 339-350 (2020).
Summary: I present a short, mechanically checked Isabelle/HOL formalization of Higman’s lemma by open induction.
For the entire collection see [Zbl 1443.03002].


68V20 Formalization of mathematics in connection with theorem provers
03B35 Mechanization of proofs and logical operations
03E05 Other combinatorial set theory
Full Text: DOI


[1] Berger, U. (2004). A computational interpretation of open induction. In 19th IEEE symposium on logic in computer science (LICS 2004) (pp. 326-334). https://doi.org/10.1109/LICS.2004.1319627.
[2] Berghofer, S. (2004). A constructive proof of Higman’s lemma in Isabelle. In Berardi, S., Coppo, M., & Damiani, F. (Eds.), Types for proofs and programs: international workshop, TYPES 2003, Torino, Italy, April 30-May 4, 2003, Revised selected papers (pp. 66-82). Berlin: Springer. https://doi.org/10.1007/978-3-540-24849-1_5. · Zbl 1100.68616
[3] Coquand, T., & Fridlender, D. (1993). A proof of Higman’s lemma by structural induction. Unpublished manuscript.
[4] Felgenhauer, B. (2015). Decreasing Diagrams II. Archive of Formal Proofs. https://isa-afp.org/entries/Decreasing-Diagrams-II.shtml. Formal proof development.
[5] Felgenhauer, B., & van Oostrom, V. (2013) Proof orders for decreasing diagrams. In van Raamsdonk, F. (Ed.), 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs) (Vol. 21, pp. 174-189). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.RTA.2013.174. · Zbl 1356.03054
[6] Fridlender, D. (1998). Higman’s lemma in type theory. In Giménez, E., & Paulin-Mohring, C. (Eds.), Types for proofs and programs: international workshop TYPES’96 Aussois, France, December 15-19, 1996 selected papers (pp. 112-133). Berlin: Springer. https://doi.org/10.1007/BFb0097789. · Zbl 0927.03080
[7] Geser, A. (1996, April). A proof of Higman’s lemma by open induction. Technical Report MIP-9606, Universitt Passau.
[8] Higman, G. (1952). Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, s3-2(1), 326-336. https://doi.org/10.1112/plms/s3-2.1.326. · Zbl 0047.03402
[9] Kruskal, J. B. (1960). Well-quasi-ordering, the Tree Theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95(2), 210-225. https://doi.org/10.1090/S0002-9947-1960-0111704-1. · Zbl 0158.27002
[10] Kruskal, J. B. (1972). The theory of well-quasi-ordering: a frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3), 297-305. https://doi.org/10.1016/0097-3165(72)90063-5. · Zbl 0244.06002
[11] Larchey-Wendling, D. (2015). A mechanized inductive proof of Kruskal’s tree theorem.
[12] Murthy, C., & Russell, J. R. (1989, October) A constructive proof of Higman’s lemma. Technical Report TR 89-1049, Cornell University, Ithaca, NY 14853-7501. http://hdl.handle.net/1813/6849.
[13] Murthy, C. R., & Russell, J. R. (1990). A constructive proof of Higman’s lemma. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS ’90), Philadelphia, Pennsylvania, USA, June 4-7, 1990 (pp. 257-267). https://doi.org/10.1109/LICS.1990.113752.
[14] Nash-Williams, C. S. J. A. (1963). On well-quasi-ordering finite trees. Mathematical Proceedings of the Cambridge Philosophical Society, 59(4), 833-835. https://doi.org/10.1017/S0305004100003844. · Zbl 0122.25001
[15] Nipkow, T., Paulson, L. C., Wenzel, M. (2002). Isabelle/HOL-a proof assistant for higher-order logic. Lecture Notes in Computer Science (Vol. 2283). Springer. https://doi.org/10.1007/3-540-45949-9. · Zbl 0994.68131
[16] Ogawa, M., & Sternagel, C. (2012, November). Open induction. Archive of Formal Proofs. https://isa-afp.org/entries/Open_induction.shtml. Formal proof development.
[17] Raoult, J.-C. (1988). Proving open properties by induction. Information Processing Letters, 29(1), 19-23. https://doi.org/10.1016/0020-0190(88)90126-3. · Zbl 0661.04002
[18] Richman, F., & Stolzenberg, G. (1993). Well quasi-ordered sets. Advances in Mathematics, 97(2), 145-153. https://doi.org/10.1006/aima.1993.1004. · Zbl 0771.03020
[19] Schwichtenberg, H., Seisenberger, M., & Wiesnet, F. (2016). Higman’s lemma and its computational content. In Kahle, R., Strahm, T., & Studer, T. (Eds.), Advances in proof theory (pp. 353-375). Cham: Springer. https://doi.org/10.1007/978-3-319-29198-7_11.
[20] Sternagel, C. (2012, April). Well-quasi-orders. Archive of Formal Proofs. https://isa-afp.org/entries/Well_Quasi_Orders.shtml. Formal proof development.
[21] Sternagel, C. (2014). Certified Kruskal’s tree theorem. Journal of Formalized Reasoning, 7(1), 45-62. https://doi.org/10.6092/issn.1972-5787/4213. · Zbl 1426.68289
[22] Sternagel, C., & Thiemann, R. (2013). Formalizing Knuth-Bendix orders and Knuth-Bendix completion. In 24th international conference on rewriting techniques and applications, Dagstuhl. LIPIcs (Vol. 21, pp. 287-302). https://doi.org/10.4230/LIPIcs.RTA.2013.287. · Zbl 1356.68201
[23] Thiemann, R., & Sternagel, C. (2009). Certification of termination proofs using \(\sf CeTA\). In 22nd international conference on theorem proving in higher-order logics (TPHOLs 2009). Lecture Notes in Computer Science (Vol. 5674, pp. 452-468). Springer. https://doi.org/10.1007/978-3-642-03359-9_31. · Zbl 1252.68265
[24] Veldman, W., & Bezem, M. (1993). Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, s2-47(2), 193-211. https://doi.org/10.1112/jlms/s2-47.2.193. · Zbl 0729.03034
[25] Vytiniotis, D., Coquand, T., Wahlstedt, D. (2012). Stop when you are almost-full. In Beringer, L. & Felty, A. (Eds.), 3rd international conference on interactive theorem proving (ITP 2012) (pp. 250-265). Berlin: Springer. https://doi.org/10.1007/978-3-642-32347-8_17. · Zbl 1360.68768
[26] Wu, C., Zhang, X., Urban, C. (2011, August). The Myhill-Nerode theorem based on regular expressions. Archive of Formal Proofs. https://isa-afp.org/entries/Myhill-Nerode.shtml. Formal proof development. · Zbl 1342.68306
[27] Wu, C. · Zbl 1314.68179
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.