PaperlayerView exact revision on arXiv

Source-linked AI summary

Proof Repair and (Co)algebra Equivalences

E. G Plante III, Eric Paul, Cosmo Viola, G. A. Kavvos, Talia Ringer

arXiv:2610.36669v1cs.PL

TL;DR

Proof repair automates adaptations to datatype changes, but its theoretical foundations have been less developed. This paper characterizes configurations through algebra isomorphisms and dualizes the account for coinductive repair.

  • Problem

    Proof repair is understood algorithmically, but its theoretical foundations and the limits of configuration-based repair are less developed.

    Source: §1 · p. 1, §2 · p. 7

  • Method

    The paper formalizes configurations, connects them to algebra isomorphisms, and dualizes this account to develop a framework for coinductive repair.

    Source: §1 · p. 2, §6 · p. 27

  • Results

    Configurations are exactly algebra isomorphisms between initial algebras for a common polynomial functor, and dualizing this account yields foundations for coinductive repair.

    Source: §1 · p. 2, §6 · p. 27

  • Takeaways & Limitations

    Inductive repair can be justified without univalence, and programs written against an initial algebra’s universal property can be repaired by re-instantiating fold.

    Source: §3.4 · p. 14, §3.3 · p. 14

    The algebra-isomorphism characterization has force only for a fixed polynomial, since any equivalence is an algebra isomorphism for a constant polynomial functor.

    Source: §3.2 · p. 12

Abstract

from arXiv · show

Maintaining formal proofs in response to breaking changes in their dependencies is a major challenge of proof engineering. Proof repair is a kind of proof automation that lessens the burden of this challenge by automatically adapting proofs in response to those changes. While proof repair is well understood through an algorithmic lens, it has, until now, been poorly understood through a theoretical lens. We address this gap by giving the first foundational treatment of proof repair, focusing in particular on type-theoretic proof repair in response to changes in datatypes. Our key insight is that the core component of a proof repair algorithm---a ``configuration''---is exactly an algebra isomorphism. We formalize and prove this insight, answering open questions from prior work. We then take this one step further and show that, by taking the dual of this representation, we obtain proof repair over coinductive types. All of our results are formalized in Agda.

1 Introduction

Proof repair automatically adapts programs and proofs to datatype changes, but its theoretical foundations have been less developed than its algorithmic practice. This paper formalizes type-theoretic repair, identifies configurations with algebra isomorphisms, and extends the framework toward coinductive types.

Motivation

  • Proof repair automatically rewrites programs and proofs across datatype changes by using relationships grounded in a proof assistant’s type theory.The paper distinguishes this type-theoretic approach from other repair tools, including tools for imperative code and methods using large language models.Source: §1 · p. 1

Contributions

  • The paper connects proof repair to algebras to clarify the changes current tools can handle and extensions future tools might support.Its scope is the mathematical characterization of repair’s core objects, not the syntactic transformations performed over terms.Source: §1 · pp. 1–2
  • The paper establishes that configurations are algebra isomorphisms, shows repair does not require univalence, and develops foundations for coinductive repair.These results formalize prior conjectures and characterize configuration-based repair.Source: §1 · p. 2

Motivation

  • The motivating change replaces unary Nat with Bin, whose constructors represent zero and positive numbers through a separate Pos datatype.The paper uses this representation change to illustrate why proof developments may require broad updates.Source: Motivation · p. 2
  • A conversion-based repair of Nat code to Bin still routes operations through Nat, whereas a configuration can produce native Bin definitions.The motivating example converts a library’s representation from Nat to Bin; the converted result still depends on Nat.Source: Motivation · pp. 2–3

2 Proof Repair via Configurations

This section formalizes configurations as a way to represent and execute datatype repair, then establishes their relation to equivalences and prior correctness criteria. It also identifies the scope of the formalization and motivates a more abstract algebraic account.

Repair algorithm

  • Repair replaces the source datatype’s constructors and eliminators with their configured target counterparts while carrying the remaining case data over.The section illustrates this componentwise replacement by repairing a proof about Nat into one about Bin.Source: §2 · p. 4

Formalizing configurations

  • A configuration packages two inductive algebras for a common signature, including constructor algebras, eliminators, and their computation laws.This internalizes the DepConstr, DepElim, and Iota data maintained externally by PUMPKIN Pi.Source: §2 · pp. 5–6

Scope

  • The formalization handles inductive families index-by-index but excludes repairs between types with differing index types.Its signatures are non-indexed, matching the changes contemporary repair tools support.Source: §2 · p. 6

Correctness conditions

  • Configurations satisfy PUMPKIN Pi’s three coherence criteria: constructors commute with the induced map, eliminators compute on constructors, and eliminators commute with that map.The latter two criteria follow from the configuration’s structure and the constructor-respecting map.Source: §2 · p. 6

Further results

  • The additional η-principle data in prior repair formulations is unnecessary because it is derivable from the remaining configuration and correctness data.The paper proves this conjecture from prior work.Source: §2 · pp. 4, 7

Configurations and equivalences

  • Given an inductive algebra on one carrier, configurations between two carriers are equivalent to type equivalences between those carriers.The equivalence is constructed using the folds of the two inductive algebras.Source: §2 · p. 7

Scope

  • Configurations can be unnatural or useless, so proof engineers and repair tools must ensure that a chosen configuration performs useful repair.The section therefore turns to an abstract formulation intended to clarify repair’s limits and properties.Source: §2 · p. 7

3 Algebraic Foundations for Proof Repair

The algebraic perspective identifies configuration-based proof repair with algebra isomorphisms, clarifying which datatype changes it captures and how repair is determined. The section develops this account through initial algebras, W-type configurations, repair by instantiation, and a result that does not require univalence.

3.1 Warming up to Algebras

  • Nat and Bin are initial algebras for the same functor, so they share a universal property whose recursor and eliminator can be instantiated at Bin.In the example, recNat/indNat and zero/succ are replaced by recBin/indBin and bzero/binSucc, leaving the programs’ defining data untouched.Source: §3.1 · pp. 9–10

3.2 Connecting Configurations and Algebras

  • A W-type configuration is exactly an algebra equivalence between two algebras whose source is initial, and every configuration can be faithfully represented in W-type form.The canonicalization preserves the repair maps, allowing results about W-types to apply to configurations over arbitrary signatures.Source: §3.2 · p. 11
  • Configurations capture exactly datatype changes representable by an algebra isomorphism for a fixed polynomial, and the characterization has force only relative to that polynomial.The class includes representation changes preserving the intended data structure; any equivalence is an algebra isomorphism for a constant polynomial functor.Source: §3.2 · p. 12
  • The repair map between initial algebras is the unique algebra isomorphism, and applying it to programs and proofs gives their repaired forms.The coherence conditions for the induced action are witnesses that original terms map to their repairs.Source: §3.2 · pp. 12–13

3.3 Algebraic Repair

  • An algebra configuration replaces syntax-heavy configuration bookkeeping with a pair of initial algebras for one polynomial, from which the repair map and coherence conditions follow.Initiality supplies constructor commutation and the properties grounded in the source algebra’s dependent eliminator and computation rule.Source: §3.3 · p. 13
  • For a fixed algebra, repair replaces the fold at the source initial algebra with the fold at the target while keeping the defining algebra data unchanged.The repaired term mentions the source type exactly when that defining data does; induction additionally uses a carrier-dependent motive and transports the target along the repair map.Source: §3.3 · p. 14

3.4 Discussion: Repair without Univalence

  • The inductive development uses intensional Martin-Löf type theory with function extensionality as its only axiom and does not rely on univalence.The authors state that this broadens the settings where this kind of repair is justified, including Lean.Source: §3.4 · p. 14

4 Dualizing Repair: Coinductive Types and Final Coalgebras

This section develops foundations for proof repair for coinductive types by dualizing algebraic repair, using coalgebraic universal properties and configurations. It characterizes M-types through final coalgebras and identifies repair between coinductive representations with coalgebra isomorphisms, establishing the homotopy conditions needed for coherence.

4 Dualizing Repair: Coinductive Types and Final Coalgebras

  • Coinductive types model infinite data through observations and face representation changes like inductive types, but existing repair tools do not address them.The section develops foundations for repair between types such as Stream and Stream’ using coalgebraic universal properties and implementation-oriented configurations.Source: §4 · pp. 14–15

4.1 Warming up to Coalgebras

  • Final coalgebras provide corecursion, while Cubical Agda’s bisimulation principle identifies behaviorally equivalent elements with paths; homotopy-finality of Agda coinductive records remains open.The section distinguishes ordinary finality, which guarantees uniqueness of the homomorphism function, from homotopy-finality, which also fixes its witness.Source: §4.1 · pp. 17–18

4.2 Coalgebraic Repair

  • A coalgebra configuration gives two carriers final coalgebra structures for the same polynomial, inducing an isomorphism whose universal properties can be swapped to repair programs and proofs without source-type references.For Stream and Stream’, corecursive programs and coinduction proofs can be reused by changing the universal property at which they are instantiated.Source: §4.2 · p. 19

4.3 Coinductive Repair via Configurations

  • M-types are carriers with destructors satisfying corecursion, computation, and uniqueness rules; they are final coalgebras and derive coinduction rather than assuming it.Strengthening function-level uniqueness to Σ-level uniqueness defines homotopy M-types, whose existence within Cubical Agda is not established generally.Source: §4.3 · pp. 20–21
  • Coinductive configurations expose representation-specific syntax by pairing destructor algebras with corecursors, per-destructor computation rules, and function-level uniqueness.The framework is designed for repair algorithms that walk over destructor and output structure.Source: §4.3 · pp. 21–22
  • Coinductive configurations satisfy dual coherence conditions, but coinduction coherence requires the homotopy tier.The four conditions cover commuting destructors, corecursor computation and compatibility, and commuting coinduction principles. The latter uses Σ-level uniqueness to identify parallel paths; the two-dimensional principle applies through the HasHMRules interface without a truncation assumption.Source: §4.3 · pp. 22–23
  • Stream configurations model repair by swapping components, and repaired terms compute to native Stream’ data.For a set element type, streams form a homotopy coinductive configuration; observing the repaired constructor yields the expected head and next-element equations definitionally.Source: §4.3 · p. 23
  • Corecursor coherence realizes repair by instantiation, while carrier-dependent bisimulations must be transported along the repair map.The source coalgebra can be reused verbatim because it lives on a third type and does not mention either repaired carrier.Source: §4.3 · p. 23

4.4 Connecting Coinductive Configurations and Coalgebra

  • M-type rules are equivalent to final-coalgebra structure, and homotopy M-type rules to homotopy-finality.Corecursion and its β-rules provide the coalgebra homomorphism, while η gives uniqueness; the homotopy tier strengthens uniqueness to contractibility of the homomorphism space.Source: §4.4 · p. 24
  • Every coinductive configuration faithfully embeds into a canonical one-destructor M-type configuration.The induced repair maps in both directions equal those from the original configuration.Source: §4.4 · pp. 24–25
  • Over an M-type signature, coinductive configurations correspond to coalgebra isomorphisms between final coalgebras, with an equivalence at the homotopy-final tier.At the final tier the correspondence is only a logical equivalence, because finality does not determine the homomorphism witness; at the homotopy-final tier the matched data is propositional and the maps are mutually inverse.Source: §4.4 · p. 25
  • Coinductive configurations capture repair changes representable by coalgebra isomorphisms between final presentations of the same functor.At the homotopy-final tier, the isomorphism out of a final source determines a unique repair map; these changes preserve observable behavior.Source: §4.4 · p. 25

5 Related Work

The paper formalizes a line of datatype-focused proof-repair work and relates it to algebraic foundations, while distinguishing it from other repair tools, proof reuse, and prior work on (co)algebras. It also connects its formal account to automatic transfer methods.

Proof Repair

  • The foundations formalize Rocq proof-repair work on datatype changes, answering open questions about configurations while excluding supplementary automation such as decompilation.The paper describes this as the first foundational treatment of proof repair.Source: §5 · p. 26
  • Other tools repair proofs in separation logic, PVS, or JML, but address specification and proof languages different from dependent type theory.Neural proof-repair methods use training data to define their scope; the foundations may help characterize data or support well-scoped neurosymbolic tools.Source: §5 · p. 26

Proof Reuse and Transfer

  • Repair differs from broader proof reuse by adapting proofs to changes, especially breaking dependency changes outside the engineer’s control.Relaxing either condition connects repair to refinement and transfer methods, or to design principles for reusable proofs.Source: §5 · p. 26
  • The formal connection between equivalences, configurations, and algebras bridges proof repair with transfer methods that use automatic transport.The paper also identifies representation independence as a property of repair and suggests it may hold for other white-box transfer approaches.Source: §5 · p. 26

(Co)algebras and (Co)inductive Types

  • The algebraic connection builds on work linking inductive datatypes and polynomial endofunctors, including the equivalence between W-type rules and homotopy-initial algebras.Related foundations include schemas for inductive definitions, universe encodings, and container representations [20].Source: §5 · pp. 26–27
  • Prior work extends categorical datatypes to dependent type theory using inductive and coinductive types, derives M-type existence in HoTT with inductive types, and characterizes M-type identity types as indexed M-types [26].Source: §5 · p. 27

6 Conclusion

The configuration at the heart of type-theoretic proof repair is an algebra isomorphism between initial algebras for a common polynomial functor. Dualizing this account establishes foundations for repair over coinductive types.

6 Conclusion

  • A configuration is exactly an algebra isomorphism between initial algebras for a common polynomial functor.Initiality makes prior coherence conditions consequences rather than separate obligations, and determines a unique repair equivalence.Source: §6 · p. 27
  • Dualizing the account establishes foundations for coinductive repair, with new correctness criteria and a characterization of (homotopy) M-types as (homotopy-)final coalgebras.The characterization is given in Theorem 4.21.Source: §6 · p. 27
  • The development uses no univalence: its inductive results use intensional MLTT with function extensionality, while Cubical Agda supplies only the coinductive path type.The authors say this broadens the type theories in which repair is known to be justified.Source: §6 · p. 27
  • The authors expect configurations, coherence conditions, and uniqueness of repair to transfer to richer algebraic presentations of several other inductive type families.They name higher inductive, quotient inductive, inductive-inductive, and inductive-recursive types.Source: §6 · p. 27
Loading 2610.36669v1…