gz-seek-mode.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.Examples
2
3namespace ZlibF.Spec.Api.Proofs
4
5private def switched : GzHandle := { gzR with mode := .write }
6
7/-- The seek relation permits the returned handle's mode to change. -/
8theorem seek_model_allows_mode_change : GzSeek gzR 0 0 0 switched := by
9  simp [GzSeek, GzHandle.tell, GzHandle.CopyMode, gzR, switched, Z.ok, Z.bufError]
10
11/-- The changed handle is then treated as a writer by the read relation. -/
12theorem read_model_after_mode_change : GzReadFn switched 1 [] (-1) switched := by
13  simp [GzReadFn, switched, gzR]
14
15/-- The existing seek/read goal is false for its current model relations. -/
16theorem gz_seek_read_false : ¬ Goal.gz_seek_read := by
17  intro goal
18  have h := goal gzR switched switched 0 0 0 1 [] (-1)
19    rfl rfl (by decide) (Or.inl rfl) seek_model_allows_mode_change (by decide)
20  have he := h.2 rfl read_model_after_mode_change
21  simp [gzR] at he
22
23#print axioms gz_seek_read_false
24end ZlibF.Spec.Api.Proofs