deflate.c.engine.loops.lean

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

1import ZlibF.Runtime.Monad
2
3/-!
4# deflate.c, engine: a loop rule with a measure
5
6`cdoWhile_run` and `cwhile_run` need the exact number of iterations. The loops of `longest_match` and
7`fill_window` end when a data-dependent test fails, so they use this rule: an invariant, a measure that falls on
8every iteration that continues, and a postcondition for the iteration that stops.
9-/
10
11namespace C
12
13/-- `do body while (cond)` with an invariant `Inv`: every iteration keeps `Inv`, and either stops with `Q` or
14continues with a smaller measure. The heap is carried through the invariant. -/
15theorem cdoWhile_measure {σ : Type} {body : σ → M σ} {cond : σ → M (Bool × σ)}
16    (Inv : σ → Heap → Prop) (μ : σ → Nat) (Q : σ → Heap → Prop)
17    (hstep : ∀ s h, Inv s h → ∃ s1 h1 c s2 h2, body s h = .ok (s1, h1) ∧ cond s1 h1 = .ok ((c, s2), h2) ∧
18      (c = false → Q s2 h2) ∧ (c = true → Inv s2 h2 ∧ μ s2 < μ s))
19    {s : σ} {h : Heap} (hI : Inv s h) (hμ : μ s < fuel) :
20    ∃ s' h', cdoWhile body cond s h = .ok (s', h') ∧ Q s' h' := by
21  have key : ∀ n (s : σ) (h : Heap), Inv s h → μ s < n →
22      ∃ s' h', cdoWhile.go body cond n s h = .ok (s', h') ∧ Q s' h' := by
23    intro n
24    induction n with
25    | zero => intro s h _ hn; omega
26    | succ n ih =>
27      intro s h hI hn
28      obtain ⟨s1, h1, c, s2, h2, hb, hc, hq, hcont⟩ := hstep s h hI
29      cases c with
30      | false => exact ⟨s2, h2, by simp [cdoWhile.go, hb, hc], hq rfl⟩
31      | true =>
32        obtain ⟨hI2, hlt⟩ := hcont rfl
33        obtain ⟨s', h', hrun, hQ⟩ := ih s2 h2 hI2 (by omega)
34        exact ⟨s', h', by simp [cdoWhile.go, hb, hc, hrun], hQ⟩
35  exact key fuel s h hI hμ
36
37/-- A monadic `if` applied to the heap. -/
38theorem M_ite_app {α : Type} (c : Prop) [Decidable c] (a b : M α) (h : Heap) :
39    (if c then a else b) h = if c then a h else b h := by
40  split <;> rfl
41
42end C