Documentation

Bdd.DecisionTree

inductive DecisionTree (n : ℕ) :

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

Instances For

instance instDecidableEqDecisionTree {n✝ : ℕ} :

DecidableEq (DecisionTree n✝)

Equations

instDecidableEqDecisionTree = decEqDecisionTree✝

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✝

Instances For

def DecisionTree.size {n : ℕ} :

DecisionTree n → ℕ

Equations

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

Instances For

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)

Instances For

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)

Instances For

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)

Instances For

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