inftrees.c.canonbridge.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Proof.«inftrees.c.canon»
2import ZlibF.Proof.«inftrees.c.link»
3
4/-!
5# The two models of the canonical construction agree
6
7`Canon` (a list `ls` of lengths, allocation index `j`, Kraft sums `K`) and the model of the main proof
8(`f`, `n`, `wsAux`, `lenAt`, `val`) describe the same objects for `ls = lensOf f n`.
9-/
10namespace Zlib.Inftrees.Proofs
11open Zlib.Inftrees.Canon
12
13theorem canon_rev_eq : ∀ k x, Canon.rev k x = Proofs.rev k x
14  | 0, _ => rfl
15  | k + 1, x => by
16    rw [Canon.rev_succ, canon_rev_eq k, Proofs.rev]; omega
17
18theorem lensOf_length (f : Nat → Nat) (n : Nat) : (lensOf f n).length = n := by simp [lensOf]
19
20theorem lensOf_getD (f : Nat → Nat) {n s : Nat} (h : s < n) : (lensOf f n).getD s 0 = f s := by
21  simp [lensOf, List.getD_eq_getElem?_getD, h]
22
23theorem symsOf_eq (f : Nat → Nat) (n l : Nat) : symsOf (lensOf f n) l = fl f l n := by
24  unfold symsOf fl
25  rw [lensOf_length]
26  apply List.filter_congr
27  intro s hs
28  rw [List.mem_range] at hs
29  rw [lensOf_getD f hs]
30
31theorem ord_eq (f : Nat → Nat) (n : Nat) : ord (lensOf f n) = wsAux f n 15 := by
32  unfold ord
33  have : ∀ k, (List.range k).flatMap (fun i => symsOf (lensOf f n) (i + 1)) = wsAux f n k := by
34    intro k
35    induction k with
36    | zero => rfl
37    | succ k ih =>
38      rw [List.range_succ, List.flatMap_append, ih]
39      simp [wsAux, symsOf_eq]
40  exact this 15
41
42theorem L_eq (f : Nat → Nat) (n : Nat) {j : Nat} (hj : j < Tc f n 15) :
43    L (lensOf f n) j = lenAt f n j := by
44  unfold L sy lenAt
45  rw [ord_eq]
46  have hlen : (wsAux f n 15).length = Tc f n 15 := wsAux_length 15
47  have hm := List.getElem_mem (show j < (wsAux f n 15).length by omega)
48  have hs := (mem_wsAux.mp hm).1
49  have hg : (wsAux f n 15).getD j 0 = (wsAux f n 15)[j]'(by omega) := by
50    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (by omega), Option.getD_some]
51  rw [hg]
52  exact lensOf_getD f hs
53
54theorem K_succ (ls : List Nat) (j : Nat) : K ls (j + 1) = K ls j + 2 ^ (15 - L ls j) := by
55  unfold K
56  rw [List.range_succ, List.map_append, List.sum_append]
57  simp
58
59theorem K_eq (f : Nat → Nat) (n : Nat) : ∀ j, j < Tc f n 15 →
60    K (lensOf f n) j = val f n j * 2 ^ (15 - lenAt f n j)
61  | 0, h => by
62    rw [val_zero h]; simp [K]
63  | j + 1, h => by
64    have ih := K_eq f n j (by omega)
65    obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) (show j < Tc f n 15 by omega)
66    obtain ⟨c1, c2⟩ := lenAt_bounds (f := f) (n := n) h
67    have mono := lenAt_mono (f := f) (n := n) (show j ≤ j + 1 by omega) h
68    have hs := val_succ (f := f) (n := n) h
69    rw [K_succ, L_eq f n (by omega), ih, hs]
70    obtain ⟨d, hd⟩ : ∃ d, lenAt f n (j + 1) = lenAt f n j + d := ⟨lenAt f n (j + 1) - lenAt f n j, by omega⟩
71    have e1 : lenAt f n (j + 1) - lenAt f n j = d := by omega
72    have e2 : 15 - lenAt f n j = (15 - lenAt f n (j + 1)) + d := by omega
73    rw [e1, e2, Nat.pow_add, Nat.add_mul, Nat.one_mul]
74    generalize (2 : Nat) ^ (15 - lenAt f n (j + 1)) = P
75    generalize (2 : Nat) ^ d = Q
76    generalize val f n j = V
77    rw [Nat.add_mul]
78    ac_rfl
79
80theorem H_eq (f : Nat → Nat) (n : Nat) {j : Nat} (hj : j < Tc f n 15) :
81    H (lensOf f n) j = Proofs.rev (lenAt f n j) (val f n j) := by
82  unfold H cv
83  rw [K_eq f n j hj, L_eq f n hj, Nat.mul_div_cancel _ (Nat.pow_pos (by omega)), canon_rev_eq]
84
85end Zlib.Inftrees.Proofs