LegalTrace.lean

1 import MachineTheory.LegalQuotient
2 import Mathlib.Data.Fintype.Basic
3 
4 /-!
5 # Preservation of legal finite executions
6 
7 Reviewed Core v0.2, Theorem 8.2, final clause. An execution returns the initial
8 state and every successor, or `none` if any requested action is disabled.
9 All statements quantify over arbitrary finite action lists. In particular, the
10 empty word retains the initial label. Encoded availability is not an assertion
11 of external moral or legal authority.
12 -/
13 
14 namespace Komorebi.MachineTheory.LegalQuotient
15 
16 universe u v w z
17 
18 variable {X : Type u} {Action : Type v} {Label : Type w} {Z : Type z}
19 
20 /-- Execute a word, retaining its initial state and all intermediate states.
21 `none` means that an action was disabled when it was reached. -/
22 def execute (M : System X Action Label) : X → List Action → Option (List X)
23   | x, [] => some [x]
24   | x, a :: word =>
25       (M.step x a).bind fun y => (execute M y word).map (x :: ·)
26 
27 @[simp] theorem execute_nil (M : System X Action Label) (x : X) :
28     execute M x [] = some [x] := rfl
29 
30 @[simp] theorem execute_cons (M : System X Action Label) (x : X)
31     (a : Action) (word : List Action) :
32     execute M x (a :: word) =
33       (M.step x a).bind (fun y => (execute M y word).map (x :: ·)) := rfl
34 
35 /-- A word is legal exactly when all requested successors exist. -/
36 def Legal (M : System X Action Label) (x : X) (word : List Action) : Prop :=
37   ∃ states, execute M x word = some states
38 
39 /-- The complete protected-label sequence, including the initial label. -/
40 def labels (M : System X Action Label) (x : X) (word : List Action) :
41     Option (List Label) :=
42   (execute M x word).map (List.map M.label)
43 
44 /-- The final state of a legal word, extracted from its complete state trace. -/
45 def endpoint (M : System X Action Label) (x : X) (word : List Action) : Option X :=
46   (execute M x word).bind List.getLast?
47 
48 @[simp] theorem labels_nil (M : System X Action Label) (x : X) :
49     labels M x [] = some [M.label x] := rfl
50 
51 theorem execute_cons_eq_some_iff (M : System X Action Label) (x : X)
52     (a : Action) (word : List Action) (states : List X) :
53     execute M x (a :: word) = some states ↔
54       ∃ y rest, M.step x a = some y ∧ execute M y word = some rest ∧
55         states = x :: rest := by
56   cases hs : M.step x a with
57   | none => simp [execute, hs]
58   | some y =>
59       cases he : execute M y word with
60       | none => simp [execute, hs, he]
61       | some rest => simp [execute, hs, he, eq_comm]
62 
63 theorem legal_cons_iff (M : System X Action Label) (x : X)
64     (a : Action) (word : List Action) :
65     Legal M x (a :: word) ↔ ∃ y, M.step x a = some y ∧ Legal M y word := by
66   constructor
67   · rintro ⟨states, hs⟩
68     obtain ⟨y, rest, hy, hr, _⟩ :=
69       (execute_cons_eq_some_iff M x a word states).mp hs
70     exact ⟨y, hy, rest, hr⟩
71   · rintro ⟨y, hy, rest, hr⟩
72     exact ⟨x :: rest, (execute_cons_eq_some_iff M x a word (x :: rest)).mpr
73       ⟨y, rest, hy, hr, rfl⟩⟩
74 
75 theorem execute_length (M : System X Action Label) (x : X)
76     (word : List Action) (states : List X)
77     (h : execute M x word = some states) : states.length = word.length + 1 := by
78   induction word generalizing x states with
79   | nil =>
80       have hs : states = [x] := (Option.some.inj h).symm
81       simp [hs]
82   | cons a word ih =>
83       obtain ⟨y, rest, _, hr, rfl⟩ :=
84         (execute_cons_eq_some_iff M x a word states).mp h
85       simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc] using
86         congrArg Nat.succ (ih y rest hr)
87 
88 theorem execute_head (M : System X Action Label) (x : X)
89     (word : List Action) (states : List X)
90     (h : execute M x word = some states) : states.head? = some x := by
91   cases word with
92   | nil =>
93       have hs : states = [x] := (Option.some.inj h).symm
94       simp [hs]
95   | cons a word =>
96       obtain ⟨_, rest, _, _, rfl⟩ :=
97         (execute_cons_eq_some_iff M x a word states).mp h
98       rfl
99 
100 /-- Every state in every finite legal execution is projected to its quotient
101 state. Illegal words remain illegal in both directions. -/
102 theorem Factors.execute_map {M : System X Action Label} {Q : System Z Action Label}
103     {π : X → Z} (h : Factors M Q π) (x : X) (word : List Action) :
104     execute Q (π x) word = (execute M x word).map (List.map π) := by
105   induction word generalizing x with
106   | nil => rfl
107   | cons a word ih =>
108       rw [execute_cons, execute_cons, h.step_map x a]
109       cases hs : M.step x a with
110       | none => rfl
111       | some y =>
112           simp only [Option.map_some, Option.bind_some]
113           rw [ih]
114           cases execute M y word <;> rfl
115 
116 theorem Factors.execute_eq_some {M : System X Action Label}
117     {Q : System Z Action Label} {π : X → Z} (h : Factors M Q π)
118     (x : X) (word : List Action) (states : List X)
119     (hs : execute M x word = some states) :
120     execute Q (π x) word = some (states.map π) := by
121   rw [h.execute_map, hs]
122   rfl
123 
124 theorem Factors.endpoint_map {M : System X Action Label}
125     {Q : System Z Action Label} {π : X → Z} (h : Factors M Q π)
126     (x : X) (word : List Action) :
127     endpoint Q (π x) word = (endpoint M x word).map π := by
128   unfold endpoint
129   rw [h.execute_map]
130   cases execute M x word with
131   | none => rfl
132   | some states =>
133       simp only [Option.map_some, Option.bind_some, List.getLast?_map]
134 
135 /-- Legality is reflected as well as preserved. -/
136 theorem Factors.legal_iff {M : System X Action Label} {Q : System Z Action Label}
137     {π : X → Z} (h : Factors M Q π) (x : X) (word : List Action) :
138     Legal Q (π x) word ↔ Legal M x word := by
139   unfold Legal
140   rw [h.execute_map]
141   cases execute M x word with
142   | none => simp
143   | some states => simp
144 
145 theorem Factors.label_trace {M : System X Action Label} {Q : System Z Action Label}
146     {π : X → Z} (h : Factors M Q π) (states : List X) :
147     (states.map π).map Q.label = states.map M.label := by
148   induction states with
149   | nil => rfl
150   | cons x states ih => simp only [List.map_cons, ← h.label_eq, ih]
151 
152 /-- Equality covers every intermediate label, with `none` detecting every
153 illegal request. It is stronger than equality of final observations. -/
154 theorem Factors.labels_eq {M : System X Action Label} {Q : System Z Action Label}
155     {π : X → Z} (h : Factors M Q π) (x : X) (word : List Action) :
156     labels Q (π x) word = labels M x word := by
157   unfold labels
158   rw [h.execute_map]
159   cases execute M x word with
160   | none => rfl
161   | some states =>
162       simp only [Option.map_some]
163       exact congrArg some (h.label_trace states)
164 
165 /-- A quotient trace can be lifted from any chosen representative of its
166 initial state, without changing the action word or protected labels. -/
167 theorem Factors.lift_execution {M : System X Action Label}
168     {Q : System Z Action Label} {π : X → Z} (h : Factors M Q π)
169     (x : X) (word : List Action) (quotientStates : List Z)
170     (hq : execute Q (π x) word = some quotientStates) :
171     ∃ states, execute M x word = some states ∧ states.map π = quotientStates ∧
172       states.map M.label = quotientStates.map Q.label := by
173   have hl : Legal Q (π x) word := ⟨quotientStates, hq⟩
174   obtain ⟨states, hs⟩ := (h.legal_iff x word).mp hl
175   have hp : states.map π = quotientStates :=
176     Option.some.inj ((h.execute_eq_some x word states hs).symm.trans hq)
177   exact ⟨states, hs, hp, by rw [← hp]; exact (h.label_trace states).symm⟩
178 
179 /-- Exact source-facing finite-state and finite-alphabet clause of Core 8.2.
180 The generic result above does not require finiteness. -/
181 theorem finite_legal_quotient_sequences [Finite X] [Finite Action]
182     {M : System X Action Label} {Q : System Z Action Label} {π : X → Z}
183     (h : Factors M Q π) (x : X) (word : List Action) :
184     (Legal Q (π x) word ↔ Legal M x word) ∧
185       execute Q (π x) word = (execute M x word).map (List.map π) ∧
186       labels Q (π x) word = labels M x word :=
187   ⟨h.legal_iff x word, h.execute_map x word, h.labels_eq x word⟩
188 
189 end Komorebi.MachineTheory.LegalQuotient

Back to source controls