Enhanced Package Coherence (pkg_coherence!)

Extends pkg_coherence with a leaf-level closer that reaches into the deep embedding.

• sp_normalize_deep — extends the minimal sp_normalize (defined in Tactics/SPNormalize.lean) with RawCode.eval unfolding, so leaf goals over reified programs reduce to pure SPComp chains.

• pkg_coherence! — the composite: try pkg_coherence; if structural leaves survive, finish them with sp_normalize_deep.

Where reflection helps

pkg_coherence by itself closes SMC structural coherence (associators, unitors, braiding, pair/fst/snd laws) because the SMC on PkgInterface is built on Sum-indexed families and every structural morphism reduces to Sum case-analysis + rfl. It does not close leaf obligations whose SPComp bodies are related by non-definitional rewrites — typical symptoms are evalWith-parameterized handlers, reified programs obtained via rawCode%, or hand-written compositions involving RawCode.substOracle. pkg_coherence! covers those by turning the leaf into a simp goal over the deep-embedding evaluation semantics.

Leaf-normalizer (deep variant)

def CatCrypt.Tactics.tacticSp_normalize_deep : Lean.ParserDescr

sp_normalize extended with RawCode.eval unfolding. Use when a leaf SPComp goal involves a reified (rawCode% …).eval on either side, or more generally any RawCode.eval application over the six core constructors.

Equations

• CatCrypt.Tactics.tacticSp_normalize_deep = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSp_normalize_deep 1024 (Lean.ParserDescr.nonReservedSymbol "sp_normalize_deep" false)

Composite tactic

def CatCrypt.Tactics.tacticPkg_coherence! : Lean.ParserDescr

Extended package-coherence tactic.

Strategy:

1. Try rfl (for trivially equal terms).
2. Try pkg_coherence (SMC-structural equality via funext + sum_cases + handler simp + rfl).
3. Fall back to funext + sum_cases, then close each leaf with the reflective mon_coherence (the ring/monoidal-coherence analog for the Kleisli bind — normal-form + one soundness lemma, MonadNormalize), and only if that misses, the sp_normalize_deep simp. mon_coherence discharges the non-definitional bind assoc/unit on concrete reified spines by rfl on normal forms, replacing the step-by-step simp.

Equations

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

Test suite