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.PermEquiv). This file shows that the relation is decidable, and computably so: the decision procedure reduces in the kernel, so concrete Nonplanar 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_permEquiv: eqv decides PermEquiv.
• RoseTree.instDecidableRelPermEquiv: the resulting DecidableRel PermEquiv.
• RootedTree.Nonplanar.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 calling the opaque List.isPermBy; go_eq_isPermBy reconnects them and imports the generic correctness from Core/Data/Multiset/Rel.lean.

[UPSTREAM] candidate.

Deciding PermEquiv: 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_permEquiv).

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 multiset matching of child lists: List.isPermBy eqv.

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

Correctness of the greedy matcher

eqv.go is List.isPermBy eqv, so the generic soundness and completeness of the greedy matcher (Core/Data/Multiset/Rel.lean) reduce eqv_iff_permEquiv to one size-bounded induction against mk-equality.

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

eqv decides PermEquiv: two ordered trees are eqv-related iff they are equal up to reordering the children of every vertex. Composite of eqv_iff_mk_eq (at a sum-of-sizes bound) with Nonplanar.mk_eq_mk_iff.

@[implicit_reducible]

instance RoseTree.instDecidableRelPermEquiv {α : Type u_1} [DecidableEq α] : DecidableRel PermEquiv

PermEquiv is decidable, computably so: decided by eqv, which reduces in the kernel.

Equations

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

@[implicit_reducible]

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

Equations

• RoseTree.instDecidableRelEquiv = RoseTree.instDecidableRelPermEquiv

@[implicit_reducible]

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

Equality of nonplanar trees — equality up to child reordering — is decidable and computable: Quotient.decidableEq over RoseTree.eqv on representatives, which reduces in the kernel, so concrete Nonplanar equalities close by decide.

Equations

• RootedTree.Nonplanar.instDecidableEq = RootedTree.Nonplanar.instDecidableEq._aux_1