inftrees.c.link.lean

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

1import ZlibF.Proof.«inftrees.c.math»
2import ZlibF.Spec.Format.Huffman
3import ZlibF.Runtime.Schema
4import ZlibF.Proof.«inftrees.c.spec»
5
6namespace Zlib.Inftrees.Proofs
7open ZlibF.Spec
8
9/-- The list of lengths that the call looks at. -/
10def lensOf (f : Nat → Nat) (n : Nat) : List Nat := (List.range n).map f
11
12theorem count_lensOf (f : Nat → Nat) (n l : Nat) : ZlibF.Spec.count (lensOf f n) l = cnt f n l := by
13  unfold ZlibF.Spec.count lensOf cnt fl
14  rw [List.filter_map, List.length_map]
15  rfl
16
17theorem codeStart_lensOf (f : Nat → Nat) (n : Nat) : ∀ l, codeStart (lensOf f n) (l + 1) = 2 * Kc f n l
18  | 0 => by simp [codeStart, Kc]
19  | l + 1 => by
20    rw [codeStart, codeStart_lensOf f n l]
21    simp [count_lensOf, Kc]
22    omega
23
24theorem fits_iff (f : Nat → Nat) (n : Nat) : ZlibF.Spec.Fits (lensOf f n) ↔ Fits f n := by
25  unfold ZlibF.Spec.Fits Zlib.Inftrees.Proofs.Fits
26  constructor
27  · intro h l hl1 hl2
28    have hm : ZlibF.Spec.maxCodeLen = 15 := rfl
29    have := h l (by simp [List.mem_range'_1, hm]; omega)
30    obtain ⟨l', rfl⟩ : ∃ l', l = l' + 1 := ⟨l - 1, by omega⟩
31    rw [codeStart_lensOf, count_lensOf] at this
32    simpa [Kc] using this
33  · intro h l hl
34    have hm : ZlibF.Spec.maxCodeLen = 15 := rfl
35    simp only [List.mem_range'_1, hm] at hl
36    obtain ⟨l', rfl⟩ : ∃ l', l = l' + 1 := ⟨l - 1, by omega⟩
37    have := h (l' + 1) (by omega) (by omega)
38    rw [codeStart_lensOf, count_lensOf]
39    simpa [Kc] using this
40
41theorem complete_iff (f : Nat → Nat) (n : Nat) : ZlibF.Spec.Complete (lensOf f n) ↔ Kc f n 15 = 2 ^ 15 := by
42  unfold ZlibF.Spec.Complete ZlibF.Spec.maxCodeLen
43  rw [show (15 : Nat) = 14 + 1 from rfl, codeStart_lensOf, count_lensOf]
44  simp [Kc]
45
46theorem Tc_eq_len (f : Nat → Nat) :
47    ∀ n, (∀ s, s < n → f s ≤ 15) → Tc f n 15 = ((List.range n).filter (fun s => decide (f s ≠ 0))).length
48  | 0, _ => rfl
49  | n + 1, hf => by
50    rw [Tc_step, Tc_eq_len f n (fun s hs => hf s (by omega)), List.range_succ, List.filter_append]
51    have := hf n (by omega)
52    by_cases h : f n = 0
53    · simp [h]
54    · simp [h]; omega
55
56/-- `inflate_table` accepts the lengths (the rule of `inftrees.c`, in the terms of the proofs). -/
57def Acc (type : UInt32) (f : Nat → Nat) (n : Nat) : Prop :=
58  Fits f n ∧ (Kc f n 15 = 2 ^ 15 ∨ Tc f n 15 = 0 ∨ (type ≠ C.CODES ∧ mxl f n = 1 ∧ Tc f n 15 = 1))
59
60theorem zero_iff (f : Nat → Nat) (n : Nat) (hf : ∀ s, s < n → f s ≤ 15) :
61    (∀ x ∈ lensOf f n, x = 0) ↔ Tc f n 15 = 0 := by
62  rw [Tc_eq_len f n hf, List.length_eq_zero_iff, List.filter_eq_nil_iff]
63  simp [lensOf]
64
65theorem single_iff (f : Nat → Nat) (n : Nat) (hf : ∀ s, s < n → f s ≤ 15) :
66    (lensOf f n).filter (· != 0) = [1] ↔ (Tc f n 15 = 1 ∧ mxl f n = 1) := by
67  have hI : (lensOf f n).filter (· != 0) = ((List.range n).filter (fun s => decide (f s ≠ 0))).map f := by
68    unfold lensOf
69    rw [List.filter_map]
70    congr 1
71  have hT := Tc_eq_len f n hf
72  have hlen : (wsAux f n 15).length = Tc f n 15 := wsAux_length 15
73  -- the first symbol of the sorted order
74  have hw : Tc f n 15 = 1 →
75      (wsAux f n 15).getD 0 0 ∈ (List.range n).filter (fun s => decide (f s ≠ 0)) := by
76    intro h1
77    have hlt : 0 < (wsAux f n 15).length := by omega
78    have hm := List.getElem_mem hlt
79    have := mem_wsAux.mp hm
80    have hg : (wsAux f n 15).getD 0 0 = (wsAux f n 15)[0] := by
81      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hlt, Option.getD_some]
82    rw [hg]
83    simp only [List.mem_filter, List.mem_range, decide_eq_true_eq]
84    exact ⟨this.1, by omega⟩
85  have hmx : Tc f n 15 = 1 → mxl f n = f ((wsAux f n 15).getD 0 0) := by
86    intro h1; unfold mxl lenAt; rw [h1]
87  rw [hI]
88  constructor
89  · intro h
90    obtain ⟨s0, hs0, hf0⟩ := List.map_eq_singleton_iff.mp h
91    have hT1 : Tc f n 15 = 1 := by rw [hT, hs0]; rfl
92    refine ⟨hT1, ?_⟩
93    have hmem := hw hT1
94    rw [hs0] at hmem
95    have : (wsAux f n 15).getD 0 0 = s0 := by simpa using hmem
96    rw [hmx hT1, this]; exact hf0
97  · rintro ⟨hT1, hm1⟩
98    obtain ⟨s0, hs0⟩ := List.length_eq_one_iff.mp (by rw [← hT]; exact hT1)
99    have hmem := hw hT1
100    rw [hs0] at hmem
101    have : (wsAux f n 15).getD 0 0 = s0 := by simpa using hmem
102    rw [hs0]
103    have : f s0 = 1 := by rw [← this, ← hmx hT1]; exact hm1
104    simp [this]
105
106theorem acc_iff (type : UInt32) (f : Nat → Nat) (n : Nat) (hf : ∀ s, s < n → f s ≤ 15) :
107    Acc type f n ↔ ZlibF.Spec.Acceptable (Zlib.Inftrees.Spec.kindOf type) (lensOf f n) := by
108  unfold Acc ZlibF.Spec.Acceptable
109  have hk : Zlib.Inftrees.Spec.kindOf type ≠ ZlibF.Spec.CodeKind.codeLength ↔ type ≠ C.CODES := by
110    unfold Zlib.Inftrees.Spec.kindOf
111    by_cases h1 : type = C.CODES
112    · simp [h1]
113    · by_cases h2 : type = C.LENS <;> simp [h1, h2]
114  have hb : ∀ x ∈ lensOf f n, x ≤ ZlibF.Spec.maxCodeLen := by
115    intro x hx
116    simp only [lensOf, List.mem_map, List.mem_range] at hx
117    obtain ⟨s, hs, rfl⟩ := hx
118    exact hf s hs
119  rw [fits_iff, complete_iff, zero_iff f n hf, hk]
120  constructor
121  · rintro ⟨h1, h2⟩
122    refine ⟨hb, h1, ?_⟩
123    rcases h2 with h | h | ⟨a, b, c⟩
124    · exact Or.inl h
125    · exact Or.inr (Or.inl h)
126    · exact Or.inr (Or.inr ⟨a, (single_iff f n hf).mpr ⟨c, b⟩⟩)
127  · rintro ⟨_, h1, h2⟩
128    refine ⟨h1, ?_⟩
129    rcases h2 with h | h | ⟨a, b⟩
130    · exact Or.inl h
131    · exact Or.inr (Or.inl h)
132    · obtain ⟨c, d⟩ := (single_iff f n hf).mp b
133      exact Or.inr (Or.inr ⟨a, d, c⟩)
134
135end Zlib.Inftrees.Proofs