inftrees.c.content.geometry.lean

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

1import ZlibF.Math.InflateTableGeometry
2import ZlibF.Proof.«inftrees.c.cover.fn»
3
4/-!
5# inftrees.c: discharge the content invariant's geometry premise
6
7Geometry follows from the actual loop environment. Complete codes and the
8accepted incomplete single-symbol case are handled separately.
9-/
10
11namespace Zlib.Inftrees.Proofs
12open Zlib.Inftrees.Canon
13set_option autoImplicit false
14
15/-- Every actual nonempty constructor loop environment establishes Geo;
16it is no longer a condition left for a public caller to assume. -/
17theorem Env.geometry (e : Env) : e.Geo := by
18  rcases e.h_end with complete | ⟨_, single, _⟩
19  · apply geometry_complete
20    refine ⟨?_, ?_, e.h_R1, e.h_Rmx, ?_, ?_⟩
21    · change 0 < Canon.nz (lensOf e.f e.n)
22      rw [Zlib.Inftrees.Proofs.nz_eq]
23      exact e.h_pos
24    · exact Cover.complete_of_Kc complete
25    · change mxl e.f e.n = Canon.L (lensOf e.f e.n) (Canon.nz (lensOf e.f e.n) - 1)
26      rw [Zlib.Inftrees.Proofs.nz_eq, L_eq e.f e.n (by have := e.h_pos; omega)]
27      rfl
28    · change Canon.L (lensOf e.f e.n) 0 ≤ e.R
29      rw [L_eq e.f e.n e.h_pos]
30      exact e.h_R0
31  · apply geometry_single
32    change Canon.nz (lensOf e.f e.n) = 1
33    rw [Zlib.Inftrees.Proofs.nz_eq]
34    exact single
35
36/-- Recover unconditional written-cell and link facts from the existing
37loop content result, using the proved geometry of that same environment. -/
38theorem Cont.established {e : Env} {written links : Nat} {ca : Array C.Code}
39    (content : Cont e written links ca) : Written e written ca ∧ Links e links ca :=
40  content e.geometry
41
42end Zlib.Inftrees.Proofs