BinaryStructure.lean

1 import MachineTheory.HardSemantics
2 import Mathlib.Data.Nat.Log
3 import Mathlib.Data.Fintype.BigOperators
4 
5 /-!
6 # Binary structure of the existing literal controllers
7 
8 These are statistics of `HardInquiry.Tree`, not a replacement tree type. Optional
9 missing branches have no leaves and no records. Unary query nodes remain counted.
10 -/
11 namespace Komorebi.MachineTheory.BinaryDiagnosis
12 open HardInquiry Finset
13 variable {E C : Type}
14 
15 /-- Number of stored terminal occurrences, even when labels repeat. -/
16 def leaves : (h : ℕ) → Tree E Bool C h → ℕ
17   | 0, _ => 1
18   | _+1, .inl _ => 1
19   | h+1, .inr (_,k) => ((k false).map (leaves h)).getD 0 +
20       ((k true).map (leaves h)).getD 0
21 
22 /-- Actual query depth, rather than the horizon annotation. -/
23 def depth : (h : ℕ) → Tree E Bool C h → ℕ
24   | 0, _ => 0
25   | _+1, .inl _ => 0
26   | h+1, .inr (_,k) => 1 + max (((k false).map (depth h)).getD 0)
27       (((k true).map (depth h)).getD 0)
28 
29 /-- Number of internal nodes having exactly one stored child. -/
30 def unary : (h : ℕ) → Tree E Bool C h → ℕ
31   | 0, _ => 0
32   | _+1, .inl _ => 0
33   | h+1, .inr (_,k) =>
34       (if (k false).isSome != (k true).isSome then 1 else 0) +
35       ((k false).map (unary h)).getD 0 + ((k true).map (unary h)).getD 0
36 
37 /-- A query with no possible child is not a successful controller. -/
38 def Live : (h : ℕ) → Tree E Bool C h → Prop
39   | 0, _ => True
40   | _+1, .inl _ => True
41   | h+1, .inr (_,k) =>
42       (k false ≠ none ∨ k true ≠ none) ∧
43       (∀ o t, k o = some t → Live h t)
44 
45 theorem depth_le_horizon (h : ℕ) (t : Tree E Bool C h) : depth h t ≤ h := by
46   induction h with
47   | zero => rfl
48   | succ h ih =>
49     cases t with
50     | inl c => exact Nat.zero_le _
51     | inr ek =>
52       obtain ⟨e,k⟩ := ek
53       have hf : ((k false).map (depth h)).getD 0 ≤ h := by
54         cases he : k false with
55         | none => simp
56         | some s => simpa [he] using ih s
57       have ht : ((k true).map (depth h)).getD 0 ≤ h := by
58         cases he : k true with
59         | none => simp
60         | some s => simpa [he] using ih s
61       change 1 + max _ _ ≤ h+1
62       omega
63 
64 theorem leaves_le_pow_depth (h : ℕ) (t : Tree E Bool C h) :
65     leaves h t ≤ 2 ^ depth h t := by
66   induction h with
67   | zero => exact le_rfl
68   | succ h ih =>
69     cases t with
70     | inl c => exact le_rfl
71     | inr ek =>
72       obtain ⟨e,k⟩ := ek
73       have branch : ∀ o, ((k o).map (leaves h)).getD 0 ≤
74           2 ^ (((k o).map (depth h)).getD 0) := by
75         intro o
76         cases he : k o with
77         | none => simp
78         | some s => simpa [he] using ih s
79       have hf := (branch false).trans
80         (Nat.pow_le_pow_right (by decide : 0 < 2) (le_max_left _ (((k true).map (depth h)).getD 0)))
81       have ht := (branch true).trans
82         (Nat.pow_le_pow_right (by decide : 0 < 2) (le_max_right (((k false).map (depth h)).getD 0) _))
83       change _ + _ ≤ 2 ^ (1 + max _ _)
84       rw [Nat.add_comm 1, pow_succ]
85       omega
86 
87 /-- Exact edge accounting includes the extra record of every unary node. -/
88 theorem records_identity (h : ℕ) (t : Tree E Bool C h) (ht : Live h t) :
89     Model.records h t + 1 = 2 * leaves h t + unary h t := by
90   induction h with
91   | zero => rfl
92   | succ h ih =>
93     cases t with
94     | inl c => rfl
95     | inr ek =>
96       obtain ⟨e,k⟩ := ek
97       cases hf : k false with
98       | none =>
99         cases hg : k true with
100         | none =>
101           have := ht.1
102           simp only [hf,hg,ne_eq,not_true_eq_false,or_self] at this
103         | some r =>
104           have hr := ih r (ht.2 true r hg)
105           simp [Model.records,leaves,unary,hf,hg]
106           omega
107       | some l =>
108         have hl := ih l (ht.2 false l hf)
109         cases hg : k true with
110         | none =>
111           simp [Model.records,leaves,unary,hf,hg]
112           omega
113         | some r =>
114           have hr := ih r (ht.2 true r hg)
115           simp [Model.records,leaves,unary,hf,hg]
116           omega
117 
118 /-- Every successful leaf contributes twice, less the root edge. -/
119 theorem records_lower (h : ℕ) (t : Tree E Bool C h) (ht : Live h t) :
120     2 * leaves h t - 1 ≤ Model.records h t := by
121   have := records_identity h t ht
122   omega
123 
124 end Komorebi.MachineTheory.BinaryDiagnosis

Back to source controls