trees.c.heap.gbclk.lean

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

1import ZlibF.Proof.«trees.c.heap.gbtree»
2
3/-!
4# Pure facts for the first pass of `gen_bitlen`
5
6`clK H hm elems L k` is the clamped depth after `k` non-root positions were processed; `blP`, `ovP`, `costP` are
7the counts the first pass has accumulated. Copied from the earlier attempt (`GenBitlenBase.lean`,
8`GenBitlenPass1.lean`), unchanged except for the namespace.
9-/
10
11namespace Zlib.Trees.Proofs.GB
12
13/-- Clamped depths after processing the first `k` non-root positions. -/
14def clK (H : Nat → Nat) (hm elems L : Nat) : Nat → Nat → Nat
15  | 0 => fun _ => 0
16  | k + 1 => fun v => if v = H (hm + 1 + k) then min (clK H hm elems L k (dadP elems (hm + 1 + k)) + 1) L
17      else clK H hm elems L k v
18
19section cl
20variable {H : Nat → Nat} {hm J elems maxc L : Nat}
21
22theorem clK_stable (S : PShape H hm J elems maxc) (q k : Nat) (hq1 : hm ≤ q) (hq2 : q ≤ hm + k) :
23    ∀ k', k ≤ k' → k' ≤ 2 * J → clK H hm elems L k' (H q) = clK H hm elems L k (H q) := by
24  have := S.hm_eq
25  intro k'
26  induction k' with
27  | zero => intro h1 _; rw [show k = 0 by omega]
28  | succ k' ih =>
29    intro h1 h2
30    by_cases e : k = k' + 1
31    · subst e; rfl
32    · simp only [clK]; rw [ite_eq_right (fun e' => by have := S.inj q (hm + 1 + k') hq1 (by omega) (by omega) (by omega) e'; omega)]
33      exact ih (by omega) (by omega)
34
35theorem dad_pos (S : PShape H hm J elems maxc) (i : Nat) (hi : i < 2 * J) :
36    ∃ q, hm ≤ q ∧ q ≤ hm + i ∧ H q = dadP elems (hm + 1 + i) := by
37  have := S.hm_eq
38  obtain ⟨q, h1, h2, e⟩ := S.appears ((2 * J - 1 - i) / 2) (by omega)
39  exact ⟨q, h1, by omega, by rw [e, S.dadP_eq i hi]⟩
40
41theorem clK_clamped (S : PShape H hm J elems maxc) : Clamped H hm J elems L (clK H hm elems L (2 * J)) := by
42  have := S.hm_eq
43  refine ⟨?_, ?_⟩
44  · rw [clK_stable S hm 0 (Nat.le_refl _) (by omega) (2 * J) (by omega) (Nat.le_refl _)]; rfl
45  · intro i hi
46    rw [clK_stable S (hm + 1 + i) (i + 1) (by omega) (by omega) (2 * J) (by omega) (Nat.le_refl _)]
47    simp only [clK, ite_true]
48    obtain ⟨q, h1, h2, e⟩ := dad_pos S i hi
49    rw [← e, clK_stable S q i h1 h2 (2 * J) (by omega) (Nat.le_refl _)]
50
51end cl
52
53/-- Leaves of length `b` among the first `k` non-root positions. -/
54def blP (H : Nat → Nat) (hm maxc : Nat) (len : Nat → Nat) (k b : Nat) : Nat :=
55  rs (fun i => if H (hm + 1 + i) ≤ maxc ∧ len (H (hm + 1 + i)) = b then 1 else 0) k
56
57/-- Clamped nodes among the first `k` non-root positions. -/
58def ovP (H : Nat → Nat) (hm elems L : Nat) (cl : Nat → Nat) (k : Nat) : Nat :=
59  rs (fun i => if cl (dadP elems (hm + 1 + i)) = L then 1 else 0) k
60
61/-- `Σ f · (len + xbits)` over the leaves among the first `k` non-root positions. -/
62def costP (H : Nat → Nat) (hm maxc : Nat) (fr len xb : Nat → Nat) (k : Nat) : Nat :=
63  rs (fun i => if H (hm + 1 + i) ≤ maxc then fr (H (hm + 1 + i)) * (len (H (hm + 1 + i)) + xb (H (hm + 1 + i)))
64    else 0) k
65
66theorem blP_succ (H : Nat → Nat) (hm maxc : Nat) (len : Nat → Nat) (k b : Nat) :
67    blP H hm maxc len (k + 1) b = blP H hm maxc len k b +
68      (if H (hm + 1 + k) ≤ maxc ∧ len (H (hm + 1 + k)) = b then 1 else 0) := rfl
69
70theorem costP_succ (H : Nat → Nat) (hm maxc : Nat) (fr len xb : Nat → Nat) (k : Nat) :
71    costP H hm maxc fr len xb (k + 1) = costP H hm maxc fr len xb k +
72      (if H (hm + 1 + k) ≤ maxc then fr (H (hm + 1 + k)) * (len (H (hm + 1 + k)) + xb (H (hm + 1 + k))) else 0) :=
73  rfl
74
75theorem blP_le (H : Nat → Nat) (hm maxc : Nat) (len : Nat → Nat) (k b : Nat) : blP H hm maxc len k b ≤ k := by
76  have := rs_le (n := k) (F := fun i => if H (hm + 1 + i) ≤ maxc ∧ len (H (hm + 1 + i)) = b then 1 else 0)
77    (G := fun _ => 1) (fun i _ => by split <;> omega)
78  rw [rs_const] at this; unfold blP; omega
79
80theorem ovP_le (H : Nat → Nat) (hm elems L : Nat) (cl : Nat → Nat) (k : Nat) : ovP H hm elems L cl k ≤ k := by
81  have := rs_le (n := k) (F := fun i => if cl (dadP elems (hm + 1 + i)) = L then 1 else 0)
82    (G := fun _ => 1) (fun i _ => by split <;> omega)
83  rw [rs_const] at this; unfold ovP; omega
84
85
86end Zlib.Trees.Proofs.GB