Structural substitution on the SO carrier

P4-pre-a of the single-carrier program. SO.replace s target replacement substitutes every subterm of s equal (in the nonplanar quotient) to target by replacement — the structural-substitution primitive on the SO carrier, replacing the legacy FreeCommMagma.lift-based SyntacticObject.replace.

The intended copy-theory use is s.replace mover SO.traceLeaf (leave an index-free trace where a mover was). Framing: this is a structural operation; the canonical MCB Internal Merge is the workspace coproduct composition (Prop 1.4.2, SO.intMerge/Workspace, #795), with traces as coproduct remainders and chains held at the workspace level (Def 1.2.1). replace supports the derived, transformational view that the paper-anchored study files are written in; it is not a claim that movement is substitution.

Built the established way (subtreesN): a planar recursion with quotient-level target matching, proved PermEquiv-invariant and lifted, then closed under IsSO via SO.ind. It is noncomputable (it rebuilds via Nonplanar.node); concrete results are related by the reduction lemmas (replace_lexLeaf/_traceLeaf/_node), not by decide.

Substitution on the planar carrier

noncomputable def Minimalist.replacePlanar (target replacement : RootedTree.Nonplanar SOLabel) : RoseTree SOLabel → RootedTree.Nonplanar SOLabel

Structural substitution on a planar SO-tree: replace every subtree equal (in the nonplanar quotient) to target by replacement, rebuilding the surrounding tree.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Minimalist.replacePlanarList (target replacement : RootedTree.Nonplanar SOLabel) : List (RoseTree SOLabel) → Multiset (RootedTree.Nonplanar SOLabel)

Auxiliary: substitute in each child, collecting the results as a multiset.

Equations

• Minimalist.replacePlanarList target replacement [] = 0
• Minimalist.replacePlanarList target replacement (c :: cs) = Minimalist.replacePlanar target replacement c ::ₘ Minimalist.replacePlanarList target replacement cs

theorem Minimalist.replacePlanar_permEquiv (target replacement : RootedTree.Nonplanar SOLabel) {t s : RoseTree SOLabel} (h : t.PermEquiv s) : replacePlanar target replacement t = replacePlanar target replacement s

replacePlanar is PermEquiv-invariant, so it descends to the quotient.

noncomputable def Minimalist.replaceN (target replacement : RootedTree.Nonplanar SOLabel) : RootedTree.Nonplanar SOLabel → RootedTree.Nonplanar SOLabel

Substitution lifted to the nonplanar carrier.

Equations

• Minimalist.replaceN target replacement = RootedTree.Nonplanar.lift (Minimalist.replacePlanar target replacement) ⋯

@[simp]

theorem Minimalist.replaceN_mk (target replacement : RootedTree.Nonplanar SOLabel) (p : RoseTree SOLabel) : replaceN target replacement (RootedTree.Nonplanar.mk p) = replacePlanar target replacement p

Reduction lemmas on leaves and bare binary nodes

theorem Minimalist.replaceN_leaf (target replacement : RootedTree.Nonplanar SOLabel) (x : SOLabel) : replaceN target replacement (RootedTree.Nonplanar.leaf x) = if RootedTree.Nonplanar.leaf x = target then replacement else RootedTree.Nonplanar.leaf x

theorem Minimalist.replaceN_node (target replacement a b : RootedTree.Nonplanar SOLabel) : replaceN target replacement (RootedTree.Nonplanar.node (Sum.inr ()) {a, b}) = if RootedTree.Nonplanar.node (Sum.inr ()) {a, b} = target then replacement else RootedTree.Nonplanar.node (Sum.inr ()) {replaceN target replacement a, replaceN target replacement b}

theorem Minimalist.replaceN_self (t r : RootedTree.Nonplanar SOLabel) : replaceN t r t = r

Replacing the whole tree (t itself) yields the replacement.

IsSO closure and SO.replace

theorem Minimalist.replaceN_isSO (target replacement s : SO) : IsSO (replaceN ↑target ↑replacement ↑s)

Substitution preserves well-formedness: replacing subterms of an SO by another SO yields an SO (the arity of every node is preserved).

noncomputable def Minimalist.SO.replace (s target replacement : SO) : SO

Structural substitution on the SO carrier ([MCB25] §1.2): replace every subterm of s equal to target by replacement. The copy-theory use is s.replace mover SO.traceLeaf. Noncomputable (rebuilds via SO.node); reduce concrete cases via replace_self/replace_node_of_ne/ replace_lexLeaf_of_ne.

Equations

• s.replace target replacement = ⟨Minimalist.replaceN ↑target ↑replacement ↑s, ⋯⟩

@[simp]

theorem Minimalist.SO.replace_val (s target replacement : SO) : ↑(s.replace target replacement) = replaceN ↑target ↑replacement ↑s

@[simp]

theorem Minimalist.SO.replace_self (target replacement : SO) : target.replace target replacement = replacement

Replacing the whole object by replacement.

theorem Minimalist.SO.replace_node_of_ne {l r target replacement : SO} (h : l.node r ≠ target) : (l.node r).replace target replacement = (l.replace target replacement).node (r.replace target replacement)

At a node that is not itself the target, substitution recurses into both daughters (the Head Feature Principle of substitution: structure is preserved).

theorem Minimalist.SO.replace_lexLeaf_of_ne {tok : LIToken} {target replacement : SO} (h : lexLeaf tok ≠ target) : (lexLeaf tok).replace target replacement = lexLeaf tok

A lexical leaf that is not the target is left unchanged.

theorem Minimalist.SO.replace_traceLeaf_of_ne {target replacement : SO} (h : traceLeaf ≠ target) : traceLeaf.replace target replacement = traceLeaf

The bare trace leaf, not being the target, is left unchanged.

Worked example

The copy-theory case: moving a daughter r out of [l r] and leaving a trace in its place yields [l′ t] (with l′ the recursively-substituted left daughter). The side-condition [l r] ≠ r always holds (a tree is never its own daughter; provable from weight via Subterm's immediatelyContains_lt_weight), taken as a hypothesis here to keep this module's dependencies minimal. Substitution is noncomputable, so this is a structural proof, not a decide.