Revision #3225 → #3776 · back to history
modifiedBinary tree68c41399a758
| Field | From #3225 | To #3776 |
|---|
| note | `Tree α` is the inductive type of binary trees with two children at each node, matching the Wikipedia notion. | `Tree α` (now a deprecated alias for `BinaryTree α`) is the inductive type of binary trees with at most two children per node. |
modifiedRecursive set-theoretic definition of binary tree028c6fbf9904
| Field | From #3225 | To #3776 |
|---|
| note | The inductive `Tree.nil | Tree.node a l r` is precisely the recursive constructor presentation of a binary tree. | The inductive `Tree.nil | Tree.node a l r` (alias of `BinaryTree`) is exactly the recursive constructor presentation. |
modifiedFull binary tree (recursive)f4a8b0b7b4d0
| Field | From #3225 | To #3776 |
|---|
| note | No definition of `FullBinaryTree` (every node has 0 or 2 children) exists in Mathlib. | No `FullBinaryTree`/`IsFull` predicate for binary trees (every node 0 or 2 children) exists in Mathlib. |
modifiedExtended binary tree (recursive)5ffb93a86ba7
| Field | From #3225 | To #3776 |
|---|
| note | Mathlib's `Tree` (with `nil` as external/empty node and `node` carrying two children) is precisely the extended binary tree. | Mathlib's `Tree`/`BinaryTree` (with `nil` as external node and `node` carrying two children) is precisely the extended binary tree. |
modifiedRooted binary tree35fb65419736
| Field | From #3225 | To #3776 |
|---|
| note | `Tree α` is rooted with at most two children per node, which is the Wikipedia rooted binary tree. | `Tree α`/`BinaryTree α` is rooted with at most two children per node. |
modifiedFull binary tree307ef024ab82
| Field | From #3225 | To #3776 |
|---|
| note | No predicate `IsFull`/`Tree.full` for binary trees with all internal nodes of degree 2 is present. | No predicate for binary trees with all internal nodes of degree 2 is present in Mathlib. |
modifiedInfinite complete binary tree9c1c7b5c0055
| Field | From #3225 | To #3776 |
|---|
| note | No formalization of the infinite complete binary tree (e.g., as `List Bool`) is provided as a named structure in Mathlib. | No named formalization of the infinite complete binary tree (e.g. `List Bool`) as such a structure is in Mathlib. |
modifiedBalanced binary tree1db9a47842e9
| Field | From #3225 | To #3776 |
|---|
| note | No height-balance predicate (AVL-style) on `Tree` is defined in Mathlib. | No height-balance (AVL-style) predicate on `Tree`/`BinaryTree` is defined in Mathlib. |
modifiedBounds on number of nodes in a full binary treebff27543e1ef
| Field | From #3225 | To #3776 |
|---|
| note | Bounds 2h+1 ≤ n ≤ 2^(h+1)−1 for full binary trees are not stated since `IsFull` itself isn't defined. | Bounds 2h+1 ≤ n ≤ 2^(h+1)−1 for full binary trees are not stated since no full-tree predicate is defined. |
modifiedLeaves vs. degree-2 nodes relation7310216632e8
| Field | From #3225 | To #3776 |
|---|
| mathlib.decl | BinaryTree.numLeaves_eq_numNodes_succ | Tree.numLeaves_eq_numNodes_succ |
| moderation_proposal.fields | — | {"mathlib":{"decl":"BinaryTree.numLeaves_eq_numNodes_succ","module":"Mathlib.Data.Tree.Basic","match_kind":"exact"}} |
| moderation_proposal.reason | — | `decl_exists` reports `Tree.numLeaves_eq_numNodes_succ` does not exist; the lemma lives under the current primary namespace `BinaryTree` (`Tree` is now only a deprecated type alias). |
| note | `numLeaves = numNodes + 1` is exactly the n0 = n2 + 1 identity under Mathlib's extended-tree convention where every `node` has two children and `nil` is a leaf. | `numLeaves = numNodes + 1` is exactly the n0 = n2 + 1 identity under Mathlib's extended-tree convention where every `node` has two children and `nil` is a leaf. Namespace corrected from `BinaryTree` to `Tree`. |
modifiedMinimum tree height for n nodes7748014f4479
| Field | From #3225 | To #3776 |
|---|
| mathlib.decl | BinaryTree.height_le_numNodes | Tree.height_le_numNodes |
| moderation_proposal.fields | — | {"mathlib":{"decl":"BinaryTree.height_le_numNodes","module":"Mathlib.Data.Tree.Basic","match_kind":"generalization"}} |
| moderation_proposal.reason | — | `decl_exists` reports `Tree.height_le_numNodes` does not exist; the lemma lives under the current primary namespace `BinaryTree`. |
| note | Only the upper bound `height ≤ numNodes` is provided; no lower bound `height ≥ ⌈log₂(n+1)⌉` is formalized. | Only the upper bound `height ≤ numNodes` is provided; no lower bound `height ≥ ⌈log₂(n+1)⌉` is formalized. Namespace corrected from `BinaryTree` to `Tree`. |
modifiedEdges versus nodes in a binary treee45b1758a2c1
| Field | From #3225 | To #3776 |
|---|
| note | Mathlib's `Tree` has no explicit edge-counting function, so the relation `e = n − 1` is not stated. | Mathlib's `Tree`/`BinaryTree` has no edge-counting function, so `e = n − 1` is not stated. |
modifiedNumber of null links18ae31f67f9f
| Field | From #3225 | To #3776 |
|---|
| mathlib.decl | BinaryTree.numLeaves_eq_numNodes_succ | Tree.numLeaves_eq_numNodes_succ |
| moderation_proposal.fields | — | {"mathlib":{"decl":"BinaryTree.numLeaves_eq_numNodes_succ","module":"Mathlib.Data.Tree.Basic","match_kind":"exact"}} |
| moderation_proposal.reason | — | `decl_exists` reports `Tree.numLeaves_eq_numNodes_succ` does not exist; the lemma lives under the current primary namespace `BinaryTree`. |
| note | Null links correspond to `nil` leaves in the extended representation, and `numLeaves = numNodes + 1` gives n + 1 null links. | Null links correspond to `nil` leaves in the extended representation, and `numLeaves = numNodes + 1` gives n + 1 null links. Namespace corrected from `BinaryTree` to `Tree`. |
modifiedCounting binary trees yields Catalan numbersccc70af1beab
| Field | From #3225 | To #3776 |
|---|
| mathlib.decl | BinaryTree.treesOfNumNodesEq_card_eq_catalan | Tree.treesOfNumNodesEq_card_eq_catalan |
| moderation_proposal.fields | — | {"mathlib":{"decl":"BinaryTree.treesOfNumNodesEq_card_eq_catalan","module":"Mathlib.Combinatorics.Enumerative.Catalan.Tree","match_kind":"exact"}} |
| moderation_proposal.reason | — | `decl_exists` reports `Tree.treesOfNumNodesEq_card_eq_catalan` does not exist; the theorem lives under the current primary namespace `BinaryTree`. |
| note | `#(treesOfNumNodesEq n) = catalan n` is the precise statement that binary trees with n internal nodes are counted by Catalan numbers. | `#(treesOfNumNodesEq n) = catalan n` is the precise statement that binary trees with n internal nodes are counted by Catalan numbers. Namespace corrected from `BinaryTree` to `Tree`. |
addedRecursive count of binary trees by size062e6e2492ed
modifiedBinary trees as free magma on a singleton4f6c25ae89fc
| Field | From #3225 | To #3776 |
|---|
| note | `FreeMagma α` exists with the comment that it can be viewed as labelled binary trees, but no explicit equivalence `FreeMagma Unit ≃ Tree Unit` (without `nil`) is proved. | `FreeMagma α` exists and is documented as labelled binary trees, but no explicit equivalence `FreeMagma Unit ≃ Tree Unit` (without `nil`) is proved. |
modifiedLeaf node insertionda06351e14e8
| Field | From #3225 | To #3776 |
|---|
| note | Mathlib's `Tree` API has no insertion-at-leaf operation. | Mathlib's `Tree`/`BinaryTree` API has no insertion-at-leaf operation. |
modifiedInternal node insertionb8238c613b23
| Field | From #3225 | To #3776 |
|---|
| note | No internal-node insertion operation is provided for `Tree`. | No internal-node insertion operation is provided for `Tree`/`BinaryTree`. |
modifiedDeletion of node with zero or one childreneea8d6fb8d84
| Field | From #3225 | To #3776 |
|---|
| note | No deletion operation for `Tree` nodes is defined in Mathlib. | No deletion operation for `Tree`/`BinaryTree` nodes is defined in Mathlib. |
modifiedPre-order traversalc79a4b8e7c6e
| Field | From #3225 | To #3776 |
|---|
| note | `Tree.traverse` visits node, then left, then right subtree (i.e. pre-order applicative traversal), but no named `Tree.preorderList`/`toListPreorder` function exists. | `Tree.traverse` (alias of `BinaryTree.traverse`) visits node, then left, then right subtree — the applicative pre-order traversal — but no named `toListPreorder` function exists. |
modifiedIn-order traversal4e6185a936b1
| Field | From #3225 | To #3776 |
|---|
| note | No in-order traversal of `Tree` is defined in Mathlib. | No in-order traversal of `Tree`/`BinaryTree` is defined in Mathlib. |
modifiedPost-order traversald3419b527f6c
| Field | From #3225 | To #3776 |
|---|
| note | No post-order traversal of `Tree` is defined in Mathlib. | No post-order traversal of `Tree`/`BinaryTree` is defined in Mathlib. |
modifiedDepth-first order2216b5601122
| Field | From #3225 | To #3776 |
|---|
| note | No DFS algorithm on `Tree` is formalized in Mathlib. | No DFS algorithm on `Tree`/`BinaryTree` is formalized in Mathlib. |
modifiedBreadth-first order509ea021cac7
| Field | From #3225 | To #3776 |
|---|
| note | No BFS traversal on `Tree` is formalized in Mathlib. | No BFS traversal on `Tree`/`BinaryTree` is formalized in Mathlib. |