Formalizing expressiveness of line editors

According to Wikipedia, a line editor is a text editor in which each editing command applies to one or more complete lines of text designated by the user.

We will implement our own line editor in Coq, and then we will prove that it is a complete text editor.

The most known one is *nix’s ed. Here’s a demo interacting with it:

$ ed test.txt
> i
> Hello World!
> Line two
> .
> w
> q

With the command i we say we want to insert new lines, and we write the contents we want to insert. Adding a dot will stop insertion. w means write to the file and q means quit. Here’s another demo for reading and appending more text:

$ ed test.txt
22
> n
2	Line two
> 1
Hello World!
> n
1	Hello World!
> i
> Ahoy
> .
n
1	Ahoy
> 3
Line two
> d
> w
18
> q

The command n says “print the number of the current line along with contents”. If you input a number it will set the pointer to that line. Finally, d deletes a line.

Now, before we start formalizing things we have to agree on some definitions. Here’s one.

Definition: A text editor is complete if it has the options to insert, read, and change text at any position.

Digress a little bit, why bother with line editors when we can simply make a char editor? Well, it turns out that line editors are much more convenient than char editors. For example, it may be tricky to keep track of the position of every character to read/insert/delete.

Here’s another wild definition that we’ll have to accept:

Definition: Strings (list of characters) can be inserted (created), read, and changed.

Don’t get scared by “changed”, as in functional programming we’ll simply be returning new (updated) strings instead.

Finally,

Definition: A line editor contains a buffer. Buffer is simply a list of strings.

The definition of a line editor is simple. No, really. It can:

Read a line (get nth element of a list)
Insert a line (put an element in a list at a specific position)
Delete a line (get first nth elements of a list, skip n+1 elements of a list)

We wrap all of that in a single EditorEval to make it more convenient.

To formalize this complete text editor, we prove in Coq that:

Our line editor can insert any text, that is, $\forall s, n, b, (s \in insertLine( n, b, s ))$ for s – string, n – position, b – buffer
Our line editor can read any text, that is, $\forall s, n, b, (readLine(insertLine( n, b, s ), n) = s)$ for s – string, n – position, b – buffer
Our line editor can change any text, that is, $\exists f \forall s1, s2, n, b, f(readLine(insertLine( n, b, s ), n) = s1) \to (readLine(insertLine( n, b, s ), n) = s2)$ for s1, s2 – string, n – position, b – buffer. In the code, $f$ is defined as a combination of deletion and insertion.

Well, that’s about it. I learned how powerful line editors are, and also I did some programming in Coq again which I haven’t in some time.

The full source code available at https://github.com/bor0/misc/blob/master/2019/formal-ed. Note that my Coq skills are still at a beginner’s level. I used this cheatsheet together with a lot of asserts. 🙂