Document Open Access Logo

Proof Pearl : Playing with the Tower of Hanoi Formally

Author Laurent Théry

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2021.31.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Mathematical logic
  • Formal proof
  • Hanoi Tower

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

The Tower of Hanoi is a typical example that is used in computer science courses to illustrate all the power of recursion. In this paper, we show that it is also a very nice example for inductive proofs and formal verification. We present some non-trivial results that have been formalised in the {Coq} proof assistant.

Cite As Get BibTex

Laurent Théry. Proof Pearl : Playing with the Tower of Hanoi Formally. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.31

Author Details

Laurent Théry
  • INRIA Sophia Antipolis - Université Côte d’Azur, France

Acknowledgements

We would like to thank Paul Zimmermann for pointing us to the star problem with 4 pegs and the anonymous reviewers for their careful reading and suggestions.

Supplementary Materials

References

  1. Yves Bertot, Georges Gonthier, Sidi Ould Biha, and Ioana Pasca. Canonical Big Operators. In TPHOLs, volume 5170 of LNCS, Montreal, Canada, 2008. Google Scholar
  2. Thierry Bousch. La quatrième tour de Hanoï. Bull. Belg. Math. Soc. Simon Stevin, 21(5):895-912, 2014. Google Scholar
  3. Thierry Bousch. La Tour de Stockmeyer. Séminaire Lotharingien de Combinatoire, 77(B77d), 2017. Google Scholar
  4. Thierry Bousch, Andreas M. Hinz, Sandi Klavžar, Daniele Parisse, Ciril Petr, and Paul K. Stockmeyer. A note on the Frame-Stewart conjecture. Discrete Math., Alg. and Appl., 11(4), 2019. Google Scholar
  5. Mathematical Component. The SSReflect Proof Language. Section of the Coq refence manual, available at URL: https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html.
  6. Roberto Demontis. What is the least number of moves needed to solve the k-peg Towers of Hanoi problem? Discrete Math., Alg. and Appl., 11(1), 2019. Google Scholar
  7. Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria, 2016. URL: https://hal.inria.fr/inria-00258384.
  8. John Harrison. Without loss of generality. In TPHOLs 2009, volume 5674 of LNCS, pages 43-59, 2009. Google Scholar
  9. Andreas M. Hinz, Sandi Klavžar, Uroš Milutinović, and Ciril Petr. The Tower of Hanoi - Myths and Maths. Birkhaüser, 2013. Google Scholar
  10. Ralf Hinze. Functional pearl: la tour d'Hanoï. In ICFP, pages 3-10. ACM, 2009. Google Scholar
  11. Assia Mahboubi and Enrico Tassi. Mathematical components. available at URL: https://math-comp.github.io/mcb/book.pdf.
  12. Laurent Théry. Proof Pearl: Revisiting the Mini-Rubik in Coq. In TPHOLs, volume 5170 of LNCS, pages 310-319. Springer, 2008. Google Scholar
  13. Wikipedia. Tower of Hanoi, March 2020. available at URL: https://en.wikipedia.org/w/index.php?title=Tower_of_Hanoi&oldid=943067350.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact