Huffman Tree

Stream: new members

[Sébastien Boisgérault]

Hello everyone,

Is the following code (that Lean 4 rejects) "patchable" or is there a fundamental limitation there that I should know about? If that's the case, what would be the idiomatic way to define a tree where only the terminal leaves can carry a (String) payload?

inductive Tree where
  | nil : Tree
  | leaf
      (string? : Option String)
      (left : Tree)
      (right : Tree)
      (check : string?.isSome → (left = Tree.nil) ∧ (right = Tree.nil)) :
      Tree

[Sébastien Boisgérault]

FYI, the top-level error is:

(kernel) invalid nested inductive datatype 'And', nested inductive datatypes parameters cannot contain local variables.

[Damiano Testa]

Would what is below work for you?

inductive Tree where
  | leaf (s : String) : Tree
  | node (left right : Tree) : Tree

[Eric Wieser]

Or if you also want the string to be optional on leaf nodes (as in your original)

inductive Tree where
  | nil : Tree
  | leaf (s : String) : Tree
  | node (left right : Tree) : Tree

or more simply

inductive Tree where
  | leaf (s : Option String) : Tree
  | node (left right : Tree) : Tree

[Sébastien Boisgérault]

Damiano Testa said:

Would what is below work for you?

inductive Tree where
  | leaf (s : String) : Tree
  | node (left right : Tree) : Tree

In this model, you cannot have a leaf that has a single non-nil child right? A tree that has for example a single "left" leave that holds a String should be valid.

[Damiano Testa]

Yes, the model that I suggested does not allow what you want. But Eric's seems to:

inductive Tree where
  | nil : Tree
  | leaf (s : String) : Tree
  | node (left right : Tree) : Tree

#check Tree.node (Tree.leaf "") Tree.nil

[Sébastien Boisgérault]

I think that there are two issues here:

- I have not really thought about the existence of a simple "classic" ADT model, correct by construction for my context, thank you for pushing me to revisit this. :pray:

- But I was also a little surprised for not being able to simply embed extra constraints in the definition of inductive types, since when I do that with structs, that usually works without effort (e.g. to define a rational number whose denominator is non-zero). And therefore I'd also appreciate knowing more about what the technical issue is behind the original design (forgetting for a moment that it is unnecessarily complicated).

Any pointer would be appreciated!

[Damiano Testa]

I don't know how to impose such constraints. I am also not sure whether it is possible or not.

[Eric Wieser]

Here's one way to impose constraints:

inductive Tree : Bool → Type where
  | nil : Tree true
  | leaf
      (string? : Option String)
      {lisNil risNil}
      (left : Tree lisNil)
      (right : Tree risNil)
      (check : string?.isSome → lisNil ∧ risNil) :
      Tree false

[Eric Wieser]

I wouldn't recommend using that here, but it perhaps shows you another tool that is available

[Sébastien Boisgérault]

Eric Wieser said:

I wouldn't recommend using that here, but it perhaps shows you another tool that is available

Agreed. :praise: Thanks a lot for this method!