{"version":3,"kind":"module","module":{"id":1,"user_id":"cef483b5-8f5a-40e6-b0b3-f82d7a8be13a","title":"Partial patch replay: definitions and concatenation law","namespace":"PatchReplay","description":"A reusable generic partial patch interpreter and named sequential concatenation lemma. Operations return Option State and failures propagate. This abstracts sequential replay and establishes no implementation refinement, network convergence or cost optimality.","profile":"core","declarations":[{"kind":"definition","name":"replay","type":"(State Op : Type) → (Op → State → Option State) → List Op → State → Option State","value":"fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)"},{"kind":"lemma","name":"concat","type":"∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (replay State Op step xs s)","value":"by\n  intro State Op step xs ys s\n  exact List.foldl_append"}],"module_pins":[],"module_context":[],"module_hash":"527d91c48d760214c5802af0f022008063b177251f485842f8234df651666143","status":"verified","check_log":"'_private.0.Hunch.PatchReplay.replay' does not depend on any axioms\n'_private.0.Hunch.PatchReplay.concat' depends on axioms: [propext, Quot.sound]\n'_private.0.OA_target' does not depend on any axioms\nOA_target : OA_statement","axioms":["propext","Quot.sound"],"created_at":1791444144,"checked_at":1791444158,"hidden_at":null,"secondary_status":"not_run","secondary_details":null,"origin_submission_id":null,"origin_source_hash":null},"problem":{"statement":"True","profile":"core","module_context":[],"module_pins":[],"module_declarations":[{"kind":"definition","name":"replay","type":"(State Op : Type) → (Op → State → Option State) → List Op → State → Option State","value":"fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)"},{"kind":"lemma","name":"concat","type":"∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (replay State Op step xs s)","value":"by\n  intro State Op step xs ys s\n  exact List.foldl_append"}],"namespace":"PatchReplay"},"profile":"core","policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","proof":"by trivial","statement_hash":"2a08c013e3b3f61442dc6bd1ee2a9959610c940d0ee05197817c74f0ebd13476","source":"import Init\n\nnamespace Hunch.PatchReplay\ndef replay : ((State Op : Type) → (Op → State → Option State) → List Op → State → Option State) :=\n  fun _ _ step ops s => ops.foldl (fun prior op => prior.bind (step op)) (some s)\n\ntheorem concat : (∀ (State Op : Type) (step : Op → State → Option State) (xs ys : List Op) (s : State), replay State Op step (xs ++ ys) s = ys.foldl (fun prior op => prior.bind (step op)) (replay State Op step xs s)) :=\n  by\n    intro State Op step xs ys s\n    exact List.foldl_append\n\nend Hunch.PatchReplay\n\ndef OA_statement : Prop := (True)\n\ntheorem OA_target : OA_statement :=\n  by trivial\n\n#print axioms Hunch.PatchReplay.replay\n#print axioms Hunch.PatchReplay.concat\n#print axioms OA_target\n#check OA_target\n"}