PaperlayerView exact revision on arXiv

Source-linked AI summary

Certification of Bilateral Patience Sort in Theorema and Rocq

Isabela Drǎmnesc, Tudor Jebelean, Sorin Stratulat

arXiv:2609.34889v1cs.LO

TL;DR

Sorting correctness matters because errors can affect higher-level behavior, while comparisons of formal systems certifying non-trivial algorithms remain limited. The paper develops and certifies Patience Sort variants in Theorema and Rocq, including a transformation toward tail recursion, and compares their certification approaches. It reports that the systems differ in termination requirements and proof-checking safeguards.

  • Problem

    Comparative evidence on how formal systems support certification of non-trivial algorithms and how algorithm design relates to formal reasoning remains limited, despite the importance of correct sorting for reliable behavior.

    Source: §1 · pp. 1–2

  • Method

    The paper develops Patience Sort variants from nested recursion toward tail recursion and certifies them in Theorema and Rocq, using multisets in its Theorema approach.

    Source: §1 · pp. 1–2, Related Work · p. 3

  • Results

    The case study provides formal correctness certifications in both systems and reports differences in their certification approaches.

    Source: §1 · p. 1, §4.1 · pp. 15–16

  • Takeaways & Limitations

    Rocq permits only terminating function definitions and kernel-checks completed proofs, whereas Theorema permits non-terminating definitions and requires care with inference rules.

    Source: §4.1 · pp. 15–16

    The paper does not estimate algorithm running time or investigate time and space complexity.

    Source: Related Work · p. 4

Abstract

from arXiv · show

This is a case study on a specific version of the Patience Sort algorithm in which we illustrate the evolution of it from an intuitive but inefficient nested recursion into a more complex but more efficient tail recursion, together with its formal implementation and certification in Theorema and Rocq (formerly Coq). We identify some general principles of algorithm transformation, and we develop the necessary background theory and proof methods. As a significant distinctive aspect, the approach in Theorema uses multisets, which simplifies the whole process and makes it more intuitive. The certification process reveals significant differences between the Theorema and Rocq approaches, about which we provide a comparative analysis with respect to algorithm definition, proof development, and proof effort. This analysis offers insights into how algorithm design influences the complexity and structure of formal proofs and demonstrates how non-trivial algorithms can be effectively verified across different formal frameworks.

1 Introduction

The introduction motivates sorting correctness and identifies a gap in comparing how formal systems certify non-trivial algorithms. It presents a Patience Sort case study spanning algorithm transformation, certification in Theorema and Rocq, and analysis of the systems’ approaches.

1 Introduction

  • Correct sorting is crucial for reliable behavior, particularly in safety-sensitive autonomous and robotic systems.The introduction notes that errors in ordering can propagate into higher-level components and lead to negative consequences.Source: §1 · p. 1
  • Comparative study of how formal systems support non-trivial algorithm certification and how algorithm design interacts with formal reasoning remains limited.The related-work discussion says prior Rocq verification of this algorithm class is absent and comparisons between paradigms such as Theorema and Rocq are rare.Source: §1 · p. 2, Related Work · p. 3

Related Work

  • The paper uses multisets to express that lists contain the same elements, supporting ordering and inclusion reasoning in sorting proofs.The authors say this approach opens the possibility of efficient inference rules for these domains.Source: Related Work · p. 3
  • Prior recursive-to-tail-recursive transformation work is described as limited to subclasses or simple examples, without comprehensive automation for complex sorting functions.The cited discussion also notes that accumulator generation is not automated in one algebraic method.Source: Related Work · p. 3
  • The paper presents three Patience Sort versions, tracing an intuitive but inefficient approach toward tail recursion and illustrating transformation principles.Its specific version builds one sorted sublist by adding elements at either end, then recursively sorts and merges the remainder.Source: §1 · pp. 1–2, Related Work · p. 4
  • The Theorema work develops a theory of lists and multisets over ordered domains and a dedicated prover, using natural-style logical definitions and proofs.Theorema permits algorithm definitions directly in predicate logic rather than a programming language.Source: §1 · p. 2, Related Work · p. 4
  • The algorithms receive correctness certifications in Theorema and Rocq, alongside a comparison of expressiveness, proof structure, and proof effort.The case study uses both systems to express the algorithms and their correctness proofs.Source: §1 · p. 1, Related Work · p. 4

2 The Patience Sort Algorithm

The section develops a bilateral Patience Sort from an intuitive nested-recursive algorithm toward tail-recursive sorting, with the algorithm organized around a sorted sublist and the remaining input.

2 The Patience Sort Algorithm

  • The algorithm’s bilateral split places elements at either end of a sorted sublist when possible and recursively sorts the other sublist before combining results.The section contrasts this approach with Patience Sort’s multiple piles and k-way merge.Source: §2 · p. 4

2.1 Basic Notions and Notations

  • The background theory treats lists and multisets over a totally ordered domain and formalizes ordering, inclusion, sorting, and list-to-multiset notions.It includes five predicate definitions, one function definition, 14 algorithms, and 38 properties.Source: §2.1 · p. 5

2.2 The Straightforward Algorithm

  • The straightforward algorithm scans input into a sorted sublist and a remainder, recursively sorts the remainder, and merges the two lists.Its auxiliary functions use multiple recursive calls, making this intuitive version inefficient.Source: §2.2 · p. 6

2.3 Using a Tail-recursive Split

  • PatSplit consumes the input while maintaining the sorted sublist’s minimum and maximum and accumulating the sorted sublist and remainder.The initial call sets the first two input elements as the extrema; termination returns the sublist with those extrema added and the rest of the input.Source: §2.3 · pp. 7–8

2.4 Tail-recursive Sorting

  • The fully tail-recursive sorting version uses PatJoin to accumulate the sorted result while consuming the remaining input.Its recursion reduces the consumed input to the unsorted remainder; Merge can also be made tail-recursive if append and concat are treated as one-step functions.Source: §2.4 · pp. 8–9

3 Certification in Rocq and Theorema

The section develops the certification method and proof strategies for Patience Sort in Theorema and Rocq. It contrasts multiset-based and permutation-based correctness reasoning and explains how tail-recursive proofs use invariants.

3.1 The Certification Method

  • Theorema expresses preservation of list contents with multiset equality, while Rocq characterizes it through a permutation relation.Both systems prove that the result is sorted and contains the same elements as the input.Source: §3.1 · p. 9
  • For tail-recursive algorithms, an auxiliary invariant lemma relates changing arguments to an element equal to the unchanged main term and satisfying the correctness conditions.This formulation avoids requiring a meta-logic to describe properties of function-call arguments during computation.Source: §3.1 · pp. 9–10

3.2.1 Proving in Theorema

  • Theorema proofs are organized as trees of proof situations, with inference rules applied directly or triggered by strategies.The case study implements a prover for lists over ordered domains and multisets, including generalized induction and domain-specific rules.Source: §3.2.1 · p. 10

3.2.2 Certification Statements and Proofs

  • PatSplit requires an invariant lemma for its tail-recursive correctness proof, which proceeds by head-tail induction and is the case study’s largest proof at 55 steps.PatSort3’s correctness proof reduces to PatJoin-correctness, while PatSort1 and Merge separate permutation and sortedness statements.Source: §3.2.2 · pp. 11–12

3.3.1 Specifying the Properties of Sorting Algorithms

  • Rocq specifies sorting as returning an increasingly sorted permutation of a natural-number list, with permutation defined using both occurrence counts and membership.Soundness is split into proving permutation preservation and sortedness; the paper presents PatSort3’s specification and main lemmas while companion materials contain all three proofs.Source: §3.3.1 · pp. 13–14

3.3.2 Specifying and Certifying PatSort3

  • Rocq’s PatSort3 is defined through PatJoin, whose termination requires a user-specified well-founded measure; its correctness follows from permutation and sortedness lemmas.PatJoin preserves the permutation of its inputs, and PatSort3 is the special case PatJoin nil l.Source: §3.3.2 · pp. 14–15

4 Conclusions and Further Work

The paper compares Theorema and Rocq in algorithm definition, proof development, proof effort, and presentation. It proposes further study of algorithm transformation, lemma discovery, and interactions between the systems.

4.1 Comparison between Theorema and Rocq

  • Theorema permits partial and nonterminating functions, whereas Rocq uses typed specifications, requires total functions, and accepts only terminating definitions.Rocq can handle partial functions with the option type.Source: §4.1 · p. 15
  • Both systems use cascading proof development, but Rocq users create many lemmas themselves while Theorema relies on inference rules based on total-order properties.Rocq’s kernel checks completed proofs; Theorema permits user-defined rules that may be logically incorrect.Source: §4.1 · p. 16
  • Rocq’s final proof required more than 2,000 user interactions across 22 lemmas and one theorem, while Theorema proofs comprised 295 inference steps.Theorema presents proofs in a natural style; Rocq proof development is highly interactive and scripts can be automated with tactics and solvers.Source: §4.1 · p. 16

4.2 Future Work

  • Future work proposes formalizing rules for recursive-to-tail-recursive transformation and investigating whether lemma creation can be automated.The paper also proposes exploring translation of Rocq scripts into natural-style proofs, generating Rocq scripts from Theorema, and checking Theorema proofs with Rocq.Source: §4.2 · p. 16

A Other functions and lemmas used in the Rocq proof

The appendix lists auxiliary Rocq lemmas used to establish sortedness, permutation preservation, and PatSplit properties, alongside the main theorem that PatSort3 is correct.

A Other functions and lemmas used in the Rocq proof

  • The Rocq proof uses lemmas for sorted-list extension and concatenation, count over appended lists, and preservation of membership and counts by Merge.It also gives sortedness and non-emptiness lemmas for PatSplit, its permutation property, and the theorem that PatSort3 is correct.Source: A Other functions and lemmas used in… · p. 20
Loading 2609.34889v1…