Subterm enumeration and containment for syntactic objects

[MCB25] §1.1–1.2. The containment / subterm theory of the SyntacticObject carrier, mirroring the legacy Basic.lean theory on FreeCommMagma (LIToken ⊕ Nat). Imports only the carrier skeleton (no Merge algebra).

Contents

• SyntacticObject.immediatelyContains — membership in the root children (via Nonplanar.rootChildren).
• SyntacticObject.subtrees/SyntacticObject.Acc — subterm enumeration (incl. root) and MCB's accessible terms Acc(T) (Def 1.2.2, root excluded).
• SyntacticObject.contains/isTermOf/containsOrEq — dominance and its reflexive/term-of variants.
• subtree ↔ containment bridges, and tree-relative c-command (cCommandsIn).

Immediate containment (via Nonplanar.rootChildren)

def Minimalist.SyntacticObject.immediatelyContains (x y : SyntacticObject) : Prop

x immediately contains y: y is one of x's root daughters ([MCB25] §1.1; Definition 13 of the legacy theory).

Equations

• x.immediatelyContains y = (↑y ∈ (↑x).rootChildren)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableImmediatelyContains (x y : SyntacticObject) : Decidable (x.immediatelyContains y)

Equations

• x.instDecidableImmediatelyContains y = Minimalist.SyntacticObject.instDecidableImmediatelyContains._aux_1 x y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_lexLeaf (tok : LIToken) (y : SyntacticObject) : ¬(lexLeaf tok).immediatelyContains y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_traceLeaf (y : SyntacticObject) : ¬traceLeaf.immediatelyContains y

@[simp]

theorem Minimalist.SyntacticObject.immediatelyContains_node (l r y : SyntacticObject) : (l.node r).immediatelyContains y ↔ y = l ∨ y = r

Subterm enumeration

Nonplanar.rootChildren is single-level, so deep enumeration is built fresh at the planar level and lifted. The result is a multiset of nonplanar subtrees; its Perm-invariance lets it descend to the quotient.

def Minimalist.subtreesNPlanar : RoseTree SOLabel → Multiset (RoseTree.Nonplanar SOLabel)

All subtrees of a planar tree (incl. the root), as nonplanar trees.

Equations

• Minimalist.subtreesNPlanar (RoseTree.node a cs) = RoseTree.Nonplanar.mk (RoseTree.node a cs) ::ₘ Minimalist.subtreesNPlanarList cs

def Minimalist.subtreesNPlanarList : List (RoseTree SOLabel) → Multiset (RoseTree.Nonplanar SOLabel)

Auxiliary: union of subtree-multisets across a child list.

Equations

• Minimalist.subtreesNPlanarList [] = 0
• Minimalist.subtreesNPlanarList (c :: cs) = Minimalist.subtreesNPlanar c + Minimalist.subtreesNPlanarList cs

theorem Minimalist.subtreesNPlanar_perm {t s : RoseTree SOLabel} : t.Perm s → subtreesNPlanar t = subtreesNPlanar s

subtreesNPlanar is Perm-invariant, so it descends to Nonplanar. At a node the root mk-image is fixed by mk_eq_mk_iff and the child-list sum by the PermList companion.

theorem Minimalist.subtreesNPlanarList_permList {cs ds : List (RoseTree SOLabel)} : RoseTree.PermList cs ds → subtreesNPlanarList cs = subtreesNPlanarList ds

The child-list subtree sum is PermList-invariant: it is a multiset sum, and the List.Perm-style case split matches heads by the mutual subtreesNPlanar_perm and reorders by add_left_comm.

def Minimalist.subtreesN : RoseTree.Nonplanar SOLabel → Multiset (RoseTree.Nonplanar SOLabel)

All subtrees of a nonplanar tree (incl. the root).

Equations

• Minimalist.subtreesN = RoseTree.Nonplanar.lift Minimalist.subtreesNPlanar ⋯

@[simp]

theorem Minimalist.subtreesN_mk (t : RoseTree SOLabel) : subtreesN (RoseTree.Nonplanar.mk t) = subtreesNPlanar t

theorem Minimalist.subtreesN_leaf (a : SOLabel) : subtreesN (RoseTree.Nonplanar.leaf a) = {RoseTree.Nonplanar.leaf a}

theorem Minimalist.subtreesN_node (a b : RoseTree.Nonplanar SOLabel) : subtreesN (RoseTree.Nonplanar.node (Sum.inr ()) {a, b}) = RoseTree.Nonplanar.node (Sum.inr ()) {a, b} ::ₘ (subtreesN a + subtreesN b)

subtreesN on a bare binary node: the node plus the subtrees of each child.

@[simp]

theorem Minimalist.mem_subtreesN_leaf {m : RoseTree.Nonplanar SOLabel} {a : SOLabel} : m ∈ subtreesN (RoseTree.Nonplanar.leaf a) ↔ m = RoseTree.Nonplanar.leaf a

Membership in subtreesN of a leaf.

@[simp]

theorem Minimalist.mem_subtreesN_node {m a b : RoseTree.Nonplanar SOLabel} : m ∈ subtreesN (RoseTree.Nonplanar.node (Sum.inr ()) {a, b}) ↔ m = RoseTree.Nonplanar.node (Sum.inr ()) {a, b} ∨ m ∈ subtreesN a ∨ m ∈ subtreesN b

Membership in subtreesN of a bare binary node.

theorem Minimalist.self_mem_subtreesN (u : RoseTree.Nonplanar SOLabel) : u ∈ subtreesN u

Every nonplanar tree is among its own subtrees.

SyntacticObject.subtrees / SyntacticObject.Acc

theorem Minimalist.subtreesN_closure (s : SyntacticObject) (m : RoseTree.Nonplanar SOLabel) : m ∈ subtreesN ↑s → IsSO m

Subtrees of a syntactic object are themselves syntactic objects.

def Minimalist.SyntacticObject.subtrees (s : SyntacticObject) : Multiset SyntacticObject

All subtrees of a syntactic object (incl. the root), as syntactic objects ([MCB25] §1.2; the legacy SyntacticObject.subtrees).

Equations

• s.subtrees = Multiset.pmap (fun (m : RoseTree.Nonplanar Minimalist.SOLabel) (h : Minimalist.IsSO m) => ⟨m, h⟩) (Minimalist.subtreesN ↑s) ⋯

@[simp]

theorem Minimalist.SyntacticObject.mem_subtrees {x s : SyntacticObject} : x ∈ s.subtrees ↔ ↑x ∈ subtreesN ↑s

theorem Minimalist.SyntacticObject.self_mem_subtrees (s : SyntacticObject) : s ∈ s.subtrees

The root is among its own subtrees.

@[simp]

theorem Minimalist.SyntacticObject.mem_subtrees_node {x l r : SyntacticObject} : x ∈ (l.node r).subtrees ↔ x = l.node r ∨ x ∈ l.subtrees ∨ x ∈ r.subtrees

Subtree membership at a bare binary node: the node itself, or a subtree of a daughter.

theorem Minimalist.SyntacticObject.subtrees_subset_of_mem {w s : SyntacticObject} (h : w ∈ s.subtrees) : w.subtrees ⊆ s.subtrees

subtrees is downward-closed along the subtree relation: every subtree of a subtree of s is a subtree of s.

Cardinality (MCB's vertex/accessible-term counts, Def 1.2.2 eq. 1.2.5)

theorem Minimalist.subtreesNPlanar_card (p : RoseTree SOLabel) : (subtreesNPlanar p).card = p.numNodes

subtreesN has one element per vertex: its cardinality is the node count.

theorem Minimalist.subtreesNPlanarList_card (cs : List (RoseTree SOLabel)) : (subtreesNPlanarList cs).card = (List.map RoseTree.numNodes cs).sum

Auxiliary list version.

theorem Minimalist.subtreesN_card (u : RoseTree.Nonplanar SOLabel) : (subtreesN u).card = u.numNodes

theorem Minimalist.SyntacticObject.subtrees_card (s : SyntacticObject) : s.subtrees.card = (↑s).numNodes

subtrees enumerates the vertices ([MCB25] Def 1.2.2: subtrees = Acc'(T), so its size is #V(T), the MCB workspace-size primitive).

Accessible terms Acc(T) (Def 1.2.2)

def Minimalist.SyntacticObject.Acc (s : SyntacticObject) : Multiset SyntacticObject

MCB's accessible-terms operator Acc(T) ([MCB25] Def 1.2.2, eq. 1.2.2): the subtrees at all non-root vertices (leaves included — the counting identity eq. 1.2.5 #V = b₀ + #Acc forces this). Defined as subtrees − {self} (Acc'(T) = {T} ∪ Acc(T), eq. 1.2.3).

Equations

• s.Acc = s.subtrees - {s}

theorem Minimalist.SyntacticObject.Acc_card (s : SyntacticObject) : s.Acc.card = (↑s).numNodes - 1

MCB counting identity (eq. 1.2.5, one-component case): #Acc(T) = #V(T) − 1.

@[simp]

theorem Minimalist.SyntacticObject.Acc_lexLeaf (tok : LIToken) : (lexLeaf tok).Acc = 0

@[simp]

theorem Minimalist.SyntacticObject.Acc_traceLeaf : traceLeaf.Acc = 0

Containment / dominance

theorem Minimalist.weight_node_pair (a b : RoseTree.Nonplanar SOLabel) : (RoseTree.Nonplanar.node (Sum.inr ()) {a, b}).numNodes = a.numNodes + b.numNodes + 1

Weight of a bare binary node is one more than the sum of its daughters'.

inductive Minimalist.SyntacticObject.contains : SyntacticObject → SyntacticObject → Prop

Containment (dominance) is the transitive closure of immediate containment ([MCB25] §1.1; the legacy contains).

• imm (x y : SyntacticObject) : x.immediatelyContains y → x.contains y
• trans (x y z : SyntacticObject) : x.immediatelyContains z → z.contains y → x.contains y

theorem Minimalist.SyntacticObject.imm_implies_contains {x y : SyntacticObject} (h : x.immediatelyContains y) : x.contains y

theorem Minimalist.SyntacticObject.contains_trans {x y z : SyntacticObject} (hxy : x.contains y) (hyz : y.contains z) : x.contains z

theorem Minimalist.SyntacticObject.immediatelyContains_lt_weight {x y : SyntacticObject} (h : x.immediatelyContains y) : (↑y).numNodes < (↑x).numNodes

Immediate containment strictly decreases weight.

theorem Minimalist.SyntacticObject.contains_lt_weight {x y : SyntacticObject} (h : x.contains y) : (↑y).numNodes < (↑x).numNodes

Containment strictly decreases weight; hence it is irreflexive.

theorem Minimalist.SyntacticObject.contains_irrefl (x : SyntacticObject) : ¬x.contains x

Subtree ↔ containment bridge

theorem Minimalist.SyntacticObject.mem_subtrees_of_immediatelyContains {x y : SyntacticObject} (h : x.immediatelyContains y) : y ∈ x.subtrees

theorem Minimalist.SyntacticObject.mem_subtrees_of_contains {x y : SyntacticObject} (h : x.contains y) : y ∈ x.subtrees

theorem Minimalist.SyntacticObject.mem_subtrees_iff_eq_or_contains {x y : SyntacticObject} : y ∈ x.subtrees ↔ y = x ∨ x.contains y

A subtree of x is either x itself or properly contained in x.

theorem Minimalist.SyntacticObject.contains_iff_mem_subtrees_and_ne {x y : SyntacticObject} : x.contains y ↔ y ∈ x.subtrees ∧ y ≠ x

Containment ↔ proper subtree membership. Gives a decision procedure for contains without well-founded recursion: y is properly contained in x iff it is a subtree distinct from x.

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableContains (x y : SyntacticObject) : Decidable (x.contains y)

Equations

• x.instDecidableContains y = decidable_of_iff (y ∈ x.subtrees ∧ y ≠ x) ⋯

Term-of and reflexive containment

def Minimalist.SyntacticObject.isTermOf (x y : SyntacticObject) : Prop

x is a term of y: x = y or y contains x.

Equations

• x.isTermOf y = (x = y ∨ y.contains x)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableIsTermOf (x y : SyntacticObject) : Decidable (x.isTermOf y)

Equations

• x.instDecidableIsTermOf y = Minimalist.SyntacticObject.instDecidableIsTermOf._aux_1 x y

theorem Minimalist.SyntacticObject.isTermOf_iff_mem_subtrees (x y : SyntacticObject) : x.isTermOf y ↔ x ∈ y.subtrees

def Minimalist.SyntacticObject.containsOrEq (x y : SyntacticObject) : Prop

Reflexive containment.

Equations

• x.containsOrEq y = (x = y ∨ x.contains y)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableContainsOrEq (x y : SyntacticObject) : Decidable (x.containsOrEq y)

Equations

• x.instDecidableContainsOrEq y = Minimalist.SyntacticObject.instDecidableContainsOrEq._aux_1 x y

theorem Minimalist.SyntacticObject.containsOrEq_trans {x y z : SyntacticObject} (hxy : x.containsOrEq y) (hyz : y.containsOrEq z) : x.containsOrEq z

RoseTree-relative c-command ([Rei76])

def Minimalist.SyntacticObject.areSistersIn (root x y : SyntacticObject) : Prop

x and y are sisters in root: distinct co-daughters of some subtree.

Equations

• root.areSistersIn x y = ∃ z ∈ root.subtrees, z.immediatelyContains x ∧ z.immediatelyContains y ∧ x ≠ y

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableAreSistersIn (root x y : SyntacticObject) : Decidable (root.areSistersIn x y)

Equations

• root.instDecidableAreSistersIn x y = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.cCommandsIn (root x y : SyntacticObject) : Prop

x c-commands y in root: x has a sister (in root) that contains-or-equals y.

Equations

• root.cCommandsIn x y = ∃ z ∈ root.subtrees, root.areSistersIn x z ∧ z.containsOrEq y

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableCCommandsIn (root x y : SyntacticObject) : Decidable (root.cCommandsIn x y)

Equations

• root.instDecidableCCommandsIn x y = Multiset.decidableExistsMultiset

def Minimalist.SyntacticObject.asymCCommandsIn (root x y : SyntacticObject) : Prop

x asymmetrically c-commands y in root.

Equations

• root.asymCCommandsIn x y = (root.cCommandsIn x y ∧ ¬root.cCommandsIn y x)

@[instance_reducible]

instance Minimalist.SyntacticObject.instDecidableAsymCCommandsIn (root x y : SyntacticObject) : Decidable (root.asymCCommandsIn x y)

Equations

• root.instDecidableAsymCCommandsIn x y = Minimalist.SyntacticObject.instDecidableAsymCCommandsIn._aux_1 root x y

decide demonstrations

The containment / c-command decision procedures reduce on concrete trees built via Nonplanar.mk ∘ RoseTree.node (not the noncomputable SyntacticObject.node), confirming the "state result trees directly" discipline carries through to the relational layer.