Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
3.0 kB · 67 lines
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768# eukhe: the proof of LAW command_menu_space_lead## PROOF of LAW command_menu_space_lead: a line with a space has two or# more words (msl_words_two: a space starts a word after the words# before it, and the words of a line are never none), and a leading# space adds one empty first word. With two or more words the cut keeps# the first word, so the words before the last stay not none with or# without the empty word before them; the menu walks them from the root,# where the empty word changes nothing (step.empty of Top is Top), and# both menus compute to the same term.
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
# two or more wordsdef msl_two(ws: List<&2, List<&2, Nat>>) -> Bool: match ws: case Nil{}: False{} case Con{w, rest}: LSp.sp_ne(rest)
def msl_two_put(-c: Nat, ws: List<&2, List<&2, Nat>>, h: {msl_two(ws) == True{} : Bool}) -> {msl_two(Cmd.put_word(c, ws)) == True{} : Bool}: match ws: case Nil{}: LLogicLogic.cb_absurd({msl_two(Cmd.put_word(c, Nil{})) == True{} : Bool}, h) case Con{w, rest}: h
def msl_two_at(b: Bool, -c: Nat, r: List<&2, Nat>, h: {Bool.and(Bool.not(b), Command.cmd_spaceless(r)) == False{} : Bool}, ih: {Command.cmd_spaceless(r) == False{} : Bool} -> {msl_two(Cmd.words(r)) == True{} : Bool}) -> {msl_two(Cmd.words.at(b, c, Cmd.words(r))) == True{} : Bool}: match b: case True{}: LSp.sp_words_ne(r) case False{}: msl_two_put(c, Cmd.words(r), ih(h))
# a line with a space has two or more wordsdef msl_words_two(line: List<&2, Nat>, h: {Command.cmd_spaceless(line) == False{} : Bool}) -> {msl_two(Cmd.words(line)) == True{} : Bool}: match line: case Nil{}: LA.cb_absurd2({msl_two(Cmd.words(Nil{})) == True{} : Bool}, h) case Con{+c, +r}: msl_two_at(Nat.is_eq(c, 32n), c, r, h, e => msl_words_two(r, e))
def msl_pair(c: List<&2, List<&2, Nat>> & List<&2, Nat>, -a: List<&2, Nat>, +t: List<&2, Cmd.Ent>) -> {Cmd.menu.cut(Cmd.cut.cons(Nil{}, Cmd.cut.cons(a, c)), t) == Cmd.menu.cut(Cmd.cut.cons(a, c), t) : Cmd.Menu}: match c: case (d, p): {==}
# an empty first word before two or more words changes nothing the menudef msl_lead(ws: List<&2, List<&2, Nat>>, +t: List<&2, Cmd.Ent>, h: {msl_two(ws) == True{} : Bool}) -> {Cmd.menu.cut(Cmd.cut(Nil{} <> ws), t) == Cmd.menu.cut(Cmd.cut(ws), t) : Cmd.Menu}: match ws: case Nil{}: LLogicLogic.cb_absurd({Cmd.menu.cut(Cmd.cut([Nil{}]), t) == Cmd.menu.cut(Cmd.cut(Nil{}), t) : Cmd.Menu}, h) case Con{a, rest}: match rest: case Nil{}: LLogicLogic.cb_absurd({Cmd.menu.cut(Cmd.cut([Nil{}, a]), t) == Cmd.menu.cut(Cmd.cut([a]), t) : Cmd.Menu}, h) case Con{b, more}: msl_pair(Cmd.cut.go(more, b), a, t)
def Command.command_menu_space_lead(t, line, two): msl_lead(Cmd.words(line), t, msl_words_two(line, two))