Structural substitution on the SyntacticObject carrier

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

The intended copy-theory use is s.replace mover SyntacticObject.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, SyntacticObject.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 Perm-invariant and lifted, then closed under IsSO via SyntacticObject.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 : RoseTree.Nonplanar SOLabel) : RoseTree SOLabel → RoseTree.Nonplanar SOLabel

Structural substitution on a planar SyntacticObject-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 : RoseTree.Nonplanar SOLabel) : List (RoseTree SOLabel) → Multiset (RoseTree.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_perm (target replacement : RoseTree.Nonplanar SOLabel) {t s : RoseTree SOLabel} : t.Perm s → replacePlanar target replacement t = replacePlanar target replacement s

replacePlanar is Perm-invariant, so it descends to the quotient. At a node the if mk _ = target guard is fixed because mk is Perm-invariant (mk_eq_mk_iff), and the rebuilt child multiset by the PermList companion.

theorem Minimalist.replacePlanarList_permList (target replacement : RoseTree.Nonplanar SOLabel) {cs ds : List (RoseTree SOLabel)} : RoseTree.PermList cs ds → replacePlanarList target replacement cs = replacePlanarList target replacement ds

The rebuilt child multiset is PermList-invariant: it is built child-by-child, the List.Perm-style case split matching heads by the mutual replacePlanar_perm and reordering by Multiset.cons_swap.

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

Substitution lifted to the nonplanar carrier.

Equations

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

@[simp]

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

Reduction lemmas on leaves and bare binary nodes

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

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

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

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

IsSO closure and SyntacticObject.replace

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

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

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

Structural substitution on the SyntacticObject carrier ([MCB25] §1.2): replace every subterm of s equal to target by replacement. The copy-theory use is s.replace mover SyntacticObject.traceLeaf. Noncomputable (rebuilds via SyntacticObject.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.SyntacticObject.replace_val (s target replacement : SyntacticObject) : ↑(s.replace target replacement) = replaceN ↑target ↑replacement ↑s

@[simp]

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

Replacing the whole object by replacement.

theorem Minimalist.SyntacticObject.replace_node_of_ne {l r target replacement : SyntacticObject} (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.SyntacticObject.replace_lexLeaf_of_ne {tok : LIToken} {target replacement : SyntacticObject} (h : lexLeaf tok ≠ target) : (lexLeaf tok).replace target replacement = lexLeaf tok

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

theorem Minimalist.SyntacticObject.replace_traceLeaf_of_ne {target replacement : SyntacticObject} (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.