[Merged by Bors] - feat(data/tree): Add definitions about binary trees; special support for tree unit

[prakol16]

Provide convenience API for tree unit. In particular, define a recursor for tree unit as well as other helper lemmas.

In addition, define common functions on binary trees such as nodes, num_leaves, height, and prove basic lemmas about these functions, such as the fact that the number of leaves is one more than the number of internal nodes and the height is at most the number of nodes.

---

Moving part of #16415 into its own PR, so that the catalan PR, which doesn't need to know anything about encodings, can proceed faster.

[YaelDillies]

Can you use tree punit rather than defining a new inductive type? If you want simpler constructors (that is, not having to give an element of punit every time), you can still provide them as API.

[prakol16]

Can you use tree punit rather than defining a new inductive type? If you want simpler constructors (that is, not having to give an element of punit every time), you can still provide them as API.

The reason I initially decided against it was because the use case in #16415 is to allow encodings to trees. The encoding of unit_tree should be id, whereas the polymorphic encoding of tree α based on α is probably different.

There were also minor annoyances with having some a : unit types in proofs and have to explicitly add unit_eq_star as a simp lemma every time, or call cases a where a : unit. This occurs sometimes when simp does not generate the most general form of a lemma e.g.

@[simp] def something : tree unit -> α
| tree.nil := /- something -/
| (tree.node () x y) := /- something -/

generates a simp lemma which only simplifies something (tree.node a x y) when the argument is explicitly () (rather than just a : unit). On the other hand, induction does not automatically call cases on unit types.

[YaelDillies]

This all sounds like things you can solve using a new recursor.

[YaelDillies]

I'm fine with this PR but I would like another reviewer's opinion.

[YaelDillies]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[alreadydone]

it's been two months so we should probably merge master first

[Vierkantor]

Sorry for the long wait!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests