lean for coq users?

Stream: new members

[Pedro Minicz]

Hello, is there a Lean introduction aimed at Coq users?

[Mario Carneiro]

There is a lean/coq cheat sheet although it is pretty dated

[Mario Carneiro]

https://github.com/jldodds/coq-lean-cheatsheet

[Pedro Minicz]

Thank you very much! Can I have Lean on VSCode behave like CoqIDE, that is, instead of having the goal screen follow the cursor, manually go forward command by command?

[Heather Macbeth]

Pedro Minicz said:

Thank you very much! Can I have Lean on VSCode behave like CoqIDE, that is, instead of having the goal screen follow the cursor, manually go forward command by command?

Thanks for asking this, I also would like to know this ...

[Reid Barton]

I don't use vscode but I think there's a button with "freeze" in its name that maybe you can use to stop the goal window from changing when you move the cursor?

[Pedro Minicz]

Yes, indeed, there is a freeze function! However it seems much less convenient than having shortcuts to step through the proof.

[Reid Barton]

That shortcut is pressing the :down: key :slight_smile:

[Reid Barton]

I must be failing to imagine the use case which is not covered by one of these two

[Pedro Minicz]

It is mostly a matter of convenience, or getting used to. Maybe some trickery with multiple cursors could be attempted, if VSCode supports it.

[Reid Barton]

I think normal usage is to never use the freeze button--I use emacs which doesn't have an equivalent feature as far as I know.

[Patrick Massot]

Thank you very much! Can I have Lean on VSCode behave like CoqIDE, that is, instead of having the goal screen follow the cursor, manually go forward command by command?

@Pedro Minicz @Heather Macbeth I would really love to understand where this question come from. Coq's iron curtain moving up and down the proof is one of the first thing I mention when explaining how Lean is more user friendly than Coq, sometimes even before the general use of unicode. And I've never met any Coq user defending that. Usually people mumble there is some extension somewhere which fixes this issue in Coq but it's no longer compatible with current Coq (this is general theme with what I've seen from Coq: there are so many people hacking it that almost every issue has been fixed by someone but there aren't any pair of fixes that are compatible). What do you do with the iron curtain that you cannot do with your up and down arrow key in Lean? Do you know you can even use left and right arrows in Lean to have a finer view of the proof state, for instance in case of multiple rewriting in the same tactic invocation?

I have no difficulties imagining how trying another proof assistant can be frustrating, if only because your muscle memory keeps typing the wrong keywords or notation. And I know SSReflect has really nice tactics that Lean is missing. But I honestly have no idea why anyone would want the rigid curtain that prevents you from inspecting tactic state anywhere in your file without recompiling.

[Patrick Massot]

Is it something like https://xkcd.com/1172/ again?

[Mario Carneiro]

I was actually going to say that while I think the iron curtain is not something we should replicate, I have had use for a second cursor where I want to see the goal state (live). For instance if I'm adding lemmas to a simp[] call and I want to see the goal state at the end of the line, or perhaps two tactics later

[Johan Commelin]

Nothing a widget cannot solve, I guess.

[Johan Commelin]

@Edward Ayers will probably tell you he has already implemented this in some VScode plugin (-;

[Mario Carneiro]

I think it can be done in vscode, but not via widgets if I understand them correctly

[Patrick Massot]

This is definitely doable in the VScode extension without any change on the Lean side.

[Gabriel Ebner]

Mario Carneiro said:

I was actually going to say that while I think the iron curtain is not something we should replicate, I have had use for a second cursor where I want to see the goal state (live). For instance if I'm adding lemmas to a simp[] call and I want to see the goal state at the end of the line, or perhaps two tactics later

You are not the only one. https://github.com/leanprover/vscode-lean/issues/151

[Heather Macbeth]

@Patrick Massot It's basically what Mario said, I would like to easily keep the goal state from one line in view while changing a different line. It doesn't even need to be dynamic (though that would be awesome) -- is there a keyboard shortcut for "freeze display"?

[Bryan Gin-ge Chen]

Not by default, but you can add one by searching for "toggle updating" in VS Code's keyboard shortcuts.

[Heather Macbeth]

Great, thanks!

[Patrick Massot]

I must have missed something about that when I tried Coq, because the iron curtain thing looked like the opposite of dynamic.

[Patrick Massot]

By the way, I'm still very much interested in seeing your exercises.

[Heather Macbeth]

I will start a separate topic in #Lean for teaching , is that the polite thing to do on Zulip?

[Patrick Massot]

Sure. Great!

[Kevin Buzzard]

Heather Macbeth said:

Patrick Massot It's basically what Mario said, I would like to easily keep the goal state from one line in view while changing a different line. It doesn't even need to be dynamic (though that would be awesome) -- is there a keyboard shortcut for "freeze display"?

I don't understand -- does clicking the "pause" button not do exactly what you want here?

[Kevin Buzzard]

pause.png

[Kevin Buzzard]

I clicked the "pause" icon and it froze the Lean Goal window; I can restart with the "play" icon which I'm pointing out with my cursor. The cursor in the left hand window is at the bottom of the proof and I can type stuff there without the right hand window changing. @Heather Macbeth is that what you're looking for or have I misunderstood?

[Bryan Gin-ge Chen]

I think Heather was asking about a keyboard shortcut for the pause button, and as far as I understand she managed to set one up.

[Pedro Minicz]

@Patrick Massot I like the flexibility that Lean gives for inspecting the proof state. However, I would prefer to have inspecting the proof state and editing/navigating around the code as separate actions.

@Mario Carneiro gives one example where this would be useful. Another would be not having unknown identifier errors while typing. While this could be fixed by adding more "intelligence" to Lean/the VSCode plugin, I would rather be able to control where the "proof state cursor" is myself.

[Kevin Buzzard]

Why can this not be solved with the "pause" button?

[Pedro Minicz]

Indeed, the pause button and @Bryan Gin-ge Chen's suggestion are viable solutions.

[Mario Carneiro]

@Heather Macbeth @Pedro Minicz I recently made a PR vscode-lean#158 that should give you some of this flexibility. The way it works is you trigger the "Toggle Sticky Position" command, and then it drops a mark in your code where the goal state will now be reported rather than at the cursor. Unlike Coq's iron curtain, it is live updating, although if you put the mark far below the cursor it might take a while to get feedback since you have to wait for those orange bars to clear first.