Token.lean

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

1import ZlibF.Spec.Format.Token
2
3/-!
4# Local tokens and the original Huffman-block grammar
5
6Successful tokens compose with, and are exposed by, the original Symbols
7constructors. Every token rejection contradicts that grammar using only
8determinism of the independent symbol and extra-bit functions.
9-/
10
11namespace ZlibF.Spec.Token
12
13/-- Each local success supplies exactly the corresponding original
14constructor, without requiring the unread suffix to be valid. -/
15theorem step_composes_symbols : Goal.step_composes_symbols := by
16  intro L D dict history input rest next finished token
17  cases token with
18  | literal decoded small =>
19    refine ⟨?_, ?_⟩
20    · intro impossible; cases impossible
21    · intro _ tail output continuation
22      exact Symbols.lit decoded small continuation
23  | copy decoded lower upper lengthRead distanceDecoded distanceBound distanceRead fits =>
24    refine ⟨?_, ?_⟩
25    · intro impossible; cases impossible
26    · intro _ tail output continuation
27      exact Symbols.copy decoded lower upper lengthRead distanceDecoded distanceBound distanceRead
28        (by simpa only [Nat.add_comm] using fits) continuation
29  | eob decoded =>
30    refine ⟨fun _ => ⟨rfl, Symbols.eob decoded⟩, ?_⟩
31    intro impossible; cases impossible
32
33/-- An original block derivation always begins with the same local token
34and either ends there or has the original grammar as its continuation. -/
35theorem symbols_exposes_step : Goal.symbols_exposes_step := by
36  intro L D dict history input tail output parsed
37  cases parsed with
38  | eob decoded =>
39    exact ⟨_, _, true, Step.eob decoded, Or.inl ⟨rfl, rfl, rfl⟩⟩
40  | lit decoded small continuation =>
41    exact ⟨_, _, false, Step.literal decoded small, Or.inr ⟨rfl, continuation⟩⟩
42  | copy decoded lower upper lengthRead distanceDecoded distanceBound distanceRead fits continuation =>
43    exact ⟨_, _, false,
44      Step.copy decoded lower upper lengthRead distanceDecoded distanceBound distanceRead
45        (by simpa only [Nat.add_comm] using fits), Or.inr ⟨rfl, continuation⟩⟩
46
47/-- The stated invalid-code and distance-bound reasons exclude every
48original block derivation, without a heap or table assumption. -/
49theorem rejected_has_no_symbols : Goal.rejected_has_no_symbols := by
50  intro L D dict history input rejected rest output parsed
51  cases rejected with
52  | length invalid =>
53    apply invalid []
54    cases parsed with
55    | eob decoded =>
56      exact ⟨256, _, by simpa only [List.append_nil] using decoded, by decide⟩
57    | lit decoded small continuation =>
58      exact ⟨_, _, by simpa only [List.append_nil] using decoded, by omega⟩
59    | copy decoded lower upper lengthRead distanceDecoded distanceBound distanceRead fits continuation =>
60      exact ⟨_, _, by simpa only [List.append_nil] using decoded, upper⟩
61  | distance decoded lower upper lengthRead invalid =>
62    cases parsed with
63    | eob decoded' =>
64      have same := (Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))).1
65      omega
66    | lit decoded' small continuation =>
67      have same := (Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))).1
68      omega
69    | copy decoded' lower' upper' lengthRead' distanceDecoded' distanceBound' distanceRead' fits continuation =>
70      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))
71      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (lengthRead.symm.trans lengthRead'))
72      apply invalid []
73      exact ⟨_, _, by simpa only [List.append_nil] using distanceDecoded', distanceBound'⟩
74  | tooFar decoded lower upper lengthRead distanceDecoded distanceBound distanceRead far =>
75    cases parsed with
76    | eob decoded' =>
77      have same := (Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))).1
78      omega
79    | lit decoded' small continuation =>
80      have same := (Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))).1
81      omega
82    | copy decoded' lower' upper' lengthRead' distanceDecoded' distanceBound' distanceRead' fits continuation =>
83      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (decoded.symm.trans decoded'))
84      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (lengthRead.symm.trans lengthRead'))
85      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (distanceDecoded.symm.trans distanceDecoded'))
86      obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Option.some.inj (distanceRead.symm.trans distanceRead'))
87      omega
88
89end ZlibF.Spec.Token