Setup Guide

This guide covers installation and configuration of paco-lean.

Prerequisites

You need Lean 4.26.0 or later and the Lake build tool. See the Lean 4 installation guide for setup instructions.

Alternatively, use the provided Nix flake. Run nix develop from the repository root to enter a development shell with the correct Lean version pre-configured.

nix develop

The flake handles toolchain management automatically.

Installation

Add paco-lean to your project by modifying lakefile.lean. Include the following require statement.

require paco from git
  "https://github.com/hxrts/paco-lean.git"@"main"

The @"main" specifies the branch to use.

Building

Run lake build from your project root to compile the library.

lake build

Lake will download mathlib and other dependencies on first build. This process may take 5-15 minutes depending on your connection speed and whether mathlib cache is available. Subsequent builds are much faster.

Running Tests

The test suite validates the library functions correctly. Run tests with the following command.

lake build Tests

All tests should pass without errors. If tests fail, ensure your dependencies are up to date by running lake update.

Troubleshooting

Mathlib Cache Issues

If you encounter errors like “failed to load header” or corruption messages, clear the build cache.

lake clean
lake build

This removes all compiled artifacts and rebuilds from scratch.

Dependency Updates

When mathlib or other dependencies change, update your local copies.

lake update
lake build

This fetches the latest versions specified in your lakefile.

Next Steps

See Theoretical Foundations for the mathematical concepts behind paco. See Architecture Guide for an overview of the module structure. See Basic Usage Tutorial for a tutorial on writing coinductive proofs.

Theoretical Foundations

This document explains the mathematical concepts underlying parametrized coinduction.

Standard Coinduction

Coinduction proves properties about infinite structures by showing a relation is contained in a greatest fixed point. The Knaster-Tarski theorem characterizes the greatest fixed point of a monotone function F as the union of all post-fixed points.

gfp F = ⋃ { R | R ⊆ F(R) }

A relation R is a post-fixed point when R ⊆ F(R). This means every pair in R can be justified by one application of F. To prove gfp F x y, you provide a witness relation R such that R x y and R ⊆ F(R).

This approach requires knowing the complete witness relation upfront. Every pair you want to prove related must be in R before you begin. This creates difficulties when the set of pairs grows during a proof.

The Accumulation Problem

Consider proving transitivity for a coinductive relation. Given x ~ y and y ~ z, you want to show x ~ z. The witness relation must include all intermediate pairs.

For a chain x₀ ~ x₁ ~ x₂ ~ xₙ, standard coinduction requires predicting every xᵢ ~ xⱼ pair that will arise. The number of such pairs grows quadratically with chain length, and the witness relation becomes impossible to specify for infinite chains.

This is the accumulation problem. Standard coinduction cannot accumulate new facts during a proof. You must know everything before starting.

Parametrized Coinduction

Parametrized coinduction solves the accumulation problem by adding a parameter to the fixed point. The parameter holds facts that can be assumed during the proof.

paco F r = gfp (λ R. F(R ∪ r))

The relation r is the accumulator. The generating function λ R. F(R ∪ r) allows using facts from both the coinductive hypothesis R and the accumulator r.

The usable coinductive hypothesis becomes upaco F r = paco F r ∪ r. When you need to make a recursive call, you can appeal to either paco F r or directly to facts in r.

Key Properties

The key properties describe accumulation, monotonicity, and the empty accumulator case.

theorem paco_acc (F : MonoRel α) (r : Rel α) :
    paco F (paco F r) ≤ paco F r

theorem paco_mon (F : MonoRel α) {r s : Rel α} (hrs : r ≤ s) :
    paco F r ≤ paco F s

theorem paco_bot (F : MonoRel α) : paco F ⊥ = F.toOrderHom.gfp

The accumulation lemma shows nested paco can be folded. The monotonicity lemma shows larger accumulators give larger results. The empty accumulator lemma shows paco reduces to the greatest fixed point.

Generalized Paco

Generalized paco adds a second parameter for guarded facts. The parameter r holds immediate facts and g holds facts available after one F step.

gpaco F r g = paco F (r ∪ g) ∪ r

gupaco F r g = gpaco F r g ∪ g

The guard prevents immediate use of facts in g. The usable hypothesis is gupaco, which releases the guard after one step.

Relationship to Paco

When the guard is empty, gpaco reduces to upaco.

theorem gpaco_bot_g (F : MonoRel α) (r : Rel α) :
    gpaco F r ⊥ = upaco F r

When both parameters are equal, gpaco also simplifies.

theorem gpaco_diag (F : MonoRel α) (r : Rel α) :
    gpaco F r r = upaco F r

These properties show gpaco is a strict generalization of paco.

Up-To Techniques

Up-to techniques enhance coinductive proofs by allowing reasoning “up to” some closure operation. Instead of proving R ⊆ F(R), you prove R ⊆ F(clo(R)) for some closure operator clo.

A closure operator is compatible with F when clo(F(R)) ⊆ F(clo(R)) for all R. Compatibility ensures the closure does not add pairs that F cannot justify.

def Compatible (F : MonoRel α) (clo : Rel α → Rel α) : Prop :=
  ∀ R, clo (F R) ≤ F (clo R)

Standard closures include reflexive closure, symmetric closure, transitive closure, and equivalence closure. Each is compatible with appropriate classes of relation transformers.

The Companion

The companion is the greatest compatible monotone closure operator. It is defined as the supremum over all closures that are both monotone and compatible with F.

def companion (F : MonoRel α) : Rel α → Rel α :=
  ⨆ clo, (· : { clo // CloMono clo ∧ Compatible F clo}).val

The companion subsumes all other compatible closures. If a closure clo is compatible with F, then clo R ≤ companion F R for all R. This makes the companion a universal choice.

The companion satisfies three key properties. It is extensive, meaning R ≤ companion F R. It is compatible with F. It absorbs gupaco, meaning gupaco_clo F (companion F) R ≤ companion F R.

In practice, the companion is useful when you do not know which specific closure to use. By choosing the companion, you get the maximum up-to reasoning power without committing to a particular closure.

References

The theoretical foundations of paco come from academic research on coinduction and bisimulation.

• Hur et al. “The Power of Parameterization in Coinductive Proof” (POPL 2013) introduces parametrized coinduction
• Hur et al. “An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction” (CPP 2020) introduces gpaco
• Pous and Sangiorgi “Enhancements of the bisimulation proof method” covers up-to techniques

Architecture Guide

This document describes the module structure and design decisions of paco-lean.

Module Overview

The library is organized into core modules and up-to technique modules. Core modules provide parametrized coinduction without closure operators. Up-to modules extend this with enhanced reasoning capabilities.

Paco.lean (root)
├── Paco/Basic.lean      -- Core definitions
├── Paco/GPaco.lean      -- Generalized paco
├── Paco/Tactic.lean     -- Proof tactics
├── Paco/Companion.lean  -- Companion construction
├── Paco/Compat.lean     -- Coq naming aliases
├── Paco/Coind.lean      -- Coinduction wrappers
├── Paco/Simp.lean       -- Simp lemmas
└── Paco/UpTo/           -- Up-to techniques
    ├── Rclo.lean        -- Reflexive closure
    ├── Compat.lean      -- Compatibility
    ├── Cpn.lean         -- Companion
    ├── GPacoClo.lean    -- GPaco with closures
    ├── WCompat.lean     -- Weak compatibility
    ├── Closures.lean    -- Standard closures
    ├── Respectful.lean  -- Respectfulness (umbrella)
    ├── Respectful/       -- Respectfulness submodules
    │   ├── Core.lean      -- Compatible' + companion bridge
    │   ├── Tagged.lean    -- Tagged relations for proofs
    │   ├── WRespectful.lean
    │   ├── PRespectful.lean
    │   └── GRespectful.lean
    └── Compose.lean     -- Closure composition

Import Paco to get all functionality. Individual modules can be imported for smaller dependency footprints.

Core Modules

Paco/Basic.lean

This module defines the fundamental types and operations. The Rel α type represents binary relations as functions α → α → Prop.

def Rel (α : Type*) := α → α → Prop

The lattice operations use pointwise definitions. The bottom element ⊥ is the empty relation. The top element ⊤ is the total relation.

structure MonoRel (α : Type*) where
  toFun : Rel α → Rel α
  mono : Monotone toFun

The MonoRel α type bundles a relation transformer with a monotonicity proof. This bundling ensures transformers used with paco are monotone. The paco and upaco definitions provide the core parametrized coinduction interface.

Paco/GPaco.lean

This module extends paco with a second parameter for guarded facts. The gpaco F r g definition represents generalized parametrized coinduction. The gupaco F r g definition provides the usable coinductive hypothesis.

Key theorems connect gpaco to paco. When the guard is empty or equals the accumulator, gpaco simplifies.

Paco/Tactic.lean

This module provides tactics that mirror the Coq paco library. The pfold tactic folds an F-step into paco. The punfold tactic unfolds paco to expose F.

The pstep tactic moves into the paco side of upaco. The pbase tactic uses the accumulator side. The pclearbot tactic simplifies upaco F ⊥ to paco F ⊥.

Paco/Coind.lean

This module provides ergonomic wrappers for coinduction. The coind theorem hides plumbing for simple proofs. The coind_acc theorem handles accumulators.

For gpaco and up-to reasoning, gcoind, upto_coind, and companion_coind provide entry points with reduced boilerplate.

Paco/Compat.lean

This module provides naming aliases for users familiar with the Coq paco library. It maps Coq names to their Lean equivalents.

Paco/Simp.lean

This module defines additional simp lemmas for common simplifications. These supplement the core lemmas marked with @[simp] in other modules.

Up-To Modules

Paco/UpTo/Rclo.lean

This module defines rclo, the reflexive-transitive closure under a closure operator. The definition uses an inductive type with base case and closure application.

inductive rclo (clo : Rel α → Rel α) (R : Rel α) : Rel α where
  | base (h : R x y) : rclo clo R x y
  | clo (R' : Rel α) (hR' : R' ≤ rclo clo R) (h : clo R' x y) : rclo clo R x y

The base constructor injects R into rclo. The clo constructor applies the closure to any relation contained in rclo. This formulation allows iterating a closure while accumulating results.

Paco/UpTo/Compat.lean

This module defines compatibility between transformers and closures. A closure is compatible with F when clo (F R) ≤ F (clo R).

def Compatible (F : MonoRel α) (clo : Rel α → Rel α) : Prop :=
  ∀ R, clo (F R) ≤ F (clo R)

Compatibility ensures the closure preserves the F-structure needed for soundness.

Paco/UpTo/Cpn.lean

This module constructs the companion as a supremum over compatible monotone closures. The companion is the greatest closure satisfying both monotonicity and compatibility.

Paco/UpTo/GPacoClo.lean

This module defines gpaco with user-provided closures. The gpaco_clo F clo r rg definition composes F with rclo clo. Key theorems include coinduction principles and accumulation.

Paco/UpTo/WCompat.lean

This module provides weak compatibility, a relaxed notion using gupaco instead of paco. Weak compatibility is easier to establish for some closures.

Paco/UpTo/Closures.lean

This module defines standard closure operators. These include reflClosure, symmClosure, transClosure, rtClosure, and eqvClosure.

Paco/UpTo/Compose.lean

This module proves composition lemmas for closures. Composing compatible closures yields a compatible closure. Idempotence lemmas simplify nested applications.

Paco/UpTo/Respectful/

This directory contains the respectfulness framework. Respectfulness provides weaker conditions than compatibility for closure soundness.

The submodules include Core.lean for base definitions, WRespectful.lean for weak respectfulness, PRespectful.lean for paco respectfulness, and GRespectful.lean for generalized respectfulness. The Tagged.lean module provides internal machinery for proofs.

The tagged layer also provides the TagRoundtrip and PrespectRightGuarded assumptions. These assumptions are used to recover Compatible' from PRespectful in Lean.

Key Types

Rel α

Binary relations are the fundamental data type. All paco operations work on relations. The lattice structure provides union, intersection, and subset ordering.

MonoRel α

Bundled monotone transformers ensure well-formedness. The toFun field gives the transformer. The mono field proves monotonicity.

rclo clo R

Reflexive closure under a closure operator. This type accumulates closure applications starting from base relation R.

Design Decisions

Bundled Monotone Transformers

The MonoRel type bundles transformers with monotonicity proofs. This prevents errors from passing non-monotone functions to paco. The alternative of requiring monotonicity at each use site would create proof obligations throughout client code.

Simp Lemma Strategy

Some lemmas are marked @[simp] while others are not. The paco_eq and gpaco_step lemmas can cause simp loops and are not marked. Lemmas that always reduce complexity are marked.

Basic Usage Tutorial

This tutorial teaches you to write coinductive proofs using paco. It assumes familiarity with the concepts in Theoretical Foundations.

Defining a Monotone Transformer

Every paco proof starts with a monotone relation transformer. The transformer specifies the one-step behavior of your coinductive relation.

import Paco

def EqF : Paco.MonoRel α :=
  ⟨fun R x y => x = y ∨ R x y, by
    intro R S hRS x y hxy
    cases hxy with
    | inl heq => exact Or.inl heq
    | inr hR => exact Or.inr (hRS x y hR)
  ⟩

This transformer relates x and y if they are equal or if R relates them. The monotonicity proof shows that enlarging R enlarges the output. The inl case handles equality. The inr case uses the hypothesis that R ≤ S.

Simple Coinduction

The paco_coind theorem is the main coinduction principle. It takes a witness relation R and shows paco F r x y when R is a post-fixpoint containing (x, y).

theorem paco_eq (x : α) : paco EqF ⊥ x x := by
  apply paco_coind EqF (fun a b => a = b) ⊥
  · intro a b hab
    subst hab
    simp only [Rel.sup_bot]
    exact Or.inl rfl
  · rfl

The first argument after EqF is the witness relation. Here it is equality. The second argument is the accumulator, which is ⊥ for proofs without accumulation.

The first goal shows the witness is a post-fixpoint. The second goal shows the witness contains (x, x).

Using the Coind Wrapper

The coind wrapper from Paco.Coind simplifies the interface. It reorders arguments and handles the ⊥ accumulator case.

theorem paco_eq' (x : α) : paco EqF ⊥ x x := by
  apply coind (R := fun a b => a = b)
  · rfl
  · intro a b hab
    subst hab
    exact Or.inl rfl

The witness comes first, then the membership proof, then the step function. The step function does not need the ⊔ r part since the accumulator is handled internally.

Working with the Accumulator

When you have facts to accumulate, use coind_acc. The step function receives R ⊔ r as the recursive relation.

theorem paco_with_acc (x : α) (r : Rel α) (hr : r x x) : paco EqF r x x := by
  apply coind_acc (R := fun a b => a = b)
  · rfl
  · intro a b hab
    subst hab
    exact Or.inl rfl

The accumulator r appears in the goal type. The step function can use facts from r by returning them on the right side of the disjunction.

Using Tactics

The tactic interface provides commands that mirror the Coq paco library.

pfold

The pfold tactic transforms a goal of paco F r x y into F (upaco F r) x y.

theorem test_pfold (x : α) : paco EqF ⊥ x x := by
  pfold
  exact Or.inl rfl

After pfold, the goal becomes EqF (upaco EqF ⊥) x x. The transformer expects either equality or a recursive call through upaco.

pstep

The pstep tactic moves into the paco side of upaco. It transforms upaco F r x y into F (upaco F r) x y.

theorem test_pstep (x : α) : upaco EqF ⊥ x x := by
  pstep
  exact Or.inl rfl

Use pstep when you need to make progress on a upaco goal.

pbase

The pbase tactic uses the accumulator side of upaco. It transforms upaco F r x y into r x y.

theorem test_pbase (x y : α) (hr : r x y) : upaco EqF r x y := by
  pbase
  exact hr

Use pbase when you can discharge the goal using accumulated facts.

pclearbot

The pclearbot tactic simplifies upaco F ⊥ to paco F ⊥.

theorem test_pclearbot (x y : α) (h : paco EqF ⊥ x y) : upaco EqF ⊥ x y := by
  pclearbot
  exact h

This is useful when the accumulator is empty and you have a paco hypothesis.

Unfolding Hypotheses

The paco_unfold theorem exposes the F-structure inside a paco hypothesis.

example (x y : α) (h : paco EqF ⊥ x y) : EqF (upaco EqF ⊥) x y :=
  paco_unfold EqF ⊥ x y h

After unfolding, you can case split on the disjunction to handle equality and recursive cases separately.

Example: Reflexivity

This complete example proves that paco EqF ⊥ is reflexive.

theorem paco_refl (x : α) : paco EqF ⊥ x x := by
  pfold
  left
  rfl

The proof folds into paco, then provides the left disjunct (equality) with rfl.

Additional Tactics

The library provides several convenience tactics for common patterns.

pmult

The pmult tactic absorbs nested paco into a single paco. It applies the accumulation lemma paco F (paco F r) ≤ paco F r.

theorem nested_paco (h : paco EqF (paco EqF r) x y) : paco EqF r x y := by
  pmult
  exact h

Use pmult when composing lemmas that each return paco results.

pdestruct

The pdestruct tactic combines unfold, destruct, and bot-clearing in one step.

example (h : paco EqF ⊥ x y) : x = y ∨ paco EqF ⊥ x y := by
  pdestruct h
  · left; assumption
  · right; assumption

This is equivalent to punfold h; cases h; pclearbot. The original hypothesis is preserved.

pinversion

The pinversion tactic is similar to pdestruct but explicitly preserves the original hypothesis.

example (h : paco EqF ⊥ x y) : x = y ∨ paco EqF ⊥ x y := by
  pinversion h
  · left; assumption
  · right; assumption

Use pinversion when you need to reference the original paco hypothesis after case analysis.

Choosing a Witness Relation

The witness relation R determines what you can prove. A good witness satisfies two properties. First, R must contain your target pair. Second, R must be a post-fixpoint of the parameterized transformer.

For reflexivity proofs, equality is often a good witness. For transitivity proofs, the transitive closure works well. For bisimulation, pairs of related states form the witness.

Start with the simplest relation that contains your target. If the post-fixpoint proof fails, expand the witness to include more pairs.

Troubleshooting

pfold does not apply

The pfold tactic expects a goal of the form paco F r x y. If your goal is upaco F r x y, use pstep instead. If your goal has a different form, you may need to unfold definitions first.

Witness is not a post-fixpoint

The step function must show R a b → F (R ⊔ r) a b. If this fails, your witness may be too small. Try expanding R to include more pairs that the F-step might produce.

Accumulator mismatch

When working with non-empty accumulators, ensure the accumulator in your goal matches the accumulator in your hypothesis. Use paco_mon to weaken from a smaller accumulator to a larger one.

Next Steps

See GPaco & Guards Tutorial for two-parameter coinduction. See Up-To Techniques Guide for enhanced reasoning with closures.

GPaco & Guards Tutorial

This tutorial explains generalized parametrized coinduction (gpaco). GPaco extends paco with a second parameter for guarded facts.

When to Use GPaco

Use gpaco when you need to delay access to certain facts until after making progress. The guard prevents immediate use of facts that would create unsound reasoning.

Standard paco provides one parameter r for accumulated facts. GPaco provides two parameters: r for immediately available facts and g for guarded facts. Guarded facts become available only after one F-step.

Available vs Guarded Parameters

The gpaco F r g relation has two parameters with different accessibility rules.

def gpaco (F : MonoRel α) (r g : Rel α) : Rel α :=
  paco F (r ⊔ g) ⊔ r

The parameter r is immediately available. You can use facts from r at any point. The parameter g is guarded. You must apply F once before accessing facts from g.

This distinction matters when certain facts would create circular reasoning if used immediately. The guard ensures you make progress before accessing them.

Guard Release

The guard releases after one F-step. When you unfold a gpaco goal with gpfold, the recursive positions receive gupaco F r g instead of gpaco F r g.

def gupaco (F : MonoRel α) (r g : Rel α) : Rel α :=
  gpaco F r g ⊔ g

The gupaco definition adds g to the available facts. This equals upaco F (r ⊔ g), meaning after one step both r and g are accessible.

theorem gupaco_eq_upaco (F : MonoRel α) (r g : Rel α) :
    gupaco F r g = upaco F (r ⊔ g)

The guard mechanism prevents using g before making progress. After the first F-step, the guard lifts and g joins the accumulator.

Coinduction with GPaco

The gpaco_coind theorem provides coinduction for gpaco. The step function can return either an F-step or an immediate base case.

theorem gpaco_coind (F : MonoRel α) (R : Rel α) (r g : Rel α)
    (step : ∀ x y, R x y → F (R ⊔ gupaco F r g) x y ∨ r x y)
    {x y : α} (hxy : R x y) : gpaco F r g x y

The step function receives R ⊔ gupaco F r g for recursive calls. It can return r x y as a base case without making an F-step.

The gcoind Wrapper

The gcoind wrapper from Paco.Coind provides a cleaner interface.

theorem gcoind {F : MonoRel α} {r g : Rel α} {x y : α}
    (R : Rel α)
    (witness : R x y)
    (step : ∀ a b, R a b → F (R ⊔ gupaco F r g) a b ∨ r a b) :
    gpaco F r g x y

The witness comes first, then the membership proof, then the step function.

Tactics

The gpfold tactic transforms a goal of gpaco F r g x y into F (gupaco F r g) x y ∨ r x y.

theorem test_gpfold (x : α) : gpaco TestF ⊥ ⊥ x x := by
  gpfold
  exact Or.inl rfl

After gpfold, you choose between making an F-step (left disjunct) or using the base case (right disjunct).

Relationship to Paco

GPaco generalizes paco. Several special cases reduce gpaco to simpler forms.

Empty Guard

When the guard is empty, gpaco reduces to upaco.

theorem gpaco_bot_g (F : MonoRel α) (r : Rel α) :
    gpaco F r ⊥ = upaco F r

With no guarded facts, gpaco behaves exactly like upaco.

Empty Available Parameter

When the available parameter is empty, gpaco reduces to paco.

theorem gpaco_bot_r (F : MonoRel α) (g : Rel α) :
    gpaco F ⊥ g = paco F g

With no base case, gpaco behaves like paco with the guard as accumulator.

Diagonal Case

When both parameters are equal, gpaco simplifies.

theorem gpaco_diag (F : MonoRel α) (r : Rel α) :
    gpaco F r r = upaco F r

There is no distinction between available and guarded when they contain the same facts.

Example: Multi-Step Proof

Consider proving a property that requires multiple F-steps with intermediate facts.

def StepF : MonoRel α :=
  ⟨fun R x y => x = y ∨ ∃ z, R x z ∧ R z y, by
    intro R S hRS x y hxy
    cases hxy with
    | inl heq => exact Or.inl heq
    | inr ⟨z, hxz, hzy⟩ => exact Or.inr ⟨z, hRS x z hxz, hRS z y hzy⟩
  ⟩

This transformer allows either equality or a two-step chain through an intermediate element.

Here is a complete proof using gpaco. The witness relation is equality, and the step function uses the left disjunct for the F-step.

theorem step_refl : gpaco StepF ⊥ ⊥ x x := by
  apply gpaco_coind StepF (fun a b => a = b) ⊥ ⊥
  · intro a b hab
    left
    subst hab
    exact Or.inl rfl
  · rfl

The proof chooses the F-step branch and provides equality. The guard and accumulator are both empty since no additional facts are needed.

Accumulation with GPaco

GPaco supports accumulation similar to paco. The gpaco_gupaco theorem shows how gupaco absorbs into gpaco.

theorem gpaco_gupaco (F : MonoRel α) (r g : Rel α) :
    gpaco F (gupaco F r g) (gupaco F r g) ≤ gpaco F r g

This enables incremental proofs where intermediate gpaco results feed into subsequent arguments.

Next Steps

See Up-To Techniques Guide for combining gpaco with closure operators.

Up-To Techniques Guide

This guide covers advanced up-to reasoning with closure operators. Up-to techniques enhance coinductive proofs by allowing reasoning modulo some closure.

What Are Up-To Techniques

Standard coinduction requires proving R ⊆ F(R) for a witness relation R. Up-to techniques relax this to R ⊆ F(clo(R)) for some closure operator clo. The closure expands R before checking the post-fixpoint condition.

This relaxation is sound when the closure is compatible with F. Compatible closures preserve the structure that F requires. The key insight is that clo(gfp F) ⊆ gfp F when clo is compatible.

Closure Operators

A closure operator expands a relation while preserving certain properties. The library provides several standard closures.

Reflexive Closure

The reflexive closure adds identity pairs.

def reflClosure (R : Rel α) : Rel α := fun x y => x = y ∨ R x y

This closure is useful when you want to reason “up to equality”. Elements can be related through R or by being equal.

Symmetric Closure

The symmetric closure adds reverse pairs.

def symmClosure (R : Rel α) : Rel α := fun x y => R x y ∨ R y x

This closure is useful when the relation you want to prove is symmetric. You only need to establish one direction.

Transitive Closure

The transitive closure allows chains through intermediate elements.

inductive transClosure (R : Rel α) : Rel α where
  | base (h : R x y) : transClosure R x y
  | trans (h₁ : transClosure R x z) (h₂ : transClosure R z y) : transClosure R x y

This closure is useful for transitivity proofs. You can compose multiple R-steps.

Reflexive-Transitive Closure

The reflexive-transitive closure combines reflexivity and transitivity.

inductive rtClosure (R : Rel α) : Rel α where
  | refl : rtClosure R x x
  | base (h : R x y) : rtClosure R x y
  | trans (h₁ : rtClosure R x z) (h₂ : rtClosure R z y) : rtClosure R x y

This closure is commonly used for reachability arguments.

Equivalence Closure

The equivalence closure generates an equivalence relation.

inductive eqvClosure (R : Rel α) : Rel α where
  | refl : eqvClosure R x x
  | base (h : R x y) : eqvClosure R x y
  | symm (h : eqvClosure R x y) : eqvClosure R y x
  | trans (h₁ : eqvClosure R x z) (h₂ : eqvClosure R z y) : eqvClosure R x y

This closure is useful when proving equivalence relations.

Compatibility

A closure is compatible with F when applying the closure before or after F yields the same containment.

def Compatible (F : MonoRel α) (clo : Rel α → Rel α) : Prop :=
  ∀ R, clo (F R) ≤ F (clo R)

The condition clo (F R) ≤ F (clo R) ensures that closure-expanded F-steps can be justified by F-steps over closure-expanded relations.

Conditional Compatibility

Most closures are compatible only with specific classes of F. The library provides conditional compatibility theorems.

theorem reflClosure_compatible (F : MonoRel α)
    (hF_refl : ∀ R : Rel α, (∀ x, R x x) → ∀ x, F R x x) :
    Compatible F reflClosure

Reflexive closure is compatible when F preserves reflexivity. If R is reflexive and F respects that, then reflClosure works as an up-to technique.

theorem symmClosure_compatible (F : MonoRel α)
    (hF_symm : ∀ R x y, F R x y → F (symmClosure R) y x) :
    Compatible F symmClosure

Symmetric closure is compatible when F respects symmetry.

Respectfulness

Respectfulness is a weaker condition than compatibility. It is often easier to prove because it makes fewer demands on the closure operator.

The library provides three variants. See the Respectfulness Variants section below for details on when to use each one.

PRespectful and tagged roundtrip

Lean does not derive Compatible' from PRespectful without extra assumptions. The library uses a tagged roundtrip strategy to recover guardedness information.

The roundtrip assumption is TagRoundtrip F clo. It states that closing on R ⊔ S is contained in closing on tagged R and S and then forgetting the tags.

The second assumption is PrespectRightGuarded F clo. It states that the guarded branch of prespectClosure is preserved by F.

Under these assumptions, prespect_compatible'_tagged yields Compatible'. If F is inflationary and clo is PRespectfulStrong, the right-guardedness condition follows automatically.

The rclo Construction

The rclo type accumulates closure applications. It is the smallest relation containing R and closed under a closure operator.

inductive rclo (clo : Rel α → Rel α) (R : Rel α) : Rel α where
  | base (h : R x y) : rclo clo R x y
  | clo (R' : Rel α) (hR' : R' ≤ rclo clo R) (h : clo R' x y) : rclo clo R x y

The base constructor injects R into rclo. The clo constructor applies the closure to any relation R’ contained in rclo. This formulation is more general than direct application to rclo itself.

GPaco with Closures

The gpaco_clo definition integrates closures with gpaco.

def gpaco_clo (F : MonoRel α) (clo : Rel α → Rel α) (r rg : Rel α) : Rel α :=
  rclo clo (paco (composeRclo F clo) (rg ⊔ r) ⊔ r)

The generating function becomes F ∘ rclo clo. This composes F with the closure accumulator. The result is wrapped in rclo clo to allow closure at the top level.

Using gpaco_clo

The gpaco_clo_cofix theorem provides coinduction for gpaco_clo.

theorem gpaco_clo_cofix (F : MonoRel α) (clo : Rel α → Rel α)
    (r rg : Rel α) (R : Rel α)
    (step : R ≤ F (rclo clo (R ⊔ upaco (composeRclo F clo) (rg ⊔ r))) ⊔ r)
    {x y : α} (hxy : R x y) : gpaco_clo F clo r rg x y

The step function receives rclo clo (R ⊔ upaco (composeRclo F clo) (rg ⊔ r)) for recursive calls. This allows applying the closure during recursion.

The library also provides gpaco_clo_coind' as a pointwise variant. This theorem applies the witness relation to the goal points directly. It avoids the need to manually apply the resulting relation to x and y.

The Companion

The companion is the greatest compatible monotone closure. It subsumes all other compatible closures for a given F.

def companion (F : MonoRel α) : Rel α → Rel α :=
  ⨆ clo, (· : { clo // CloMono clo ∧ Compatible F clo}).val

The companion is defined as the supremum over all monotone compatible closures.

Companion Properties

The companion satisfies several key properties.

theorem companion_extensive (F : MonoRel α) (R : Rel α) :
    R ≤ companion F R

theorem companion_compat (F : MonoRel α) :
    Compatible F (companion F)

theorem companion_mono (F : MonoRel α) :
    CloMono (companion F)

These lemmas state that the companion is extensive, compatible with F, and monotone.

Companion Composition

The companion is also closed under relational composition when F is composition-compatible. The ergonomic workflow is:

1. prove F preserves transitive closure
2. derive CompCompatible F
3. use companion_compose without extra arguments

/-- If F preserves transitive closure, then transClosure is compatible. --/
theorem transClosure_compatible_of_preserve (F : MonoRel α)
    (h : ∀ R, transClosure (F R) ≤ F (transClosure R)) :
    Compatible F transClosure

/-- F is compatible with relational composition. --/
class CompCompatible (F : MonoRel α) : Prop :=
  (comp : Compatible F transClosure)

-- companion closed under composition
theorem companion_compose (F : MonoRel α) (R : Rel α) [CompCompatible F] :
    ∀ a b c, companion F R a b → companion F R b c → companion F R a c

This pattern makes the composition lemma usable without passing a proof argument at each call site.

Using the Companion

The companion_coind wrapper provides coinduction with the companion closure.

theorem companion_coind {F : MonoRel α} {r rg : Rel α} {x y : α}
    (R : Rel α)
    (witness : R x y)
    (step : R ≤ F (rclo (companion F) (R ⊔ upaco (composeRclo F (companion F)) (rg ⊔ r))) ⊔ r) :
    gpaco_clo F (companion F) r rg x y

Using the companion gives you the maximum up-to reasoning power available.

Composing Closures

Compatible closures can be composed. The Paco.UpTo.Compose module provides composition theorems.

theorem compatible_compose (F : MonoRel α)
    (h₁_mono : CloMono clo₁) (h₁ : Compatible F clo₁) (h₂ : Compatible F clo₂) :
    Compatible F (clo₁ ∘ clo₂)

Composing compatible closures yields a compatible closure. This allows building custom closures from primitives.

Closure Union

Closure union combines two closures. The result applies both closures and takes the union.

def cloUnion (clo₁ clo₂ : Rel α → Rel α) : Rel α → Rel α :=
  fun R => clo₁ R ⊔ clo₂ R

infixl:65 " ⊔ᶜ " => cloUnion

theorem cloMono_union {clo₁ clo₂ : Rel α → Rel α}
    (h₁ : CloMono clo₁) (h₂ : CloMono clo₂) :
    CloMono (clo₁ ⊔ᶜ clo₂)

theorem wcompat_union (F : MonoRel α) {clo₁ clo₂ : Rel α → Rel α}
    (h₁ : WCompatible F clo₁) (h₂ : WCompatible F clo₂) :
    WCompatible F (clo₁ ⊔ᶜ clo₂)

These lemmas show closure union preserves monotonicity and weak compatibility. This helps when combining multiple up-to techniques.

Idempotence

Several closures are idempotent. Applying them twice is the same as applying once.

theorem reflClosure_idem (R : Rel α) : reflClosure (reflClosure R) = reflClosure R
theorem symmClosure_idem (R : Rel α) : symmClosure (symmClosure R) = symmClosure R
theorem eqvClosure_idem (R : Rel α) : eqvClosure (eqvClosure R) = eqvClosure R

Idempotence simplifies reasoning about nested closure applications.

Example: Up-To Reflexivity

This example proves a property using up-to reflexivity.

def EqF : MonoRel α :=
  ⟨fun R x y => x = y ∨ R x y, by
    intro R S hRS x y hxy
    cases hxy with
    | inl heq => exact Or.inl heq
    | inr hR => exact Or.inr (hRS x y hR)
  ⟩

-- EqF is reflexive when R is reflexive
theorem EqF_refl (R : Rel α) (hR : ∀ x, R x x) : ∀ x, EqF R x x :=
  fun x => Or.inl rfl

Since EqF preserves reflexivity, reflClosure is compatible with EqF. You can use up-to reflexivity in proofs involving EqF.

Example: Up-To Transitivity

For transitivity arguments, use transClosure or rtClosure. You must verify compatibility holds for your specific F.

Transitivity is sound when F distributes over transitive chains. The step function can return chains of intermediate elements, and the closure accumulates them for later justification.

Respectfulness Variants

The library provides three forms of respectfulness. Each offers a weaker condition than compatibility that is easier to verify.

WRespectful (weak respectfulness) requires that applying the closure to a relation l yields something in F of the rclo-expanded relation. This is the weakest form. Use it when you only need basic closure properties.

PRespectful (paco respectfulness) strengthens WRespectful by requiring the result lands in paco rather than just F. This variant integrates better with accumulator-based proofs.

GRespectful (generalized respectfulness) works with the companion closure. It provides the strongest guarantees and is useful for complex up-to arguments.

When to Use Respectfulness

Respectfulness is useful when direct compatibility is hard to prove. The condition clo (F R) ≤ F (clo R) required by compatibility can be difficult to establish for some closures.

Respectfulness relaxes this by allowing the closure to interact with the paco structure. The trade-off is that respectfulness requires additional assumptions about the generator F.

For generators that are inflationary (where R ≤ F R), respectfulness conditions are often easier to verify. The library provides lemmas connecting respectfulness to compatibility under these assumptions.

Differences from Coq Paco

This document describes the key architectural differences between paco-lean and the Coq paco library (GitHub). Understanding these differences helps developers choose appropriate proof strategies when working with paco-lean.

Overview

Paco-lean follows the Coq paco library closely in its core definitions. The paco, upaco, gpaco, and rclo constructions match their Coq counterparts. Both libraries provide full proving power for coinductive proofs with up-to techniques.

The key architectural difference is in how each library characterizes sound up-to techniques. Coq paco provides several sufficient conditions (wrespectfulN, prespectfulN, grespectfulN) that are known to imply compatibility. Paco-lean uses bisimulation to encode the exact boundary of what constitutes a sound up-to technique. This gives users a direct characterization rather than a collection of patterns to match.

Proof Paths Comparison

Coq paco provides a single implicit path from respectfulness to compatibility. The proof term structure handles branch tracking automatically. Users prove the weak conditions and the library derives compatibility.

Paco-lean provides multiple explicit paths. Users choose the path that best fits their use case. The paths differ in their hypotheses and assumptions.

The strong respectfulness path requires no extra assumptions. For inflationary generators, which include most practical examples, automatic instances handle the assumptions.

Strong vs Weak Conditions

Coq paco uses weak respectfulness conditions with conjunctive hypotheses. The condition prespectfulN requires both l ≤ r and l ≤ gf r to conclude that clo l lands in paco.

Paco-lean provides both weak and strong variants. The strong variant PRespectfulStrong uses a disjunctive hypothesis l ≤ r ⊔ F r directly.

-- Weak form (matches Coq, requires tagged assumptions)
structure PRespectful (F : MonoRel α) (clo : Rel α → Rel α) : Prop where
  mon : CloMono clo
  respect : ∀ l r, l ≤ r → l ≤ F r → clo l ≤ paco F (r ⊔ clo r)

-- Strong form (no extra assumptions needed)
structure PRespectfulStrong (F : MonoRel α) (clo : Rel α → Rel α) : Prop where
  mon : CloMono clo
  respect : ∀ l r, l ≤ r ⊔ F r → clo l ≤ paco F (r ⊔ clo r)

The strong form directly proves Compatible' via prespect_compatible'_strong. In practice, proving the strong condition is often no harder than proving the weak condition. When your closure respects the combined relation r ⊔ F r, use the strong form.

Inflationary Generators

Paco-lean distinguishes inflationary generators where R ≤ F R for all R. Most practical coinductive definitions are inflationary. Stream bisimulation, process equivalence, and simulation relations all have this property.

class Inflationary (F : MonoRel α) : Prop where
  h : ∀ R, R ≤ F R

When Inflationary F holds, the library provides automatic instances for ExtCompatImpliesCompat. This means the compatibility chain works without manual assumptions. The theorem prespect_compatible'_inflationary combines strong respectfulness with inflationary to derive Compatible' directly.

Coq paco does not distinguish inflationary generators explicitly. The property is used implicitly in proofs but not exposed as a reusable abstraction.

Extended Generator Framework

Both libraries use an extended generator gf' = id ⊔ gf for compatibility proofs. The Compatible' condition is compatibility with this extended generator.

Paco-lean makes the extended generator explicit via extendedGen. The ExtCompatImpliesCompat assumption captures when extended-generator compatibility implies original-generator compatibility.

def extendedGen (F : MonoRel α) : MonoRel α where
  F := fun R => R ⊔ F R
  mono := fun _ _ hRS => sup_le_sup hRS (F.mono' hRS)

class ExtCompatImpliesCompat (F : MonoRel α) : Prop where
  h : ∀ clo, CloMono clo → Compatible (extendedGen F) clo → Compatible F clo

Two sufficient conditions provide automatic instances. Inflationary generators satisfy the assumption because the identity component adds nothing new. The extendedGen itself is always inflationary, providing a bootstrapping instance.

Tagged Relation Framework

For cases requiring the weak respectfulness conditions, paco-lean provides explicit branch-tracking machinery. The Tagged framework marks whether elements came from the unguarded branch (R) or the guarded branch (F R).

inductive rcloTagged (clo : Rel α → Rel α) (F : MonoRel α) (R : Rel α) : Bool → Rel α where
  | base_unguarded : R x y → rcloTagged clo F R false x y
  | base_guarded : F R x y → rcloTagged clo F R true x y
  | clo_step : (∀ a c, R' a c → rcloTagged clo F R b a c) →
               clo R' x y → rcloTagged clo F R b x y

This machinery is only needed when using the weak PRespectful condition with non-inflationary generators. Most users can ignore it entirely by using the strong variants or inflationary instances.

The framework does provide value beyond respectfulness proofs. The Tag, tagLeft, tagRight, and projection functions form a reusable toolkit for any proof requiring explicit branch tracking.

Bisimulation-Based Boundary Characterization

The most significant difference between the libraries is how they characterize sound up-to techniques.

Coq paco provides several sufficient conditions that are known to imply compatibility. The conditions wrespectfulN, prespectfulN, and grespectfulN are patterns that users can match. If a closure fits one of these patterns, the corresponding lemma proves it embeds into the companion. If a closure does not fit these patterns, users must provide an ad-hoc compatibility proof.

Paco-lean uses bisimulation to encode the exact boundary of soundness. The TagClosed property and the preservation lemmas characterize precisely which operations maintain the structure required for compatibility. Any closure can be checked against this characterization directly.

def TagClosed (R : Rel (Tag α)) : Prop :=
  (∀ a b, R (Sum.inl a) (Sum.inr b) → False) ∧
  (∀ a b, R (Sum.inr a) (Sum.inl b) → False)

The bisimulation establishes a correspondence between relations on Tag α = Sum α α and pairs of relations on α. Operations that preserve TagClosed respect this correspondence. The preservation lemmas (projLeft_paco, prespectClosure_taggedUnion, upaco_closed) show that paco operations maintain this structure.

This approach has a concrete advantage. Users do not need to fit their closure into a predefined pattern. They can verify directly whether their closure preserves the tagged structure. The bisimulation makes the boundary explicit rather than encoding it implicitly through sufficient conditions.

Choosing a Proof Strategy

For most use cases, follow this decision process.

First, check if your generator is inflationary (R ≤ F R). If yes, use PRespectfulStrong with the automatic Inflationary instance. This path requires no manual assumptions.

If not inflationary, try proving PRespectfulStrong directly. The disjunctive hypothesis often works without needing to split cases. The theorem prespect_compatible'_strong gives you Compatible' immediately.

If the strong form is difficult, use PRespectful with explicit TagRoundtrip and PrespectRightGuarded instances. For direct compatibility proofs, use Compatible' with compatible'_le_companion.

Summary

References

See Architecture Guide for the module structure. See Up-To Techniques Guide for usage of closures and respectfulness. The Coq paco library documentation provides additional context for the original design.

Tutorial: Parametrized Coinduction Examples

This tutorial walks through three examples that demonstrate parametrized coinduction. The examples are based on the Coq paco library tutorial. Each example shows how paco simplifies coinductive proofs compared to traditional approaches.

The corresponding Lean code is in Tests/Tutorial.lean. The three examples cover stream equality, infinite tree equality, and mutual coinduction.

Prerequisites

This tutorial assumes familiarity with the concepts in Basic Usage Tutorial. Understanding the paco, upaco, and paco_coind definitions is essential.

Example 1: Stream Equality

This example defines infinite streams of natural numbers. It proves that two differently-constructed streams are equal.

Stream Definition

Streams are defined as an inductive type with a single constructor.

inductive NStream : Type where
  | cons : Nat → NStream → NStream

This definition captures the structure of a stream. Each stream consists of a head value and a tail stream. The type is finite, but we will postulate infinite inhabitants.

Infinite Streams via Axioms

Lean 4 does not support non-terminating definitions directly. We use axioms to postulate infinite streams and their equational properties.

axiom enumerate : Nat → NStream
axiom enumerate_eq : ∀ n, enumerate n = NStream.cons n (enumerate (n + 1))
axiom mapStream : (Nat → Nat) → NStream → NStream
axiom mapStream_cons : ∀ f n t,
  mapStream f (NStream.cons n t) = NStream.cons (f n) (mapStream f t)

The enumerate n stream contains the values n, n+1, n+2, and so on. The mapStream function applies a function to each element. These axioms give us the computational equations without requiring termination proofs.

An alternative approach is to use the QpfTypes library. That library provides the codata macro for defining coinductive types via quotient polynomial functors.

Stream Equality Generator

Stream equality is defined as the greatest fixed point of a generating function.

inductive SeqGen (R : NStream → NStream → Prop) : NStream → NStream → Prop where
  | mk (n : Nat) (s1 s2 : NStream) : R s1 s2 → SeqGen R (cons n s1) (cons n s2)

def SeqF : MonoRel NStream where
  F := SeqGen
  mono := seqGen_mono

def seq' (s1 s2 : NStream) : Prop := paco SeqF ⊥ s1 s2

The generator SeqGen relates two streams when they have the same head and their tails are related by R. The SeqF bundled transformer satisfies monotonicity automatically. The seq' predicate instantiates paco with an empty accumulator.

Main Example

The main theorem proves that enumerate n equals cons n (mapStream Nat.succ (enumerate n)).

theorem example_seq : ∀ n, seq' (enumerate n) (cons n (mapStream Nat.succ (enumerate n))) := by
  intro n
  unfold seq'
  apply paco_coind SeqF (fun s t => ∃ m, s = enumerate m ∧ t = cons m (mapStream Nat.succ (enumerate m))) ⊥
  · intro s t ⟨m, hs, ht⟩
    rw [enumerate_eq] at hs
    rw [enumerate_eq, mapStream_cons] at ht
    subst hs ht
    apply SeqGen.mk m
    exact Or.inl ⟨m + 1, rfl, rfl⟩
  · exact ⟨n, rfl, rfl⟩

The proof uses paco_coind with a witness relation. The witness captures all pairs of the form (enumerate m, cons m (mapStream Nat.succ (enumerate m))). After unfolding the definitions, the generator step follows directly.

In Coq, this proof using cofix requires pattern ... at 1 instead of rewrite ... at 1. The syntactic guardedness checker rejects the rewrite. With paco, guardedness is checked semantically at each step. This allows standard tactics like simp and rw to work freely.

Extracting Stream Components

The seq'_cons theorem shows how to extract information from stream equality.

theorem seq'_cons (n1 n2 : Nat) (s1 s2 : NStream)
    (h : seq' (cons n1 s1) (cons n2 s2)) : n1 = n2 ∧ seq' s1 s2 := by
  unfold seq' at h ⊢
  have h_unf := paco_unfold SeqF ⊥ _ _ h
  match h_unf with
  | SeqGen.mk n t1 t2 hR =>
    constructor
    · rfl
    · rw [upaco_bot] at hR
      exact hR

The proof unfolds the paco definition using paco_unfold. Pattern matching on the generator reveals that both streams have the same head. The tail relation follows from upaco_bot, which simplifies upaco F ⊥ to paco F ⊥.

Example 2: Infinite Tree Equality

This example involves infinite binary trees. It demonstrates compositional proofs using paco.

Tree Definition

Trees are defined with a single constructor taking a value and two subtrees.

inductive InfTree : Type where
  | node : Nat → InfTree → InfTree → InfTree

The structure is similar to streams but with two children instead of one. We again use axioms for infinite inhabitants.

Mutually Recursive Trees

We postulate four trees with mutual recursive structure.

axiom one : InfTree
axiom two : InfTree
axiom eins : InfTree
axiom zwei : InfTree

axiom one_eq : one = node 1 one two
axiom two_eq : two = node 2 one two
axiom eins_eq : eins = node 1 eins (node 2 eins zwei)
axiom zwei_eq : zwei = node 2 eins zwei

The trees one and two are defined mutually. The trees eins and zwei have a different structure but represent the same infinite objects. The goal is to prove one = eins and two = zwei.

Tree Equality Generator

Tree equality follows the same pattern as stream equality.

inductive TeqGen (R : InfTree → InfTree → Prop) : InfTree → InfTree → Prop where
  | mk (n : Nat) (t1l t1r t2l t2r : InfTree) :
      R t1l t2l → R t1r t2r → TeqGen R (node n t1l t1r) (node n t2l t2r)

def TeqF : MonoRel InfTree where
  F := TeqGen
  mono := teqGen_mono

def teq' (t1 t2 : InfTree) : Prop := paco TeqF ⊥ t1 t2

The generator requires the same root value and related subtrees. This captures the coinductive nature of tree equality.

Compositional Proof Strategy

Unlike Coq’s cofix approach, paco allows opaque lemmas. We can prove conditional equalities as separate theorems and compose them.

theorem teq'_two_one (r : Rel InfTree) (h : r two zwei) : paco TeqF r one eins := by
  apply paco_coind TeqF (fun t1 t2 => (t1 = one ∧ t2 = eins) ∨ (t1 = two ∧ t2 = node 2 eins zwei)) r
  · intro t1 t2 hR
    cases hR with
    | inl hoe =>
      obtain ⟨h1, h2⟩ := hoe
      subst h1 h2
      conv => lhs; rw [one_eq]
      conv => rhs; rw [eins_eq]
      apply TeqGen.mk 1 one two eins (node 2 eins zwei)
      · exact Or.inl (Or.inl ⟨rfl, rfl⟩)
      · exact Or.inl (Or.inr ⟨rfl, rfl⟩)
    | inr htw =>
      obtain ⟨h1, h2⟩ := htw
      subst h1 h2
      conv => lhs; rw [two_eq]
      apply TeqGen.mk 2 one two eins zwei
      · exact Or.inl (Or.inl ⟨rfl, rfl⟩)
      · exact Or.inr h
  · exact Or.inl ⟨rfl, rfl⟩

The teq'_two_one theorem proves paco TeqF r one eins under the assumption r two zwei. It parametrizes over an arbitrary relation r. When we need the fact that two = zwei, we use the assumption r.

A similar theorem teq'_one_two proves the converse direction. These lemmas can be composed using paco_acc to prove the final result.

Main Theorems

The final theorems prove one = eins and two = zwei directly.

theorem teq'_eins : teq' one eins := by
  unfold teq'
  apply paco_coind TeqF (fun t1 t2 =>
    (t1 = one ∧ t2 = eins) ∨
    (t1 = two ∧ t2 = zwei) ∨
    (t1 = two ∧ t2 = node 2 eins zwei)) ⊥
  · intro t1 t2 hR
    cases hR with
    | inl hoe =>
      obtain ⟨h1, h2⟩ := hoe
      subst h1 h2
      conv => lhs; rw [one_eq]
      conv => rhs; rw [eins_eq]
      apply TeqGen.mk 1 one two eins (node 2 eins zwei)
      · exact Or.inl (Or.inl ⟨rfl, rfl⟩)
      · exact Or.inl (Or.inr (Or.inr ⟨rfl, rfl⟩))
    | inr hrest =>
      -- handle remaining cases...
  · exact Or.inl ⟨rfl, rfl⟩

The witness relation captures all needed pairs simultaneously. This avoids the need to compose separate lemmas. The proof handles each case by unfolding the tree definitions and applying the generator.

Example 3: Mutual Coinduction

This example shows how paco handles mutually coinductive predicates. In Coq, this requires specialized paco1_2_0 and paco1_2_1 constructors. In Lean, we use sum types.

Encoding Mutual Predicates

We define two predicates eqone and eqtwo that identify trees equal to one and two respectively.

inductive EqOneTwoGen (R : (InfTree ⊕ InfTree) → (InfTree ⊕ InfTree) → Prop) :
    (InfTree ⊕ InfTree) → (InfTree ⊕ InfTree) → Prop where
  | eqone_step (tl tr : InfTree) :
      R (Sum.inl tl) (Sum.inl tl) →
      R (Sum.inr tr) (Sum.inr tr) →
      EqOneTwoGen R (Sum.inl (node 1 tl tr)) (Sum.inl (node 1 tl tr))
  | eqtwo_step (tl tr : InfTree) :
      R (Sum.inl tl) (Sum.inl tl) →
      R (Sum.inr tr) (Sum.inr tr) →
      EqOneTwoGen R (Sum.inr (node 2 tl tr)) (Sum.inr (node 2 tl tr))

The type InfTree ⊕ InfTree tags which predicate applies. Elements of the form Sum.inl t represent “t satisfies eqone”. Elements of the form Sum.inr t represent “t satisfies eqtwo”.

The generator has two constructors. The eqone_step constructor handles trees with root 1. The eqtwo_step constructor handles trees with root 2. Each requires the subtrees to satisfy the appropriate predicates.

Mutual Predicate Definitions

The individual predicates are projections from the combined paco.

def EqOneTwoF : MonoRel (InfTree ⊕ InfTree) where
  F := EqOneTwoGen
  mono := eqOneTwoGen_mono

def eqone' (t : InfTree) : Prop := paco EqOneTwoF ⊥ (Sum.inl t) (Sum.inl t)
def eqtwo' (t : InfTree) : Prop := paco EqOneTwoF ⊥ (Sum.inr t) (Sum.inr t)

The EqOneTwoF bundled transformer handles both predicates. The eqone' predicate specializes to the left injection. The eqtwo' predicate specializes to the right injection.

Mutual Coinduction Proof

The theorem eqone'_eins proves that eins satisfies eqone'.

theorem eqone'_eins : eqone' eins := by
  unfold eqone'
  apply paco_coind EqOneTwoF (fun x y => x = y ∧
    ((∃ t, x = Sum.inl t ∧ (t = eins ∨ t = one)) ∨
     (∃ t, x = Sum.inr t ∧ (t = zwei ∨ t = two)))) ⊥
  · intro x y ⟨hxy, hcase⟩
    subst hxy
    cases hcase with
    | inl heqone =>
      obtain ⟨t, hx, ht⟩ := heqone
      subst hx
      cases ht with
      | inl heins =>
        subst heins
        conv => lhs; rw [eins_eq]
        conv => rhs; rw [eins_eq]
        apply EqOneTwoGen.eqone_step eins (node 2 eins zwei)
        · exact Or.inl ⟨rfl, Or.inl ⟨eins, rfl, Or.inl rfl⟩⟩
        · exact Or.inl ⟨rfl, Or.inr ⟨node 2 eins zwei, rfl, Or.inl zwei_eq.symm⟩⟩
      | inr hone =>
        -- handle one case...
    | inr heqtwo =>
      -- handle eqtwo cases...
  · exact ⟨rfl, Or.inl ⟨eins, rfl, Or.inl rfl⟩⟩

The witness relation tracks both eqone and eqtwo simultaneously. Each case unfolds the tree definition and applies the appropriate generator constructor. The mutual structure is captured in the sum type encoding.

Key Takeaways

Parametrized coinduction provides semantic guardedness checking. Traditional cofix checks guardedness syntactically on the entire proof term. Paco checks guardedness at each step independently. This allows standard tactics to work without restriction.

The upaco construction enables incremental proofs. The coinductive hypothesis is upaco F r = paco F r ∨ r. The parameter r can accumulate facts as the proof progresses. This is essential for compositional reasoning.

The paco_acc theorem enables composition. The key property is paco F (paco F r) ≤ paco F r. Lemmas that return paco results can be composed without exposing their internal structure. This matches the opacity benefits of Coq’s theorem over Defined.

Sum types encode mutual coinduction. Multiple mutually coinductive predicates become a single paco over a sum type. The encoding is straightforward and requires no specialized library support.

Further Reading

See Tests/Examples.lean for stream equivalence with zero insertion. See Tests/ExamplesUpTo.lean for up-to techniques in coinductive proofs. The Up-To Techniques Guide covers closure operators and compatibility.