Decidable equality of nonplanar rose trees

Two rose trees represent the same nonplanar tree exactly when they are equal up to reordering the children of every vertex (RoseTree.Perm). This file shows that the relation is decidable, and computably so: the decision procedure reduces in the kernel, so concrete UnorderedTree equalities close by decide.

Main definitions

• RoseTree.eqv: Boolean comparison of two ordered trees up to child reordering — equal root values, and child lists matching as multisets under eqv (greedy matching).

Main results

• RoseTree.eqv_iff_perm: eqv decides Perm.
• RoseTree.instDecidableRelPerm: the resulting DecidableRel Perm.
• UnorderedTree.instDecidableEq: decidable equality on the quotient, via Quotient.decidableEq.

Implementation notes

eqv must recurse structurally for kernel reduction (decide needs brecOn, not WellFounded.fix), so the greedy matcher is inlined as eqv.go rather than passed to a list function. It finds each match with findIdx? and removes it with eraseIdx, evaluating eqv once per comparison, where the contains-then-erase shape of List.isPerm would evaluate it twice at every level of the tree.

List.isPerm_iff needs a lawful BEq on the whole type. go_iff needs eqv to compute mk-equality only on the pairs eqv.go compares, which is what the inductive hypothesis of eqv_iff_perm provides.

[UPSTREAM] candidate.

Deciding Perm: equality up to child reordering

def RoseTree.eqv {α : Type u_1} [DecidableEq α] : RoseTree α → RoseTree α → Bool

eqv t s decides whether t and s are equal up to child reordering (eqv_iff_perm).

Equations

• (RoseTree.node a cs).eqv (RoseTree.node b ds) = (decide (a = b) && RoseTree.eqv.go cs ds)

def RoseTree.eqv.go {α : Type u_1} [DecidableEq α] : List (RoseTree α) → List (RoseTree α) → Bool

Greedy matching of child lists, pairing each child of the first list with the first eqv-related child of the second still unmatched.

Equations

• RoseTree.eqv.go [] a✝ = a✝.isEmpty
• RoseTree.eqv.go (c :: cs) a✝ = match List.findIdx? c.eqv a✝ with | some i => RoseTree.eqv.go cs (a✝.eraseIdx i) | none => false

theorem RoseTree.eqv_iff_perm {α : Type u_1} [DecidableEq α] {t s : RoseTree α} : t.eqv s = true ↔ t.Perm s

Two ordered trees are eqv-related iff they are equal up to reordering the children of every vertex.

@[instance_reducible]

instance RoseTree.instDecidableRelPerm {α : Type u_1} [DecidableEq α] : DecidableRel Perm

Perm is decided by eqv, which reduces in the kernel.

Equations

• x✝¹.instDecidableRelPerm x✝ = decidable_of_iff (x✝¹.eqv x✝ = true) ⋯

@[instance_reducible]

instance RoseTree.instDecidableRelEquiv {α : Type u_1} [DecidableEq α] : DecidableRel fun (x1 x2 : RoseTree α) => x1 ≈ x2

Equations

• RoseTree.instDecidableRelEquiv = RoseTree.instDecidableRelPerm

@[instance_reducible]

instance UnorderedTree.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (UnorderedTree α)

Equality of nonplanar trees is decided by RoseTree.eqv on representatives (Quotient.decidableEq), so concrete UnorderedTree equalities close by decide.

Equations

• UnorderedTree.instDecidableEq = UnorderedTree.instDecidableEq._aux_1