rooted trees

Stream: Is there code for X?

[Daniel Weber]

Do we have rooted trees in Mathlib? I'm interested in formalizing Kruskal's tree theorem

[Yaël Dillies]

No we do not

[Daniel Weber]

What would be the best way to define it?

import Mathlib.Data.Multiset.Basic

inductive RootedTree.{u} : Type u → Type u
| nil : {α : Type u} → RootedTree α
| node : {α : Type u} → (Multiset (α × RootedTree α)) → RootedTree α

makes the kernel complain, and is also restricted to finite trees (which is fine for Kruskal's theorem, but something more generic might be better for Mathlib). It's possible to make this from docs#SimpleGraph.IsTree, but I fear it would be annoying to work with

[Daniel Weber]

Or perhaps docs#PredOrder could be used as a base?

[Daniel Weber]

Actually, isn't a PredOrder with an OrderBot exactly a rooted tree?

[Yaël Dillies]

It is, yes (at least so long as you don't care about infinite dangling bits). But from your description it's not very clear how exactly you want to manipulate rooted trees

[Daniel Weber]

I'm not quite sure yet, but I'm looking for something which could eventually be added to Mathlib. Looking at it like an order does seem promising, though - a tree homeomorphism is an injective docs#InfHom, for instance, if I'm not mistaken

[Daniel Weber]

To exclude infinite dangling bits you can just add docs#LocallyFiniteOrder, right?

[Yaël Dillies]

... or docs#IsPredArchimedean

[Daniel Weber]

Oh, I didn't notice it's only about comparable elements

[Daniel Weber]

Although I do need to look at subtrees, and I'm not sure how nice that is with orders

[Yaël Dillies]

Ici a should be the subtree rooted at a

[Daniel Weber]

Yes, but that's a set

[Yaël Dillies]

Sure, but it can be coerced to a type with PredOrder (Ici a) and IsPredArchimedean (Ici a)

[Daniel Weber]

Hmm. I'll try to prove Kruskal's theorem with this

[Yaël Dillies]

Again, "look at subtrees" could mean

1. Needing to construct a subtree
2. Stating that an existing object is a subtree
3. Considering the overall collection of subtrees
4. etc...

and it's really hard for me to help you if you don't tell me which one(s) you are after

[Daniel Weber]

I think the main things I need to do with subtrees are

1. look at the set of (immediate) subtrees of a Fintype tree as a Finset (or maybe Multiset, it depends on how tree equality is defined) of trees, let's call this subtrees t
2. I have a function f : subtrees a → subtrees b and a function g : (s : subtrees a) → s → f s and I need to extend it to a function a → b by mapping the root to the root, and mapping other elements using g for their subtree I think this is just finding the subtree a non-root element is contained in

[Yaël Dillies]

Okay so in the paradigm I'm offering the immediate subtrees would be indexed by the atoms of the order, which might be convenient enough?

[Daniel Weber]

I want to talk about sequences of trees, so I think it would be best if everything was bundled, right?

[Daniel Weber]

To find the subtree of an element I can use docs#IsPredArchimedean with bot and apply pred n-1 times, would that work well?

[Andrew Yang]

The subtrees are just Set.Ici '' Set.Iic x I think.

[Yaël Dillies]

Daniel Weber said:

I want to talk about sequences of trees, so I think it would be best if everything was bundled, right?

Sequences of trees, or sequences of subtrees?

[Daniel Weber]

Sequences of trees

[Daniel Weber]

Do I need DecidableEq α to define Set.Ici.predOrder, or is there a way to avoid it?

[Yaël Dillies]

Yes, I would think you need it

[Daniel Weber]

I'm almost done with the proof, but there's a problem with my definition of Tree.subtrees - I want all of thoseTrees to be different, but they are types, so their equality doesn't behave nicely at all. What's a good alternative way to do that?

import Mathlib

structure RootedTree where
  α : Type*
  [order : SemilatticeInf α]
  [bot : OrderBot α]
  [pred : PredOrder α]
  [pred_archimedean : IsPredArchimedean α]

instance coeSort : CoeSort RootedTree (Type*) := ⟨RootedTree.α⟩

variable (t : RootedTree) (r : t)

instance : SemilatticeInf t := t.order
instance : PredOrder t := t.pred
instance : OrderBot t := t.bot
instance : IsPredArchimedean t := t.pred_archimedean

instance Set.Ici.predOrder {α : Type*} [DecidableEq α] [PartialOrder α] [PredOrder α] {a : α} : PredOrder (Set.Ici a) := sorry

instance Set.Ici.isPredArchimedean {α : Type*} [DecidableEq α] [PartialOrder α] [PredOrder α]
    [IsPredArchimedean α] {a : α} : IsPredArchimedean (Set.Ici a) := sorry

def RootedTree.subtree (t : RootedTree) [DecidableEq t] (r : t) : RootedTree where
  α := Set.Ici r

def RootedTree.subtrees [DecidableEq t] : Set RootedTree :=
  t.subtree '' {x | IsAtom x}

[Yaël Dillies]

You could force α to be of the form Fin n for some n

[Daniel Weber]

How would that help? I want all of the subtrees to appear in the set, without some getting deduplicated

[Daniel Weber]

I can use {x // IsAtom x} → RootedTree in place of Set, but I'm not sure how convenient that is

[Daniel Weber]

I think I settled on defining a type synonym SubRootedTree, and then I define

instance [DecidableEq t] : CoeOut (SubRootedTree t) RootedTree where
  coe r := {
    α := Set.Ici r.root
  }

but it delaborates weirdly - #check (t.subtree r : RootedTree) prints RootedTree.mk ↑(Set.Ici (t.subtree r).root) : RootedTree instead of ↑(t.subtree r) : RootedTree. How can I fix this?

[Daniel Weber]

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.RootedTree.mk]
def delabRTMk : Delab := do
  let e ← getExpr
  guard <| e.isAppOfArity' ``RootedTree.mk 5
  guard <| (e.getArg!' 0).isAppOfArity' ``Set.Elem 2
  guard <| ((e.getArg!' 0).getArg!' 1).isAppOfArity' ``Set.Ici 3
  let arg ← withAppArg (withAppArg delab)
  `(↑$arg)

seems to work, I couldn't get an unexpander working there for some reason

[Yaël Dillies]

abbrev coe (r : SubRootedTree t) : RootedTree where  α := Set.Ici r.root

instance [DecidableEq t] : CoeOut (SubRootedTree t) RootedTree where
  coe := coe

should do

[Daniel Weber]

That works, thanks Now it writes coe t (t.subtree r)

[Daniel Weber]

I'm having a problem with handling subtrees - I define

instance [DecidableEq t] : CoeOut (SubRootedTree t) RootedTree where
  coe r := {
    α := Set.Ici r.root
  }

instance [DecidableEq t] (r : SubRootedTree t) : CoeOut r t where
  coe := Subtype.val

def RootedTree.subtrees [DecidableEq t] : Set <| SubRootedTree t :=
  {x | IsAtom x.root}

def RootedTree.subtreeOf [DecidableEq t] (r : t) (hr : r ≠ ⊥) : t.subtrees := sorry

def RootedTree.mem_subtreeOf [DecidableEq t] (r : t) (hr : r ≠ ⊥) : ↑(t.subtreeOf r hr) :=
  ⟨r, sorry⟩

and now I have an embedding f : a.subtrees ↪ b.subtrees and a function g : (t : a.subtrees) → t ↪ (f t), and I define a function by
g' (x : a) : b := if h : x = ⊥ then ⊥ else g (a.subtreeOf x h) (a.mem_subtreeOf x h)
now I need to show that this g' is injective, but when neither x or y are the root and g' x = g' y, I can show that the subtrees are equal (apply subtreeOf, show this gives f (a.subtreeOf x h1) = f (a.subtreeOf y h2) and apply f's injectivity), but I can't rewrite with that equality because they're types. What's a better way to handle all of this?

[Daniel Weber]

I think changing g to a.subtrees -> a -> b (filling everything irrelevant with junk values) and using docs#Set.InjOn and docs#Set.MapsTo could work

[Notification Bot]

33 messages were moved from this topic to #mathlib4 > weaker SuccOrder/PredOrder by Floris van Doorn.

[Daniel Weber]

A rooted tree (PredOrder + IsPredArchimedean + OrderBot) is uniquely an InfSemilattice where inf is the LCA in the tree. What's the proper way to state this result?

[Yaël Dillies]

abbrev PredOrder.toSemilatticeInf [PredOrder α] [IsPredArchimedean α] [OrderBot α] : SemilatticeInf α

[Daniel Weber]

Couldn't that cause defeqness issues if there's already a SemilatticeInf instance, as it's data?

[Yaël Dillies]

No, because abbrev too is data

[Daniel Weber]

I made a PR defining rooted trees, #16272