external interaction

Stream: general

[Alexandre Rademaker]

In http://logitext.mit.edu/main, Coq is used in background to manipulate the proof state. How hard would be to implement something similar with Lean4 ? For propositional logic first...

[Jason Rute]

I don't know about Lean4. Honestly I would ask in the #lean4 stream, so this gets more visibility by the right folks.

[Jason Rute]

But for Lean3, the answer is just to use the lean server. What you would be doing is essentially translating the sequent to Lean code and having lean check every step along the way. Lean can obviously represent first order logic, so either you use the built in tactics or make your own corresponding to the rules in the calculus. The process would be something like this. Your webpage backend starts the lean server lean --server, and sends it the string for a file dummy.lean to sync. This will will be our scratch pad. When the user wants to prove p -> p, we send an updated version of dummy.lean to sync:

example : p -> p :=
begin

end

Then when the user applies a rule, you put in the corresponding tactic into the file and sync again.

example : p -> p :=
begin
intro h,
end

At each stage you can check the error messages and the state to see where things are at.

[Jason Rute]

I wrote up an example of this in a python notebook here. The ideas are right, but I really should have been using asynchronous programming. The lean python client addresses that. (It however needs to have a PR merged to work properly again. It isn't on the top of anyones TODO list.)

[Jason Rute]

Of course there is no need to use Python. The lean server just communicates via JSON. Unfortunately, the interface isn't documented so that is why I suggest looking that those examples.

[Jason Rute]

Lean4 has (or will have) a server as well. It will be a really language server following the language server protocol if I recall. This is of course a hack of the language server, but it is a good hack since the use case is very similar to interactively editing a lean file.

[Alexandre Rademaker]

nice, thank you for your detailed explanation.

[Jason Rute]

Another approach is to directly program this in lean 3 or 4. The Lean program would be a read eval print loop which takes in a goal and then takes in instructions. You would have a (non-interactive) tactic which parses the instructions and applies the appropriate (non-interactive) lean tactics to the goal. If speed is your need, this would be much faster than using the language server, but otherwise you would just have to code up more I think. (In either case, 90% of the work would be translating your sequent calculus to Lean.)

[Bryan Gin-ge Chen]

I suspect an experienced Lean 3 widget hacker could cook something up that does at least some of what that example webpage does. Maybe someone in @Kevin Buzzard's discord?