Compress.lean

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

1import ZlibF.Spec.Api.Goals
2
3namespace ZlibF.Spec.Api.Proofs
4
5/-- The `Compress2` model refuses `Z_BUF_ERROR` when the destination has at least
6`compressBound` bytes, and its output stays within that bound. This is a property
7of the model relation; applying it to translated calls also needs refinement. -/
8theorem compress_bound_adequate : Goal.compress_bound_adequate := by
9  intro level src cap rc dst hcap hrun
10  cases hp : compressParams level with
11  | none =>
12    simp only [Compress2, Bool.true_eq_false, ↓reduceIte, hp] at hrun
13    obtain ⟨rfl, rfl⟩ := hrun
14    exact ⟨by decide, by simp⟩
15  | some p =>
16    simp only [Compress2, Bool.true_eq_false, ↓reduceIte, hp] at hrun
17    rcases hrun with ⟨rfl, rfl⟩ | ⟨rfl, _, _, hb⟩ | ⟨_, _, hlt, _⟩
18    · exact ⟨by decide, by simp⟩
19    · exact ⟨by decide, hb⟩
20    · omega
21
22end ZlibF.Spec.Api.Proofs