Document Open Access Logo

Treating Congruences as Equalities Within Proofs

Author Dale Miller

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.24.pdf
  • Filesize: 0.73 MB
  • 17 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Proof theory
  • equality
  • equivalences
  • congruences

Metrics

Abstract

Gentzen’s sequent calculus is a foundational tool for describing and investigating provability, yet its fine-grained inference rules generally do not directly support automated proof search. Incorporating synthetic inferences improves automatability, but they do not provide mechanisms for reasoning naturally about the elementary mathematical notions of equivalence and congruence. In this paper, we present a first-order framework for reasoning modulo such relations within the sequent calculus. We provide a setting in which congruences can be treated as actual equalities, mirroring the informal practice of mathematicians and eliminating the need to use the lemmas typically required for formal congruence proofs. We demonstrate that this approach remains strictly first-order, avoids the complexity of higher-order or set-theoretic constructions, and yields proof systems that retain essential meta-theoretic properties.

Cite As Get BibTex

Dale Miller. Treating Congruences as Equalities Within Proofs. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 24:1-24:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.24

Author Details

Dale Miller
  • Inria Saclay & LIX Institut Polytechnique de Paris, France

Acknowledgements

I thank Kaustuv Chaudhuri, Arunava Gantait, and Dominik Kirst for useful discussions regarding the topic of this paper.

References

  1. Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, volume 27 of Applied Logic Series. Kluwer Academic Publishers, second edition, 2002. URL: https://doi.org/10.1007/978-94-015-9934-4.
  2. Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a Logical Framework based on the λΠ-calculus Modulo Theory, September 2016. Working Paper or Preprint. URL: https://hal.science/hal-01368161.
  3. Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 4(3):217-247, 1994. URL: https://doi.org/10.1093/logcom/4.3.217.
  4. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. J. of Formalized Reasoning, 7(2):1-89, 2014. URL: https://doi.org/10.6092/issn.1972-5787/4650.
  5. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, editor, 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pages 391-397, New York, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-73595-3_28.
  6. Gilles Barthe, Venanzio Capretta, and Olivier Pons. Setoids in type theory. Journal of Functional Programming, 13(2):261-293, 2003. URL: https://doi.org/10.1017/S0956796802004501.
  7. Stanley Burris and H. P. Sankappanavar. A Course in Universal Algebra, volume 78 of Graduate Texts in Mathematics. Springer-Verlag, 1981. Millennium Edition available online. URL: https://doi.org/10.1007/978-1-4613-8130-3.
  8. Alonzo Church. A formulation of the Simple Theory of Types. J. of Symbolic Logic, 5:56-68, 1940. URL: https://doi.org/10.2307/2266170.
  9. Claudio Sacerdoti Coen. A semi-reflexive tactic for (sub-)equational reasoning. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs (TYPES 2004), volume 3839 of Lecture Notes in Computer Science, pages 98-114. Springer, 2006. URL: https://doi.org/10.1007/11617990_7.
  10. Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986. Google Scholar
  11. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. J. of Automated Reasoning, 31(1):31-72, 2003. Google Scholar
  12. Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. ACM SIGPLAN Notices, 28(6):237-247, 1993. URL: https://doi.org/10.1145/155090.155113.
  13. Peter J. Freyd. Properties invariant within equivalence types of categories. In Alex Heller and Myles Tierney, editors, Algebra, Topology, and Category Theory: A Collection of Papers in Honor of Samuel Eilenberg, pages 55-61. Academic Press, New York, 1976. URL: https://doi.org/10.1016/B978-0-12-339050-9.50010-0.
  14. Peter J. Freyd and Andre Scedrov. Categories, Allegories, volume 39 of North-Holland Mathematical Library. Elsevier Science Publishers B.V., Amsterdam, Netherlands, 1990. URL: https://doi.org/10.1016/C2009-0-09144-1.
  15. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. URL: https://doi.org/10.1016/j.ic.2010.09.004.
  16. Gerhard Gentzen. The consistency of elementary number theory. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 132-213. North-Holland, Amsterdam, 1969. Translated from the 1936 German original. URL: https://doi.org/10.1016/S0049-237X(08)70823-1.
  17. Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 23:1-23:17, 2017. URL: https://doi.org/10.4230/LIPIcs.CSL.2017.23.
  18. Jean-Yves Girard. A fixpoint theorem in linear logic. An email posting to linear@cs.stanford.edu archived at https://www.seas.upenn.edu/~sweirich/types/archive/1992/msg00030.html, February 1992.
  19. Joseph A. Goguen and José Meseguer. Equality, types, modules, and (why not?) generics for logic programming. The Journal of Logic Programming, 1(2):179-210, 1984. URL: https://doi.org/10.1016/0743-1066(84)90011-X.
  20. Quentin Heath and Dale Miller. A proof theory for model checking. J. of Automated Reasoning, 63(4):857-885, 2019. URL: https://doi.org/10.1007/s10817-018-9475-3.
  21. David Hilbert. The foundations of mathematics. In Jean van Heijenoort, editor, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, pages 464-479. Harvard University Press, Cambridge, Massachusetts, 1967. URL: https://doi.org/10.4159/harvard.9780674324497.c22.
  22. Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Twenty-Five Years of Constructive Type Theory, volume 36 of Oxford Logic Guides, pages 83-111. Oxford University Press, 1998. URL: https://doi.org/10.1093/oso/9780198501275.003.0008.
  23. Oiva Ketonen. Investigations into the Predicate Calculus. College Publications, 2022. Ed. by S. Negri and J. von Plato. Google Scholar
  24. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 1-35. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_1.
  25. Michael Makkai. First order logic with dependent sorts, with applications to category theory. Manuscript, McGill University, 1995. URL: https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.
  26. Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 173(5):1-32, 2022. URL: https://doi.org/10.1016/j.apal.2022.103091.
  27. Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153-175, Amsterdam, 1982. North-Holland. Google Scholar
  28. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. URL: https://doi.org/10.1007/s10817-007-9085-y.
  29. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. URL: https://doi.org/10.1017/CBO9781139021326.
  30. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. URL: https://doi.org/10.1145/1094622.1094628.
  31. John C. Mitchell and Gordon D. Plotkin. Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3):470-502, 1988. URL: https://doi.org/10.1145/44501.45065.
  32. Sara Negri and Jan von Plato. Cut elimination in the presence of axioms. Bulletin of Symbolic Logic, 4(4):418-435, 1998. URL: https://doi.org/10.2307/420956.
  33. Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2001. Google Scholar
  34. Sara Negri and Jan von Plato. Proof Analysis: A Contribution to Hilbert’s Last Problem. Cambridge University Press, Cambridge, 2011. URL: https://doi.org/10.1017/CBO9780511921629.
  35. Peter Schroeder-Heister. Rules of definitional reflection. In M. Vardi, editor, 8th Symp. on Logic in Computer Science, pages 222-232. IEEE Computer Society Press, IEEE, June 1993. URL: https://doi.org/10.1109/LICS.1993.287585.
  36. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. 6th Vampire Workshop, 71:1-10, 2019. URL: https://doi.org/10.29007/sc9t.
  37. Matthieu Sozeau. A new look at generalized rewriting in type theory. Journal of Formalized Reasoning, 2(1):41-62, 2009. URL: https://doi.org/10.6092/issn.1972-5787/1574.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact