Documentation

CatCryptCore.Tactics.SumCases

sum_cases and pkg_coherence_lite #

Cycle-free home for the exhaustive Sum-case-splitter (sum_cases) and a lightweight SMC-coherence closer (pkg_coherence_lite) built from it.

This file depends only on Lean core metaprogramming — nothing from CatCrypt/Core, CatCrypt/Bridge, or CatCrypt/Category. That lets it be imported by foundational files such as Bridge/SemPkg.lean and Category/Affine.lean, which sit below PkgCoherence / UCCoherence in the dependency DAG.

Main contents #

When to use #

Goals of shape f = g where both sides are handler-like functions built from Sum-indexed data constructors, and the leaves are definitionally equal. Typical sites: MonoidalCategoryStruct field definitions (associator, unitors, braidings, pentagon / hexagon coherence), TypedHandler.pair/fst/snd laws, Affine-category coherence.

For richer closers that additionally normalize SPComp monad chains or reach into the deep embedding, see Tactics/SPNormalize.lean and Tactics/PkgCoherenceBang.lean.

source
partial def CatCrypt.Tactics.sumCasesCore (goal : Lean.MVarId) :
Lean.Elab.Tactic.TacticM (List Lean.MVarId)

Recursively case-split all Sum-typed variables in the local context, eliminating Empty branches via cases. Terminates because each recursive call strictly reduces the total Sum nesting depth.

source
def CatCrypt.Tactics.tacticSum_cases :
Lean.ParserDescr

Exhaustive Sum-case split on the local context. Recursively unpacks nested sums and eliminates Empty branches.

Equations
Instances For
    source
    def CatCrypt.Tactics.tacticPkg_coherence_lite :
    Lean.ParserDescr

    Lightweight SMC-coherence closer for Sum-indexed handler equalities.

    Tries in order:

    1. rfl.
    2. funext _; sum_cases; all_goals rfl.
    3. funext _ _; sum_cases; all_goals rfl (deeper curry).
    4. funext _ _ _; sum_cases; all_goals rfl.

    Use for MonoidalCategoryStruct / SymmetricCategory field goals over Sum-indexed packaged-interface tensors, where the structure morphisms reduce by case-analysis plus definitional equality.

    Equations
    Instances For