Defining Functions on Equivalence Classes

Lawrence C. Paulson

arxiv: 1907.07591 · v1 · pith:BWJA3OBOnew · submitted 2019-07-17 · 💻 cs.LO

Defining Functions on Equivalence Classes

Lawrence C. Paulson This is my paper

Pith reviewed 2026-05-24 19:59 UTC · model grok-4.3

classification 💻 cs.LO

keywords quotient constructionequivalence classeslemma libraryintegers from naturalsrecursive datatypesequational constraintstype definitionabstract types

0 comments

The pith

A general lemma library makes it possible to define and reason about functions on equivalence classes for quotient constructions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how quotient types, formed by identifying equivalent elements of a concrete type, can be handled through lemmas that let functions respect those equivalences. These techniques are used first to construct the integers from the natural numbers and then to define recursive datatypes obeying equational constraints. A reader would care because the lemmas replace repeated manual work with reusable rules for moving between concrete representatives and abstract classes.

Core claim

The paper claims that simple techniques resting on a general lemma library for functions that operate on equivalence classes suffice to define and reason about quotient constructions, as demonstrated by the definition of the integers from the naturals and by the construction of a recursive datatype satisfying equational constraints.

What carries the argument

A general lemma library concerning functions that operate on equivalence classes, which supplies the rules needed to lift operations from concrete values to abstract equivalence classes.

If this is right

The integers can be obtained from the natural numbers by treating the equivalence relation of difference as the quotient.
Recursive datatypes can be defined even when they must obey additional equational constraints.
Reasoning steps that previously required case analysis on representatives become direct applications of the library lemmas.
Quotient types become usable in larger developments without each new type demanding its own infrastructure.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same library structure could be applied to other algebraic quotients such as rings or groups once the appropriate equivalence is identified.
Developments that mix several quotient types might compose the lemmas rather than rebuild reasoning from scratch for each combination.
The approach suggests a pattern for any setting where one must work with sets of indistinguishable objects.

Load-bearing premise

The lemma library is general enough to meet the needs of the concrete examples without requiring any additional ad-hoc lemmas.

What would settle it

A new quotient construction that forces the user to prove several lemmas not already present in the library would show the claimed generality does not hold.

read the original abstract

A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are \emph{equivalence classes}: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Paulson gives a lemma library for lifting functions to equivalence classes that makes two standard quotient constructions routine in Isabelle/HOL.

read the letter

The core contribution is a reusable set of lemmas about functions that respect equivalence relations, so that once you prove the respect property you can define the corresponding function on the quotient type without further manual work. The paper walks through the integers constructed from naturals and then a recursive datatype subject to equational constraints, showing how the same library handles both cases. That is the practical advance: it turns what used to be a sequence of ad-hoc definitions into something closer to a standard pattern. The examples are well chosen because both appear often in formalizations. The integer construction is the usual one and the datatype example tests whether the library survives the extra constraints that recursive types impose. Both succeed with the supplied lemmas, which is the evidence that the library is general enough for these uses. The main limitation is that the paper only demonstrates coverage on these two constructions; users facing other quotient types will still need to check whether their respect proofs fall inside the existing lemmas or require one or two extra facts. That is a normal boundary for a methods paper rather than a flaw. The work is aimed at Isabelle users who regularly build abstract types via quotients. Anyone doing algebra or inductive definitions in HOL will find the library immediately usable. It is worth sending to referees because the techniques are concrete, the applications are non-trivial, and the lemmas are stated in a form that others can import and extend.

Referee Report

1 major / 1 minor

Summary. The paper presents techniques for defining and reasoning about quotient types, where elements are equivalence classes under an equivalence relation on a concrete type. It relies on a general lemma library for functions operating on equivalence classes to make such constructions simple and routine. The techniques are applied first to constructing the integers from the natural numbers and then to defining a recursive datatype subject to equational constraints.

Significance. If the lemma library proves sufficiently general, the approach would reduce the need for ad-hoc lemmas in quotient constructions, which appear frequently in formalizations of mathematics and programming language semantics. The concrete applications to integers and constrained recursive types provide test cases that could be reused or extended in other developments.

major comments (1)

The central claim (abstract) is that a single general lemma library suffices for the two applications without additional ad-hoc lemmas. The manuscript must explicitly demonstrate this coverage—e.g., by listing the lemmas invoked in each application and confirming none were added specifically for integers or the recursive datatype—since this is the load-bearing assumption for the claimed simplicity.

minor comments (1)

Clarify the precise statement of the general lemma library (e.g., which properties of the equivalence relation and the function are assumed) so readers can assess its scope independently of the examples.

Simulated Author's Rebuttal

1 responses · 0 unresolved

Thank you for the careful review and the recommendation of major revision. We value the focus on verifying the central claim about the lemma library's generality. We respond to the major comment below.

read point-by-point responses

Referee: The central claim (abstract) is that a single general lemma library suffices for the two applications without additional ad-hoc lemmas. The manuscript must explicitly demonstrate this coverage—e.g., by listing the lemmas invoked in each application and confirming none were added specifically for integers or the recursive datatype—since this is the load-bearing assumption for the claimed simplicity.

Authors: We agree that an explicit demonstration is needed to substantiate the claim. In the revised version, we will add a dedicated subsection (likely in Section 4 or an appendix) that enumerates every lemma from the general library used in the integers-from-naturals construction and every lemma used in the constrained recursive datatype. We will also add a clear statement confirming that no lemmas were introduced ad hoc for either example. This change directly addresses the request for verifiable coverage without altering the technical content. revision: yes

Circularity Check

0 steps flagged

No circularity; self-contained methods paper on lemma library

full rationale

The paper presents techniques for quotient constructions via a general lemma library on equivalence classes, applied to integers-from-naturals and constrained recursive datatypes. No derivation reduces to its inputs by construction, no parameters are fitted then renamed as predictions, and no load-bearing self-citations or ansatzes are invoked. All steps are explicit formal lemmas within the theorem prover, externally verifiable and independent of the target applications. This matches the default expectation of a non-circular methods contribution.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a methods contribution focused on lemma libraries and techniques rather than new mathematical axioms, free parameters, or invented entities. No such items are described in the abstract.

pith-pipeline@v0.9.0 · 5597 in / 1013 out tokens · 21167 ms · 2026-05-24T19:59:29.764580+00:00 · methodology

Defining Functions on Equivalence Classes

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)