Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
2.2 kB · 30 lines
12345678910111213141516171819202122232425262728293031# eukhe: the proof of LAW command_space_trailing## PROOF of LAW command_space_trailing: the names of a declared path q are# spaceless (cmd_wf), so the words of its line and a space are q and one# empty word (LSp.sp_words_render), and the words of its line are q# (LA.cb_words_render). The walk over q lands on q (the path with its# entry), and the empty word after it changes nothing (LSp.sp_walk_gap:# step.empty keeps a walk at a path), so both lines finish on the same# state.
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_trailing(t, q, ok, on): match q: case Nil{}: LLogicLogic.cb_absurd({Cmd.resolve(t, List.append(&2, Nat, Command.cmd_render(Nil{}), [32n])) == Cmd.resolve(t, Command.cmd_render(Nil{})) : 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)) %Equal.sym(List<&2, List<&2, Nat>>, Cmd.words(List.append(&2, Nat, Command.cmd_render(x <> rest), [32n])), x <> List.append(&2, List<&2, Nat>, rest, [Nil{}]), LSp.sp_words_render(x, rest, [32n], [Nil{}], hs, {==})) : {Cmd.finish(Cmd.walk(_, t, Cmd.Top{}), t) == Cmd.resolve(t, Command.cmd_render(x <> rest)) : Cmd.Res} %Equal.sym(Cmd.St, Cmd.walk(List.append(&2, List<&2, Nat>, x <> rest, [Nil{}]), t, Cmd.Top{}), Cmd.walk(List.append(&2, List<&2, Nat>, x <> rest, Nil{}), t, Cmd.Top{}), LSp.sp_walk_gap(t, x <> rest, Nil{}, k, o)) : {Cmd.finish(_, t) == Cmd.resolve(t, Command.cmd_render(x <> rest)) : Cmd.Res} %Equal.sym(List<&2, List<&2, Nat>>, List.append(&2, List<&2, Nat>, x <> rest, Nil{}), x <> rest, LA.cb_app_nil(List<&2, Nat>, x <> rest)) : {Cmd.finish(Cmd.walk(_, t, Cmd.Top{}), t) == Cmd.resolve(t, Command.cmd_render(x <> rest)) : Cmd.Res} %Equal.sym(List<&2, List<&2, Nat>>, Cmd.words(Command.cmd_render(x <> rest)), x <> rest, LA.cb_words_render(x, rest, hs)) : {Cmd.finish(Cmd.walk(x <> rest, t, Cmd.Top{}), t) == Cmd.finish(Cmd.walk(_, t, Cmd.Top{}), t) : Cmd.Res} {==}