inftrees.c.geom.lean

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

1import ZlibF.Proof.«inftrees.c.canonbridge»
2
3/-!
4# The geometry of the table: the closed form `desc` against the model of the main proof
5-/
6namespace Zlib.Inftrees.Proofs
7open Zlib.Inftrees.Canon
8
9theorem nz_eq (f : Nat → Nat) (n : Nat) : Canon.nz (lensOf f n) = Tc f n 15 := by
10  unfold Canon.nz; rw [ord_eq]; exact wsAux_length 15
11
12theorem count_eq (f : Nat → Nat) (n l : Nat) : (lensOf f n).count l = cnt f n l := by
13  unfold lensOf cnt fl
14  rw [List.count_eq_countP, List.countP_map, List.countP_eq_length_filter]
15  rfl
16
17theorem offL_eq (f : Nat → Nat) (n : Nat) : ∀ l, Canon.offL (lensOf f n) (l + 1) = Tc f n l
18  | 0 => by simp [Canon.offL_one, Tc]
19  | l + 1 => by
20    rw [Canon.offL_succ, offL_eq f n l]
21    simp [count_eq, Tc]
22
23theorem cntGE_eq (f : Nat → Nat) (n a : Nat) {l : Nat} (hl : 1 ≤ l) :
24    Canon.cntGE (lensOf f n) a l = rem f n a l := by
25  unfold Canon.cntGE rem
26  obtain ⟨l', rfl⟩ : ∃ l', l = l' + 1 := ⟨l - 1, by omega⟩
27  rw [offL_eq, offL_eq]
28  simp
29
30theorem grp_eq_pre (f : Nat → Nat) (n R : Nat) {j : Nat} (hj : j < Tc f n 15) (hR : R ≤ lenAt f n j) :
31    Canon.grp (lensOf f n) R j = pre f n R j := by
32  obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hj
33  unfold Canon.grp pre
34  rw [K_eq f n j hj]
35  have e : 2 ^ (15 - R) = 2 ^ (15 - lenAt f n j) * 2 ^ (lenAt f n j - R) := by
36    rw [← Nat.pow_add]; congr 1; omega
37  rw [e, Nat.mul_comm (val f n j) _, Nat.mul_div_mul_left _ _ (Nat.pow_pos (by omega))]
38
39theorem startsAt_iff (f : Nat → Nat) (n R : Nat) {i : Nat} (hi : i + 1 < Tc f n 15) :
40    Canon.startsAt (lensOf f n) R i ↔
41      (R < lenAt f n (i + 1) ∧ (lenAt f n i ≤ R ∨ pre f n R (i + 1) ≠ pre f n R i)) := by
42  unfold Canon.startsAt
43  rw [L_eq f n hi, L_eq f n (show i < Tc f n 15 by omega)]
44  by_cases hs : lenAt f n i ≤ R
45  · simp [hs]
46  · have hR1 : R < lenAt f n (i + 1) ∨ lenAt f n (i + 1) ≤ R := by omega
47    simp only [hs, false_or]
48    constructor
49    · rintro ⟨h1, h2⟩
50      refine ⟨h1, ?_⟩
51      rwa [grp_eq_pre f n R hi (by omega), grp_eq_pre f n R (show i < Tc f n 15 by omega) (by omega)] at h2
52    · rintro ⟨h1, h2⟩
53      refine ⟨h1, ?_⟩
54      rw [grp_eq_pre f n R hi (by omega), grp_eq_pre f n R (show i < Tc f n 15 by omega) (by omega)]
55      exact h2
56
57theorem look_eq (f : Nat → Nat) (n a R mx : Nat) (hR1 : 1 ≤ R) :
58    ∀ F c (left : Int), mx - R - c ≤ F →
59      Canon.look (lensOf f n) a R mx c left F = (SL (rem f n a) R mx c left).1
60  | 0, c, left, h => by
61    have : mx ≤ R + c := by omega
62    rw [SL_ge this]; rfl
63  | F + 1, c, left, h => by
64    by_cases hc : c + R < mx
65    · rw [SL_lt (show R + c < mx by omega)]
66      simp only [Canon.look, hc, ite_true]
67      rw [cntGE_eq f n a (show 1 ≤ c + R by omega), show c + R = R + c by omega]
68      by_cases hl : left - (rem f n a (R + c) : Int) ≤ 0
69      · simp [hl]
70      · simp only [hl, ite_false]
71        rw [look_eq f n a R mx hR1 F (c + 1) _ (by omega)]
72        rw [Int.mul_comm]
73    · rw [SL_ge (show mx ≤ R + c by omega), Canon.look]
74      simp [hc]
75
76theorem width_eq (f : Nat → Nat) (n R : Nat) {a : Nat} (hR1 : 1 ≤ R) (ha : a < Tc f n 15)
77    (hmx : lenAt f n a ≤ mxl f n) (hRa : R < lenAt f n a) (h15 : mxl f n ≤ 15) :
78    Canon.width (lensOf f n) a R (mxl f n) = currOf f n R a := by
79  unfold Canon.width currOf
80  rw [L_eq f n ha, look_eq f n a R (mxl f n) hR1 16 _ _ (by omega)]
81
82theorem desc_succ_of_starts (ls : List Nat) (R mx i : Nat) (h : Canon.startsAt ls R i) :
83    Canon.desc ls R mx (i + 1) =
84      ⟨R, Canon.width ls (i + 1) R mx, (Canon.desc ls R mx i).base + 2 ^ (Canon.desc ls R mx i).curr,
85        (Canon.desc ls R mx i).used + 2 ^ Canon.width ls (i + 1) R mx, Canon.rev R (Canon.grp ls R (i + 1))⟩ := by
86  simp [Canon.desc, h]
87
88theorem desc_succ_of_not (ls : List Nat) (R mx i : Nat) (h : ¬ Canon.startsAt ls R i) :
89    Canon.desc ls R mx (i + 1) = Canon.desc ls R mx i := by
90  simp [Canon.desc, h]
91
92end Zlib.Inftrees.Proofs