inductive DecisionTree (n : ℕ) : Type

• leaf {n : ℕ} : Bool → DecisionTree n
• branch {n : ℕ} : Fin n → DecisionTree n → DecisionTree n → DecisionTree n

def instDecidableEqDecisionTree.decEq {n✝ : ℕ} (x✝ x✝¹ : DecisionTree n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqDecisionTree.decEq (DecisionTree.leaf a) (DecisionTree.leaf b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqDecisionTree.decEq (DecisionTree.leaf a) (DecisionTree.branch a_1 a_2 a_3) = isFalse ⋯
• instDecidableEqDecisionTree.decEq (DecisionTree.branch a a_1 a_2) (DecisionTree.leaf a_3) = isFalse ⋯

@[implicit_reducible]

instance instDecidableEqDecisionTree {n✝ : ℕ} : DecidableEq (DecisionTree n✝)

Equations

• instDecidableEqDecisionTree = instDecidableEqDecisionTree.decEq

def DecisionTree.evaluate {n : ℕ} : DecisionTree n → Vector Bool n → Bool

Equations

• (DecisionTree.leaf b).evaluate x✝ = b
• (DecisionTree.branch j l h).evaluate x✝ = if x✝[j] = true then h.evaluate x✝ else l.evaluate x✝

def DecisionTree.size {n : ℕ} : DecisionTree n → ℕ

Equations

• (DecisionTree.leaf a).size = 0
• (DecisionTree.branch a l h).size = 1 + l.size + h.size

inductive DecisionTree.usesVar {n : ℕ} (i : Fin n) : DecisionTree n → Prop

• here {n : ℕ} {i : Fin n} {x✝ x✝¹ : DecisionTree n} : usesVar i (branch i x✝ x✝¹)
• low {n : ℕ} {i x✝ : Fin n} {x✝¹ l : DecisionTree n} : usesVar i l → usesVar i (branch x✝ l x✝¹)
• high {n : ℕ} {i x✝ : Fin n} {x✝¹ h : DecisionTree n} : usesVar i h → usesVar i (branch x✝ x✝¹ h)

theorem DecisionTree.usesVar_iff {n : ℕ} (i : Fin n) (T : DecisionTree n) : usesVar i T ↔ ∃ (i' : Fin n), ∃ (l : DecisionTree n), ∃ (h : DecisionTree n), T = branch i' l h ∧ (i = i' ∨ usesVar i l ∨ usesVar i h)

def DecisionTree.lift {n n' : ℕ} : n ≤ n' → DecisionTree n → DecisionTree n'

Equations

• DecisionTree.lift x (DecisionTree.leaf b) = DecisionTree.leaf b
• DecisionTree.lift x (DecisionTree.branch j l h) = DecisionTree.branch ⟨↑j, ⋯⟩ (DecisionTree.lift x l) (DecisionTree.lift x h)

theorem DecisionTree.lift_injective {n n' : ℕ} {h : n ≤ n'} : Function.Injective (lift h)

theorem DecisionTree.lift_evaluate {n n' : ℕ} {h : n ≤ n'} {T : DecisionTree n} {I : Vector Bool n'} : (lift h T).evaluate I = T.evaluate (Vector.cast ⋯ (I.take n))

def DecisionTree.relabel {n : ℕ} {f : ℕ → ℕ} (hf : ∀ (i : Fin n), f ↑i < f n) : DecisionTree n → DecisionTree (f n)

Equations

• DecisionTree.relabel hf (DecisionTree.leaf a) = DecisionTree.leaf a
• DecisionTree.relabel hf (DecisionTree.branch a l h) = DecisionTree.branch ⟨f ↑a, ⋯⟩ (DecisionTree.relabel hf l) (DecisionTree.relabel hf h)

theorem DecisionTree.relabel_injective {n : ℕ} {T1 T2 : DecisionTree n} {f : ℕ → ℕ} {hf : ∀ (i : Fin n), f ↑i < f n} {h : ∀ (i i' : Fin n), usesVar i T1 → usesVar i' T2 → f ↑i = f ↑i' → i = i'} : relabel hf T1 = relabel hf T2 → T1 = T2