DeflateRunSupport.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«trees.c.runs»
2
3/-! # Positive-length symbols in the existing run-length model
4
5These heap-free lemmas use the unchanged run model shared by the checked
6scan and the forthcoming output proof. They introduce no execution contract.
7-/
8
9namespace Zlib.Trees.Proofs.Out
10
11theorem runStep_done_prev (L : Nat → Nat) (n : Nat) (s : RunSt)
12    (ha : ¬ (s.cnt + 1 < s.mx ∧ s.next = L (n + 1))) :
13    (runStep L n s).1.prev = s.next := by
14  simp only [runStep, ite_eq_right ha]
15  split
16  · rfl
17  · split <;> rfl
18
19theorem runStep_done_cnt (L : Nat → Nat) (n : Nat) (s : RunSt)
20    (ha : ¬ (s.cnt + 1 < s.mx ∧ s.next = L (n + 1))) :
21    (runStep L n s).1.cnt = 0 := by
22  simp only [runStep, ite_eq_right ha]
23  split
24  · rfl
25  · split <;> rfl
26
27theorem scanFreq_le_next (L : Nat → Nat) (n k : Nat) :
28    scanFreqUpTo L n k ≤ scanFreqUpTo L (n + 1) k := by
29  simp only [scanFreqUpTo]
30  omega
31
32/-- A previously completed positive run already emitted its ordinary
33length symbol. Repetitions can omit that symbol only after it was emitted. -/
34theorem scanFreq_prev_positive (L : Nat → Nat) (n k : Nat) (hk : 0 < k)
35    (hp : (runAt L n).prev = (k : Int)) : 0 < scanFreqUpTo L n k := by
36  induction n with
37  | zero =>
38    simp only [runAt, runInit] at hp
39    split at hp <;> (dsimp only at hp; omega)
40  | succ n ih =>
41    by_cases ha : (runAt L n).cnt + 1 < (runAt L n).mx ∧ (runAt L n).next = L (n + 1)
42    · have hp' : (runAt L n).prev = (k : Int) := by
43        simpa only [runAt, runStep, ite_eq_left ha] using hp
44      have hb := ih hp'
45      have hm := scanFreq_le_next L n k
46      omega
47    · have hcur : (runAt L n).next = k := by
48        have ht := runStep_done_prev L n (runAt L n) ha
49        change (runStep L n (runAt L n)).1.prev = (k : Int) at hp
50        rw [ht] at hp
51        omega
52      by_cases hsame : ((runAt L n).next : Int) = (runAt L n).prev
53      · have hb := ih (by rw [← hsame, hcur])
54        have hm := scanFreq_le_next L n k
55        omega
56      · have hf : 0 < runFreq (some ((runAt L n).next, (runAt L n).prev, (runAt L n).cnt + 1, (runAt L n).mn)) k := by
57          simp only [runFreq]
58          by_cases hs : (runAt L n).cnt + 1 < (runAt L n).mn
59          · simp only [ite_eq_left hs, ite_eq_left (show k = (runAt L n).next by omega)]
60            omega
61          · simp only [ite_eq_right hs, ite_eq_left (show (runAt L n).next ≠ 0 by omega),
62              ite_eq_left (show ((runAt L n).next : Int) ≠ (runAt L n).prev ∧ k = (runAt L n).next from ⟨hsame, by omega⟩)]
63            omega
64        simp only [scanFreqUpTo, runStep, ite_eq_right ha]
65        change 0 < scanFreqUpTo L n k + runFreq (some ((runAt L n).next, (runAt L n).prev, (runAt L n).cnt + 1, (runAt L n).mn)) k
66        omega
67
68/-- Finishing a positive run gives positive accumulated frequency even if
69the current run itself uses only a repetition code. -/
70theorem scanFreq_finished_positive (L : Nat → Nat) (n k : Nat) (hk : 0 < k)
71    (hc : (runAt L n).next = k)
72    (ha : ¬ ((runAt L n).cnt + 1 < (runAt L n).mx ∧ (runAt L n).next = L (n + 1))) :
73    0 < scanFreqUpTo L (n + 1) k := by
74  by_cases hp : ((runAt L n).next : Int) = (runAt L n).prev
75  · have hprev : (runAt L n).prev = (k : Int) := by rw [← hp, hc]
76    have hb := scanFreq_prev_positive L n k hk hprev
77    have hm := scanFreq_le_next L n k
78    omega
79  · have hf : 0 < runFreq (some ((runAt L n).next, (runAt L n).prev, (runAt L n).cnt + 1, (runAt L n).mn)) k := by
80      simp only [runFreq]
81      by_cases hs : (runAt L n).cnt + 1 < (runAt L n).mn
82      · simp only [ite_eq_left hs, ite_eq_left (show k = (runAt L n).next by omega)]
83        omega
84      · simp only [ite_eq_right hs, ite_eq_left (show (runAt L n).next ≠ 0 by omega),
85          ite_eq_left (show ((runAt L n).next : Int) ≠ (runAt L n).prev ∧ k = (runAt L n).next from ⟨hp, by omega⟩)]
86        omega
87    simp only [scanFreqUpTo, runStep, ite_eq_right ha]
88    omega
89
90/-- A positive length that was read is either already represented by an
91ordinary length code, or is still in the unfinished current run. -/
92theorem scanFreq_seen_positive (L : Nat → Nat) (n v k : Nat) (hv : v < n)
93    (hk : 0 < k) (hvk : L v = k) :
94    0 < scanFreqUpTo L n k ∨ ((runAt L n).next = k ∧ 0 < (runAt L n).cnt) := by
95  induction n with
96  | zero => omega
97  | succ n ih =>
98    have hcur : (runAt L n).next = L n := runAt_next L n
99    by_cases ha : (runAt L n).cnt + 1 < (runAt L n).mx ∧ (runAt L n).next = L (n + 1)
100    · have hnext : (runAt L (n + 1)).next = (runAt L n).next := by
101        simp only [runAt, runStep, ite_eq_left ha]
102        exact ha.2.symm
103      have hcnt : 0 < (runAt L (n + 1)).cnt := by
104        simp only [runAt, runStep, ite_eq_left ha]
105        omega
106      by_cases hvn : v = n
107      · right
108        rw [hvn] at hvk
109        exact ⟨hnext.trans (hcur.trans hvk), hcnt⟩
110      · rcases ih (by omega) with hp | ⟨hn, hc⟩
111        · left
112          have hm := scanFreq_le_next L n k
113          omega
114        · exact Or.inr ⟨hnext.trans hn, hcnt⟩
115    · by_cases hvn : v = n
116      · left
117        rw [hvn] at hvk
118        exact scanFreq_finished_positive L n k hk (hcur.trans hvk) ha
119      · rcases ih (by omega) with hp | ⟨hn, hc⟩
120        · left
121          have hm := scanFreq_le_next L n k
122          omega
123        · exact Or.inl (scanFreq_finished_positive L n k hk hn ha)
124
125/-- Once the last pending run is finished, every positive source length
126already has positive ordinary-symbol frequency. -/
127theorem scanFreq_seen_done (L : Nat → Nat) (n v k : Nat) (hv : v < n)
128    (hk : 0 < k) (hvk : L v = k) (hdone : (runAt L n).cnt = 0) :
129    0 < scanFreqUpTo L n k := by
130  rcases scanFreq_seen_positive L n v k hv hk hvk with hf | ⟨hnext, hc⟩
131  · exact hf
132  · omega
133
134end Zlib.Trees.Proofs.Out