Trees in lean

Stream: lean4

[Anton Mueller]

I nede to work with trees as below, unfortunately i did not find them in mathlib like this. Initially i tried to work with a type DIR containing middle, left and right as its sole values and then defined paths as List Dir. The current approach looks better to me, no overhead with adding arguments on correctness of paths etc.

The problem is with the set function: I have to include a pattern, which is unreachable. The sensible approach, having the first line as _, base => T' is not accepted: "Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern .(U)"

My question: Why does this not work, and where can i find implementations of trees which have comparable functionalities implemented, so that i can learn from these approaches?

Here an #mwe of what i have so far

set_option autoImplicit true

inductive Tree where
  | leaf (n : Nat)
  | scon (n : Nat) (T : Tree)
  | bcon (n  : Nat) (l r : Tree)
open Tree

inductive Path : Tree → Tree → Type
  | base  : Path t t
  | middle (p : Path t u) : Path (scon n t) u
  | left    (p : Path l u) : Path (bcon n l r) u
  | right  (p : Path r u) : Path (bcon n l r) u
open Path

def Tree.set (T : Tree) {U} (T' : Tree) (path : Path T U) : Tree :=
  match T, path with
    | leaf ann, base => T' -- why not _, base => T'
    | scon ann R, middle p => scon ann (set R T' p)
    | bcon ann l r, right p => bcon ann l (set r T' p)
    | bcon ann l r, left p => bcon ann (set l T' p) r
    | _, _ => T'

[Kim Morrison]

Did you see docs#Tree? This just sets the children to nil to represent your leaf or scon.

[Damiano Testa]

docs#Tree ? :slight_smile:

[Robin Arnez]

You can explicitly pull U into the match (which usually happens implicitly but it seems like at the wrong position):

inductive Tree where
  | leaf (n : Nat)
  | scon (n : Nat) (T : Tree)
  | bcon (n  : Nat) (l r : Tree)
open Tree

inductive Path : Tree → Tree → Type
  | base  : Path t t
  | middle (p : Path t u) : Path (scon n t) u
  | left    (p : Path l u) : Path (bcon n l r) u
  | right  (p : Path r u) : Path (bcon n l r) u

def Tree.set (T : Tree) {U} (T' : Tree) (path : Path T U) : Tree :=
  match T, U, path with
  | _, _, .base => T' -- why not _, base => T'
  | .scon ann R, _, .middle p => scon ann (set R T' p)
  | .bcon ann l r, _, .right p => bcon ann l (set r T' p)
  | .bcon ann l r, _, .left p => bcon ann (set l T' p) r

Why? idk

[Anton Mueller]

I already found docs#Tree, i did not find it particularly useful for my demands.

Concerning working with a more reduced set of constructors (i.e. deriving leaf and scon), but thought my approach to be more natural to deal with my problem.

What is missing from docs#Tree is just something that realizes pointers or something comparable, with which subtrees can be adressed and replaced (indexOf in ## Mathlib.Data.Tree.Get is the closest but totally not what i need)

[Anton Mueller]

Robin Arnez Great, thank you!