Package Coherence Tactic

Automation for proving structural equalities between package compositions.

Design (Canonicalization by Normalization)

PkgInterface already carries genuine Mathlib MonoidalCategory and SymmetricCategory instances (pkgMonoidal / pkgSMC in Bridge/SemPkg.lean), so the structural isos α_, λ_, ρ_, β_ used below are Mathlib's own. pkg_coherence re-implements the coherence decider at the applied-handler level:

1. funext to introduce the handler argument
2. sum_cases to exhaustively case-split on nested Sum types
3. simp with handler + package simp lemmas to normalize
4. rfl to close each branch

This works because the monoidal structure on PkgInterface uses Sum on index types, so all structural morphisms (associators, unitors, braiding) reduce to Sum case analysis with rfl closures.

Main Tactic

• pkg_coherence — closes goals of the form f = g where f, g are handler transformers built from structural operations

Package Coherence Simp Set

Collects all simp lemmas needed for package-level structural equalities.

def tacticPkg_coherence : Lean.ParserDescr

Close structural equalities between package handler expressions.

Works on goals of the form:

• TypedHandler.pair h₁ h₂ = TypedHandler.pair h₃ h₄
• (f ≫ g) h = g (f h) (package category composition)
• (α_ I J K).hom h k = ... (monoidal structural isos)
• Handler equality under reassociation, braiding, etc.

Strategy:

1. Try rfl for trivially equal terms
2. Try funext + sum_cases + simp + rfl for structural terms
3. Fall back to funext + ext + sum_cases for deeper goals

Equations

• tacticPkg_coherence = Lean.ParserDescr.node `tacticPkg_coherence 1024 (Lean.ParserDescr.nonReservedSymbol "pkg_coherence" false)

Test Suite

Oracle Coherence

Higher-level tactic for oracle game proofs: apply structural simplification to oracle-parameterized games.

def tacticOracle_simp : Lean.ParserDescr

Simplify oracle game expressions.

Unfolds OracleGame.run, OracleGame.mk, GamePkg.toGame, GamePkg.ofGame and then applies pkg_coherence.

Equations

• tacticOracle_simp = Lean.ParserDescr.node `tacticOracle_simp 1024 (Lean.ParserDescr.nonReservedSymbol "oracle_simp" false)