Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
2.3 kB · 30 lines
12345678910111213141516171819202122232425262728293031# eukhe: the proof of LAW command_space_gap## PROOF of LAW command_space_gap: the names of a declared path q are# spaceless (cmd_wf), so the words of its line, a space and text are q# and the words of the text after the space (LSp.sp_words_render); a# second space adds one empty word between them. The walk over q lands# on q (the path with its entry), where the empty word changes nothing# (LSp.sp_walk_gap: step.empty keeps a walk at a path), so the rest of# the walk, and what the line resolves to, is the same.
import Baseimport ../../bend/command.bend as Cmdimport ../../laws/command/paths.bend as Commandimport ../base/logic/logic.bend as LLogicLogicimport ./base.bend as LAimport ./base/space.bend as LSp
def Command.command_space_gap(t, q, line, ok, on): match q: case Nil{}: LLogicLogic.cb_absurd({Cmd.resolve(t, List.append(&2, Nat, Command.cmd_render(Nil{}), 32n <> 32n <> line)) == Cmd.resolve(t, List.append(&2, Nat, Command.cmd_render(Nil{}), 32n <> line)) : Cmd.Res}, on) case Con{+x, +rest}: +k = ok +o = on +hs = LA.cb_names_spaceless(x <> rest, LA.cb_walks_names(t, x <> rest, k, o)) +w = Cmd.words(line) %Equal.sym(List<&2, List<&2, Nat>>, Cmd.words(List.append(&2, Nat, Command.cmd_render(x <> rest), 32n <> 32n <> line)), x <> List.append(&2, List<&2, Nat>, rest, Nil{} <> w), LSp.sp_words_render(x, rest, 32n <> 32n <> line, Nil{} <> w, hs, {==})) : {Cmd.finish(Cmd.walk(_, t, Cmd.Top{}), t) == Cmd.resolve(t, List.append(&2, Nat, Command.cmd_render(x <> rest), 32n <> line)) : Cmd.Res} %Equal.sym(List<&2, List<&2, Nat>>, Cmd.words(List.append(&2, Nat, Command.cmd_render(x <> rest), 32n <> line)), x <> List.append(&2, List<&2, Nat>, rest, w), LSp.sp_words_render(x, rest, 32n <> line, w, hs, {==})) : {Cmd.finish(Cmd.walk(x <> List.append(&2, List<&2, Nat>, rest, Nil{} <> w), t, Cmd.Top{}), t) == Cmd.finish(Cmd.walk(_, t, Cmd.Top{}), t) : Cmd.Res} %Equal.sym(Cmd.St, Cmd.walk(List.append(&2, List<&2, Nat>, x <> rest, Nil{} <> w), t, Cmd.Top{}), Cmd.walk(List.append(&2, List<&2, Nat>, x <> rest, w), t, Cmd.Top{}), LSp.sp_walk_gap(t, x <> rest, w, k, o)) : {Cmd.finish(_, t) == Cmd.finish(Cmd.walk(x <> List.append(&2, List<&2, Nat>, rest, w), t, Cmd.Top{}), t) : Cmd.Res} {==}