The data type FourTree

We define a tree-like structure, called FourTree, for storing values of a type α1 × α2 × α3 × α4.

It is defined recursively, with the following structure:

• A leaf contains a value of type α4.
• A twig contains a value of type α3, and a multiset of leafs.
• A branch contains a value of type α2, and a multiset of twigs.
• A trunk contains a value of type α1, and a multiset of branchs.
• A FourTree contains a multiset of trunks.

inductive PhysLean.FourTree.Leaf (α4 : Type) : Type

A leaf contains has the data of a term of type α4.

• leaf {α4 : Type} : α4 → Leaf α4

instance PhysLean.FourTree.instDecidableEqLeaf {α4✝ : Type} [DecidableEq α4✝] : DecidableEq (Leaf α4✝)

Equations

• PhysLean.FourTree.instDecidableEqLeaf = PhysLean.FourTree.decEqLeaf✝

inductive PhysLean.FourTree.Twig (α3 α4 : Type) : Type

A twig has the data of a term of type α3 and a multiset of type Leaf α4.

• twig {α3 α4 : Type} : α3 → Multiset (Leaf α4) → Twig α3 α4

inductive PhysLean.FourTree.Branch (α2 α3 α4 : Type) : Type

A branch has the data of a term of type α2 and a multiset of type Twig α3 α4.

• branch {α2 α3 α4 : Type} : α2 → Multiset (Twig α3 α4) → Branch α2 α3 α4

inductive PhysLean.FourTree.Trunk (α1 α2 α3 α4 : Type) : Type

A trunk has the data of a term of type α1 and a multiset of type Branch α2 α3 α4.

• trunk {α1 α2 α3 α4 : Type} : α1 → Multiset (Branch α2 α3 α4) → Trunk α1 α2 α3 α4

inductive PhysLean.FourTree (α1 α2 α3 α4 : Type) : Type

A FourTree has the data of a multiset of type Trunk α1 α2 α3 α4.

• root {α1 α2 α3 α4 : Type} : Multiset (Trunk α1 α2 α3 α4) → FourTree α1 α2 α3 α4

Repr instances for the FourTree

These instances allow the FourTree to be printed in a human-readable format, and copied and pasted.

unsafe instance PhysLean.FourTree.instReprLeaf (α4 : Type) [Repr α4] : Repr (Leaf α4)

Equations

• One or more equations did not get rendered due to their size.

unsafe instance PhysLean.FourTree.instReprTwig (α3 α4 : Type) [Repr α3] [Repr α4] : Repr (Twig α3 α4)

Equations

• One or more equations did not get rendered due to their size.

unsafe instance PhysLean.FourTree.instReprBranch (α2 α3 α4 : Type) [Repr α2] [Repr α3] [Repr α4] : Repr (Branch α2 α3 α4)

Equations

• One or more equations did not get rendered due to their size.

unsafe instance PhysLean.FourTree.instReprTrunk (α1 α2 α3 α4 : Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] : Repr (Trunk α1 α2 α3 α4)

Equations

• One or more equations did not get rendered due to their size.

unsafe instance PhysLean.FourTree.instRepr (α1 α2 α3 α4 : Type) [Repr α1] [Repr α2] [Repr α3] [Repr α4] : Repr (FourTree α1 α2 α3 α4)

Equations

• One or more equations did not get rendered due to their size.

Conversion between FourTree and Multiset

def PhysLean.FourTree.fromMultiset {α1 α2 α3 α4 : Type} [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (l : Multiset (α1 × α2 × α3 × α4)) : FourTree α1 α2 α3 α4

A FourTree from a multiset of α1 × α2 × α3 × α4.

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.toMultiset {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : Multiset (α1 × α2 × α3 × α4)

A FourTree to a multiset of α1 × α2 × α3 × α4.

Equations

• One or more equations did not get rendered due to their size.

Cardinality of the tree

def PhysLean.FourTree.Twig.card {α3 α4 : Type} (T : Twig α3 α4) : ℕ

The cardinality of a Twig is the number of leafs.

Equations

• (PhysLean.FourTree.Twig.twig xs a).card = a.card

def PhysLean.FourTree.Branch.card {α2 α3 α4 : Type} (T : Branch α2 α3 α4) : ℕ

The cardinality of a Branch is the total number of leafs.

Equations

• (PhysLean.FourTree.Branch.branch xa a).card = (Multiset.map PhysLean.FourTree.Twig.card a).sum

def PhysLean.FourTree.Trunk.card {α1 α2 α3 α4 : Type} (T : Trunk α1 α2 α3 α4) : ℕ

The cardinality of a Trunk is the total number of leafs.

Equations

• (PhysLean.FourTree.Trunk.trunk xa a).card = (Multiset.map PhysLean.FourTree.Branch.card a).sum

def PhysLean.FourTree.card {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) : ℕ

The cardinality of a FourTree is the total number of leafs.

Equations

• (PhysLean.FourTree.root xs).card = (Multiset.map PhysLean.FourTree.Trunk.card xs).sum

theorem PhysLean.FourTree.card_eq_toMultiset_card {α1 α2 α3 α4s : Type} (T : FourTree α1 α2 α3 α4s) : T.card = T.toMultiset.card

Membership of a FourTree

Based on the tree structure we can define a faster membership criterion, which is equivalent to membership based on multisets.

def PhysLean.FourTree.Leaf.mem {α4 : Type} (T : Leaf α4) (x : α4) : Prop

An element of a : α4 is a member of Leaf α4 if the underlying element of the Leaf is a.

Equations

• (PhysLean.FourTree.Leaf.leaf xs).mem x = (xs = x)

instance PhysLean.FourTree.instDecidableMemOfDecidableEq {α4 : Type} [DecidableEq α4] (T : Leaf α4) (x : α4) : Decidable (T.mem x)

Equations

• One or more equations did not get rendered due to their size.

def PhysLean.FourTree.Twig.mem {α3 α4 : Type} (T : Twig α3 α4) (x : α3 × α4) : Prop

An element of a : α3 × α4 is a member of Twig α3 α4 if the underlying α3 element of the Twig is a.1 and a.2 is a member of one of the Leaf.

Equations

• (PhysLean.FourTree.Twig.twig xs a).mem x = (xs = x.1 ∧ ∃ leaf ∈ a, leaf.mem x.2)

instance PhysLean.FourTree.instDecidableMemOfDecidableEq_1 {α3 α4 : Type} [DecidableEq α3] [DecidableEq α4] (T : Twig α3 α4) (x : α3 × α4) : Decidable (T.mem x)

Equations

• PhysLean.FourTree.instDecidableMemOfDecidableEq_1 (PhysLean.FourTree.Twig.twig xs a) x = instDecidableAnd

def PhysLean.FourTree.Branch.mem {α2 α3 α4 : Type} (T : Branch α2 α3 α4) (x : α2 × α3 × α4) : Prop

An element of a : α2 × α3 × α4 is a member of Branch α2 α3 α4 if the underlying α2 element of the Branch is a.1 and a.2 is a member of one of the Twig.

Equations

• (PhysLean.FourTree.Branch.branch xa a).mem x = (xa = x.1 ∧ ∃ twig ∈ a, twig.mem x.2)

instance PhysLean.FourTree.instDecidableMemOfDecidableEq_2 {α2 α3 α4 : Type} [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : Branch α2 α3 α4) (x : α2 × α3 × α4) : Decidable (T.mem x)

Equations

• PhysLean.FourTree.instDecidableMemOfDecidableEq_2 (PhysLean.FourTree.Branch.branch xa a) x = instDecidableAnd

def PhysLean.FourTree.Trunk.mem {α1 α2 α3 α4 : Type} (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop

An element of a : α1 × α2 × α3 × α4 is a member of Trunk α1 α2 α3 α4 if the underlying α1 element of the Trunk is a.1 and a.2 is a member of one of the Branch.

Equations

• (PhysLean.FourTree.Trunk.trunk xa a).mem x = (xa = x.1 ∧ ∃ branch ∈ a, branch.mem x.2)

instance PhysLean.FourTree.instDecidableMemOfDecidableEq_3 {α1 α2 α3 α4 : Type} [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : Trunk α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x)

Equations

• PhysLean.FourTree.instDecidableMemOfDecidableEq_3 (PhysLean.FourTree.Trunk.trunk xa a) x = instDecidableAnd

def PhysLean.FourTree.mem {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Prop

An element of a : α1 × α2 × α3 × α4 is a member of FourTree α1 α2 α3 α4 if a is a member of one of the Trunk.

Equations

• (PhysLean.FourTree.root xs).mem x = ∃ trunk ∈ xs, trunk.mem x

instance PhysLean.FourTree.instDecidableMemOfDecidableEq_4 {α1 α2 α3 α4 : Type} [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (T.mem x)

Equations

• T.instDecidableMemOfDecidableEq_4 x = Multiset.decidableExistsMultiset

instance PhysLean.FourTree.instMembershipProd {α1 α2 α3 α4 : Type} : Membership (α1 × α2 × α3 × α4) (FourTree α1 α2 α3 α4)

Equations

• PhysLean.FourTree.instMembershipProd = { mem := PhysLean.FourTree.mem }

instance PhysLean.FourTree.instDecidableMemProdOfDecidableEq {α1 α2 α3 α4 : Type} [DecidableEq α1] [DecidableEq α2] [DecidableEq α3] [DecidableEq α4] (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : Decidable (x ∈ T)

Equations

• T.instDecidableMemProdOfDecidableEq x = Multiset.decidableExistsMultiset

theorem PhysLean.FourTree.mem_iff_mem_toMultiset {α1 α2 α3 α4 : Type} (T : FourTree α1 α2 α3 α4) (x : α1 × α2 × α3 × α4) : x ∈ T ↔ x ∈ T.toMultiset

theorem PhysLean.FourTree.mem_of_parts {α1 α2 α3 α4 : Type} {T : FourTree α1 α2 α3 α4} {C : α1 × α2 × α3 × α4} (trunk : Trunk α1 α2 α3 α4) (branch : Branch α2 α3 α4) (twig : Twig α3 α4) (leaf : Leaf α4) (trunk_mem : trunk ∈ T.1) (branch_mem : branch ∈ trunk.2) (twig_mem : twig ∈ branch.2) (leaf_mem : leaf ∈ twig.2) (heq : C = (trunk.1, branch.1, twig.1, leaf.1)) : C ∈ T