Physlib.Mathematics.DataStructures.FourTree.Basic

The type `Leaf` is an inductive structure parametrized by a type $\alpha_4$ that contains a single value of type $\alpha_4$. It represents the terminal level of the hierarchical `FourTree` structure, which is designed to store nested data corresponding to the product type $\alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$.

For any type $\alpha_4$ that has decidable equality, the equality relation for the type $\text{Leaf}(\alpha_4)$ is also decidable. The $\text{Leaf}(\alpha_4)$ structure is a wrapper containing a single value of type $\alpha_4$, representing the terminal level of the hierarchical `FourTree` structure.

Given two types $\alpha_3$ and $\alpha_4$, a `Twig` is a data structure that consists of a value of type $\alpha_3$ and a multiset of elements of type `Leaf` $\alpha_4$.

Given types $\alpha_2$, $\alpha_3$, and $\alpha_4$, the `Branch` type represents a specific level within the `FourTree` hierarchical structure. An element of this type consists of a value of type $\alpha_2$ and a multiset of objects of type `Twig \alpha_3 \alpha_4`.

For any types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, a `Trunk` is a data structure that stores a value of type $\alpha_1$ and a multiset of `Branch` objects (which are parameterized by $\alpha_2, \alpha_3$, and $\alpha_4$). It represents the highest specific level within the `FourTree` hierarchical structure.

Given four types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, a `FourTree` is an inductive data structure defined as a multiset of `Trunk` elements. It is designed to store values of the product type $\alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ through a hierarchical tree structure: - A `Trunk` contains a value $a_1 \in \alpha_1$ and a multiset of `Branch` elements. - A `Branch` contains a value $a_2 \in \alpha_2$ and a multiset of `Twig` elements. - A `Twig` contains a value $a_3 \in \alpha_3$ and a multiset of `Leaf` elements. - A `Leaf` contains a value $a_4 \in \alpha_4$.

Given a type $\alpha_4$ that already has a defined string representation (an instance of the `Repr` class), this definition provides a string representation for the `Leaf` structure. For any leaf containing a value $v \in \alpha_4$, its representation is the string "leaf " followed by the string representation of $v$.

Given types $\alpha_3$ and $\alpha_4$ that have defined string representations (instances of the `Repr` class), this definition provides a string representation for the `Twig` structure. For any twig containing a value $v \in \alpha_3$ and a multiset of leaves $M$, its representation is the string "twig " followed by the string representation of $v$ and the string representation of $M$.

Given types $\alpha_2$, $\alpha_3$, and $\alpha_4$ that have defined string representations, this definition provides a string representation for the `Branch` structure. For any branch consisting of a value $x \in \alpha_2$ and a multiset of twigs $M$, its representation is the string "branch (" followed by the string representation of $x$, a closing parenthesis, and the string representation of $M$.

Given types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$ that possess string representations (instances of the `Repr` class), this definition provides a string representation for the `Trunk` structure. For any trunk node consisting of a value $x \in \alpha_1$ and a multiset of branches $M$, its representation is the string "trunk (" followed by the string representation of $x$, a closing parenthesis, and the string representation of $M$.

For types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$ that have defined string representations (instances of the `Repr` class), this definition provides a string representation for the `FourTree` structure. For a `FourTree` consisting of a multiset of trunks $S$, its representation is the string "root " followed by the string representation of the multiset $S$.

Given four types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$ with decidable equality, this function constructs a `FourTree` from a multiset $L$ of quadruples $(a_1, a_2, a_3, a_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$. The construction proceeds by hierarchically grouping and deduplicating the components of the tuples: 1. It identifies the set of unique values $a_1$ in $L$ to create the `Trunk` nodes. 2. For each $a_1$, it identifies the set of unique values $a_2$ such that $(a_1, a_2, a_3, a_4) \in L$ to create `Branch` nodes. 3. For each pair $(a_1, a_2)$, it identifies the set of unique values $a_3$ such that $(a_1, a_2, a_3, a_4) \in L$ to create `Twig` nodes. 4. For each triple $(a_1, a_2, a_3)$, it identifies the set of unique values $a_4$ such that $(a_1, a_2, a_3, a_4) \in L$ to create the terminal `Leaf` nodes. The resulting structure organizes the distinct quadruples present in the multiset into a nested hierarchy.

For types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, the function maps a `FourTree` $T$ to a multiset of quadruples $(a_1, a_2, a_3, a_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$. The multiset is constructed by traversing the hierarchical structure of $T$: for every value $a_1$ in a `Trunk`, every value $a_2$ in a `Branch` within that trunk, every value $a_3$ in a `Twig` within that branch, and every value $a_4$ in a `Leaf` within that twig, the tuple $(a_1, a_2, a_3, a_4)$ is collected into the resulting multiset.

Given a `Twig` $T$ consisting of a value of type $\alpha_3$ and a multiset of leaves of type $\alpha_4$, the cardinality of $T$ is defined as the number of elements in its multiset of leaves. If $T = (v, L)$ where $v \in \alpha_3$ and $L$ is a multiset of leaves, then the function returns $|L|$.

Given a `Branch` $T$ consisting of a value of type $\alpha_2$ and a multiset of twigs of type `Twig \alpha_3 \alpha_4`, the cardinality of $T$ is defined as the sum of the cardinalities of all twigs in its multiset. If $T = (v, S)$ where $v \in \alpha_2$ and $S$ is the multiset of twigs, the function returns $\sum_{t \in S} \text{card}(t)$, which corresponds to the total number of leaves contained within the branch.

Given a `Trunk` $T$ consisting of a value of type $\alpha_1$ and a multiset of branches $B$ (where each branch is of type `Branch α2 α3 α4`), the cardinality of $T$ is defined as the sum of the cardinalities of all branches in its multiset. If $T = (v, B)$ where $v \in \alpha_1$ and $B$ is the multiset of branches, the function returns $\sum_{b \in B} \text{card}(b)$. This sum corresponds to the total number of leaves contained within the hierarchical structure of the trunk.

Given a `FourTree` $T$ over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, which is defined as a multiset of trunks $S$, the cardinality of $T$ is the sum of the cardinalities of all trunks in $S$. Mathematically, $\text{card}(T) = \sum_{t \in S} \text{card}(t)$. This value represents the total number of leaves contained within the entire hierarchical structure of the tree.

For any `FourTree` $T$ over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, the cardinality of the tree $T$ is equal to the cardinality of the multiset of tuples $(a_1, a_2, a_3, a_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ obtained by converting $T$. That is, $\text{card}(T) = \text{card}(\text{toMultiset}(T))$.

For a leaf $T$ of type $\alpha_4$ that stores an underlying value $xs \in \alpha_4$, an element $x \in \alpha_4$ is defined to be a member of $T$ if and only if $x = xs$.

Given a type $\alpha_4$ with decidable equality, for any leaf $T$ storing a value $x_s \in \alpha_4$ and any element $x \in \alpha_4$, the proposition $x \in T$ (which is defined as $x = x_s$) is decidable.

Let $T$ be a `Twig` consisting of a value $x_s \in \alpha_3$ and a multiset of leaves $L$. An element $x = (x_1, x_2) \in \alpha_3 \times \alpha_4$ is defined to be a member of $T$ if and only if $x_s = x_1$ and there exists a leaf $l \in L$ such that $x_2$ is a member of $l$. In other words, membership requires the first component of the pair to match the Twig's data and the second component to be contained within one of its constituent leaves.

Given types $\alpha_3$ and $\alpha_4$ with decidable equality, for any twig $T$ (consisting of a value in $\alpha_3$ and a multiset of leaves of type $\alpha_4$) and any element $x \in \alpha_3 \times \alpha_4$, the proposition that $x$ is a member of $T$ is decidable. This is because the membership condition $x \in T$ requires checking the equality of the first components and the existence of a leaf in the multiset containing the second component, both of which are decidable properties.

Let $T$ be a `Branch` node consisting of a value $v \in \alpha_2$ and a multiset of twigs $\mathcal{T}$. An element $x = (x_1, x_2, x_3) \in \alpha_2 \times \alpha_3 \times \alpha_4$ is defined to be a member of $T$ if and only if $v = x_1$ and there exists a twig $t \in \mathcal{T}$ such that the pair $(x_2, x_3)$ is a member of $t$. In other words, membership requires the first component of the element to match the data stored in the branch and the remaining components to be contained within one of its constituent twigs.

Given types $\alpha_2, \alpha_3$, and $\alpha_4$ with decidable equality, for any branch $T$ (consisting of a value in $\alpha_2$ and a multiset of twigs) and any element $x \in \alpha_2 \times \alpha_3 \times \alpha_4$, the proposition that $x$ is a member of $T$ is decidable. This is because the membership condition $x \in T$ requires checking the equality of the first component of $x$ with the data stored in the branch and determining the existence of a twig in the multiset for which the remaining components $(x_2, x_3)$ form a member, both of which are decidable properties.

Let $T$ be a `Trunk` node consisting of a value $v \in \alpha_1$ and a multiset of branches $\mathcal{B}$. An element $x = (x_1, x_2, x_3, x_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ is defined to be a member of $T$ if and only if $v = x_1$ and there exists a branch $b \in \mathcal{B}$ such that the triple $(x_2, x_3, x_4)$ is a member of $b$ (according to the membership criterion for branches). In other words, membership requires the first component of the quadruple to match the data stored in the trunk and the remaining components to be contained within one of its constituent branches.

Given types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$ with decidable equality, for any trunk $T$ (consisting of a value in $\alpha_1$ and a multiset of branches) and any element $x \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$, the proposition that $x$ is a member of $T$ is decidable. This decidability follows from the fact that checking if the first component of $x$ matches the trunk's data is decidable, and checking the existence of a branch in the multiset that contains the remaining components $(x_2, x_3, x_4)$ is also decidable.

Let $T$ be a `FourTree` over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, which is structured as a multiset of `Trunk` elements. A quadruple $x = (x_1, x_2, x_3, x_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$ is defined to be a member of $T$ if there exists a trunk $t$ in the multiset such that $x$ is a member of $t$ (according to the membership criterion for trunks).

For any types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$ with decidable equality, given a `FourTree` $T$ and an element $x \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$, the proposition that $x$ is a member of $T$ (denoted `T.mem x`) is decidable. Since a `FourTree` is a multiset of trunks, this decidability is established by checking the existence of a trunk $t \in T$ such that $x$ is a member of $t$, a property which is itself decidable.

This instance defines the membership relation $\in$ for a `FourTree` $T$. For a quadruple $x = (x_1, x_2, x_3, x_4) \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$, the notation $x \in T$ represents the proposition that $x$ is contained within the hierarchical structure of $T$, which is composed of nested multisets of trunks, branches, twigs, and leaves.

For any types $\alpha_1, \alpha_2, \alpha_3, \alpha_4$ with decidable equality, given a `FourTree` $T$ and an element $x \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$, the proposition that $x$ is a member of $T$ (denoted $x \in T$) is decidable.

Let $T$ be a `FourTree` defined over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$, which hierarchically stores values of the product type $\alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$. For any quadruple $x \in \alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$, $x$ is a member of $T$ ($x \in T$) according to the recursive hierarchical membership criterion if and only if $x$ is an element of the multiset $T.\text{toMultiset}$ formed by collecting all tuples $(a_1, a_2, a_3, a_4)$ stored within the tree's trunks, branches, twigs, and leaves.

Let $T$ be a `FourTree` over types $\alpha_1, \alpha_2, \alpha_3$, and $\alpha_4$. Let $C = (a_1, a_2, a_3, a_4)$ be a quadruple in $\alpha_1 \times \alpha_2 \times \alpha_3 \times \alpha_4$. Suppose there exists: 1. a trunk $t$ in the multiset of trunks of $T$, 2. a branch $b$ in the multiset of branches of $t$, 3. a twig $w$ in the multiset of twigs of $b$, and 4. a leaf $l$ in the multiset of leaves of $w$. If $a_1, a_2, a_3$, and $a_4$ are the data values stored within $t, b, w,$ and $l$ respectively, then the quadruple $C$ is a member of the tree $T$ ($C \in T$).