Documentation

Linglib.Syntax.Minimalist.SyntacticObject.Replace

Substitution on syntactic objects #

SyntacticObject.replace s target replacement substitutes every subterm of s equal to target by replacement; it is UnorderedTree.replace closed under well-formedness, which holds because substitution preserves the arity of every vertex. The copy-theory use is s.replace mover trace, leaving a trace where a mover was. This is a structural operation: the Merge-algebraic Internal Merge is the coproduct composition of Merge/Internal.lean, with traces as cut remainders and chains held at the workspace level, and replace supports the transformational view that study files are written in. It is noncomputable; concrete cases reduce by replace_self, replace_merge_of_ne, and the leaf lemmas.

Main definitions #

source
theorem Minimalist.isSyntacticObject_replace (target replacement s : SyntacticObject) :
IsSyntacticObject ((↑target).replace ↑replacement ↑s)

Substitution preserves well-formedness.

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

Replace every subterm of s equal to target by replacement.

Equations
  • s.replace target replacement = ⟨(↑target).replace ↑replacement ↑s, ⋯⟩
Instances For
    source
    @[simp]
    theorem Minimalist.SyntacticObject.replace_val (s target replacement : SyntacticObject) :
    ↑(s.replace target replacement) = (↑target).replace ↑replacement ↑s
    source
    @[simp]
    theorem Minimalist.SyntacticObject.replace_self (target replacement : SyntacticObject) :
    target.replace target replacement = replacement
    source
    theorem Minimalist.SyntacticObject.replace_merge_of_ne {l r target replacement : SyntacticObject} (h : l.merge r ≠ target) :
    (l.merge r).replace target replacement = (l.replace target replacement).merge (r.replace target replacement)

    At a node other than the target, substitution recurses into both daughters.

    source
    theorem Minimalist.SyntacticObject.replace_lexLeaf_of_ne {tok : LexicalItem.Token} {target replacement : SyntacticObject} (h : ↑tok ≠ target) :
    (↑tok).replace target replacement = ↑tok
    source
    theorem Minimalist.SyntacticObject.replace_traceLeaf_of_ne {target replacement : SyntacticObject} (h : trace ≠ target) :
    trace.replace target replacement = trace