Document Open Access Logo

Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper)

Author Nadeem Abdul Hamid

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.39.pdf
  • Filesize: 0.57 MB
  • 7 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.39.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Automated reasoning
Keywords
  • permutations
  • reflection
  • tactics
  • Rocq
  • Coq

Metrics

Abstract

The concept of permutations is fundamental in computer science, and is useful for specifying and reasoning about a variety of data structures and algorithms. This paper presents the implementation of a fully automated tactic for proving complex permutation goals within the Rocq Prover (formerly, Coq proof assistant). Our approach leverages proof by reflection and an iterative deepening search procedure to establish permutation relations on arbitrary lists composed of concatenation operations. We detail the construction of mapping/substitution environments, a unification algorithm, and metaprogramming tactics to automate the proof process. The potential impact of the tactic for goals involving permutations is demonstrated by significant reduction in proof script length for an existing non-trivial development.

Cite As Get BibTex

Nadeem Abdul Hamid. Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 39:1-39:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.39

Author Details

Nadeem Abdul Hamid
  • Berry College, Mount Berry, GA, USA

Acknowledgements

The author thanks students Matthew Bowker and Bernny Velasquez for participating in preliminary efforts and discussions on this development.

Supplementary Materials

References

  1. Andrew W. Appel. Verified functional algorithms. In Benjamin C. Pierce, editor, Software Foundations, volume 3. Electronic textbook, 2024. Version 1.5.5, URL: http://softwarefoundations.cis.upenn.edu.
  2. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.
  3. Frédéric Blanqui, Solange Coupet-Grimal, William Delobel, Sébastien Hinderer, and Adam Koprowski. CoLoR: a Coq library on rewriting and termination. In Eighth International Workshop on Termination (WST'06), August 2006. Google Scholar
  4. Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, LNCS, pages 515-529, Berlin, Heidelberg, 1997. Springer. URL: https://doi.org/10.1007/BFb0014565.
  5. Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs, volume 7086 of LNCS, pages 167-182, Berlin, Heidelberg, 2011. Springer. URL: https://doi.org/10.1007/978-3-642-25379-9_14.
  6. Evelyne Contejean. A certified AC matching algorithm. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, pages 70-84. Springer, Berlin, Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-25979-4_5.
  7. Evelyne Contejean. Modeling permutations in Coq for Coccinelle. In Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner, editors, Rewriting, Computation and Proof: Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pages 259-269. Springer, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-73147-4_13.
  8. foreverbell. permutation-solver. Accessed 2025-02-24. URL: https://github.com/foreverbell/permutation-solver.
  9. Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in Coq. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, LNCS, pages 98-113, Berlin, Heidelberg, 2005. Springer. URL: https://doi.org/10.1007/11541868_7.
  10. Nadeem Abdul Hamid. (Nearest) Neighbors you can rely on: Formally verified k-d tree construction and search in Coq. In Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024, Avila, Spain, April 8-12, 2024, SAC '24, pages 1684-1693, New York, NY, USA, 2024. Association for Computing Machinery. URL: https://doi.org/10.1145/3605098.3635960.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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