LZ77History.lean

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

1import ZlibF.Math.LZ77HistorySpec
2
3/-!
4# Chunked copies and retained independent history
5
6Every step reads the same byte when the requested distance is inside the
7retained suffix. Induction then preserves both complete and retained views.
8-/
9
10set_option autoImplicit false
11
12namespace ZlibF.Math.LZ77History
13open ZlibF.Spec
14
15/-- A match appends exactly one byte at each step and never changes old
16output, even when a caller supplies an invalid distance to the pure model. -/
17theorem copy_back_extends_history : Goal.copy_back_extends_history := by
18  intro dict history dist n
19  induction n generalizing history with
20  | zero => simp [copyBack]
21  | succ n ih =>
22    let value := (dict ++ history).getD ((dict ++ history).length - dist) 0
23    have next := ih (history ++ [value])
24    constructor
25    · exact (List.prefix_append history [value]).trans next.1
26    · simpa only [copyBack, value, List.length_append, List.length_singleton,
27        Nat.add_assoc, Nat.add_comm 1 n] using next.2
28
29/-- Splitting a match into physical chunks does not change its bytewise
30independent result. -/
31theorem copy_back_compose : Goal.copy_back_compose := by
32  intro dict history dist n m
33  induction n generalizing history with
34  | zero => simp [copyBack]
35  | succ n ih =>
36    rw [show n + 1 + m = (n + m) + 1 by omega]
37    simp only [copyBack]
38    exact ih _
39
40private theorem retained_source (dict past current saved : List UInt8) (dist : Nat)
41    (hs : saved <:+ (dict ++ past)) (hd : dist ≤ saved.length + current.length) :
42    (dict ++ (past ++ current)).getD ((dict ++ (past ++ current)).length - dist) 0 =
43      (saved ++ current).getD ((saved ++ current).length - dist) 0 := by
44  obtain ⟨older, he⟩ := hs
45  have hword : dict ++ (past ++ current) = older ++ (saved ++ current) := by
46    rw [← List.append_assoc, ← he, List.append_assoc]
47  rw [hword]
48  have hr : older.length ≤ (older ++ (saved ++ current)).length - dist := by
49    simp only [List.length_append] at *
50    omega
51  have hi : (older ++ (saved ++ current)).length - dist - older.length =
52      (saved ++ current).length - dist := by
53    simp only [List.length_append] at *
54    omega
55  simp only [List.getD_eq_getElem?_getD, List.getElem?_append_right hr, hi]
56
57/-- Replacing complete prior history by a suffix preserves every newly
58copied byte as long as the match reaches only retained history. -/
59theorem retained_history_agrees : Goal.retained_history_agrees := by
60  intro dict past current saved dist n hs hpositive hdist
61  induction n generalizing current with
62  | zero => simp [copyBack]
63  | succ n ih =>
64    have hvalue := retained_source dict past current saved dist hs hdist
65    rw [copyBack, copyBack, hvalue]
66    rw [List.append_assoc]
67    exact ih (current ++ [(saved ++ current).getD ((saved ++ current).length - dist) 0])
68      (by simp only [List.length_append, List.length_singleton]; omega)
69
70/-- A complete retained window discards only history that a capacity-bounded
71distance cannot reach, so the two invalid-distance tests coincide. -/
72theorem window_distance_check_agrees : Goal.window_distance_check_agrees := by
73  intro dict past current capacity dist hdist
74  simp only [List.length_append, List.length_drop]
75  omega
76
77end ZlibF.Math.LZ77History