Zulip Chat Archive

Stream: new members

Topic: inspecting prop.1 and prop.2 in VS code


view this post on Zulip Nathan Glenn (Jun 12 2020 at 13:16):

Hi, I'm just working through the tutorial in VS code. I'm having difficulty getting introspection on some of the code used in lemmas. Particularly I'm looking at the inf_lt lemma, which uses hx.2. The Lean Goal window shows the value of hx, but it isn't expanded so the user can't tell what the 1 and 2 cases are. Is there are way to inspect these values in VS code?

view this post on Zulip Johan Commelin (Jun 12 2020 at 13:53):

What do you mean with "it isn't expanded"?

view this post on Zulip Johan Commelin (Jun 12 2020 at 13:53):

@Nathan Glenn (I didn't look at the file.) I guess hx : p \and q? and then hx.1 has type p.

view this post on Zulip Jeremy Avigad (Jun 12 2020 at 13:55):

Or if it is p ↔ q then hx.1 is the forward direction (aka hx.mp, for "modus ponens") and hx.2 is the reverse direction (also known as hx.mpr for "modus ponens reverse").

view this post on Zulip Nathan Glenn (Jun 12 2020 at 13:59):

by "it isn't expanded" I mean that it is shown as x is_an_inf_of A in the goals panel, and looking just at this string it is not possible to tell there are cases; you have to go find the definition of is_an_inf_of and search backwards from there.

view this post on Zulip Patrick Massot (Jun 12 2020 at 14:00):

You currently cannot do that from the goal view, but it should come soon.

view this post on Zulip Patrick Massot (Jun 12 2020 at 14:00):

Of course you can do that from the code itself.

view this post on Zulip Nathan Glenn (Jun 12 2020 at 14:03):

ooh, sounds promising! Where do the developer people hang out and discuss features being worked on? If I were to contribute, it would probably have to be there, not with the math definitions part

view this post on Zulip Nathan Glenn (Jun 12 2020 at 14:04):

By "do that from the code itself" you mean search around in VS code, or do you mean that there are commands that you can do?

view this post on Zulip Patrick Massot (Jun 12 2020 at 14:06):

In VSCode you can right-click on everything and choose "Go to definition" in the contextual menu.

view this post on Zulip Patrick Massot (Jun 12 2020 at 14:07):

Default keybinding is F12

view this post on Zulip Patrick Massot (Jun 12 2020 at 14:08):

About the coming stuff, I think the main entry point here is https://github.com/leanprover/vscode-lean/pull/159

view this post on Zulip Nathan Glenn (Jun 12 2020 at 14:16):

Ah, the "Go to definition" functionality is I think the problem here. The line exact hx.2 y h takes you to the definition of the exact tactic, no matter where your cursor is. A separate issue is that it's not possible to go to definitions of propositions shown in the goals window.

view this post on Zulip Bryan Gin-ge Chen (Jun 12 2020 at 14:19):

The former is known (and frustrating). I think it's tricky to fix due to the way the tactic parser works, but feel free to open an issue here.

The latter should be coming hopefully not too long after the info view refactor lands.

view this post on Zulip Bryan Gin-ge Chen (Jun 12 2020 at 14:22):

Nathan Glenn said:

ooh, sounds promising! Where do the developer people hang out and discuss features being worked on? If I were to contribute, it would probably have to be there, not with the math definitions part

Most Lean-related discussion (whether mathematical or programming-related) occurs in this Zulip. Feel free to open threads about anything you're curious about (after searching "all public streams" on Zulip, of course).

view this post on Zulip Nathan Glenn (Jun 12 2020 at 14:25):

Thanks! I will eagerly await the new UI, then :)

view this post on Zulip Dan Stanescu (Jun 12 2020 at 14:46):

@Nathan Glenn I don't remember, have you been made aware of the unfold tactic at this point in the tutorials?

view this post on Zulip Dan Stanescu (Jun 12 2020 at 14:49):

You should be able to apply it to, i.e.,is_an_inf_of.

view this post on Zulip Nathan Glenn (Jun 12 2020 at 17:09):

Sounds promising! Okay, so I'm in tutorial 0, lemma inf_lt. If I type unfold hx, I get unfold tactic failed, hx does not have equational lemmas nor is a projection. :thinking: The documentation says that unfold unfolds constants at their appearances in the goal, but I need to look at things that aren't necessarily in the goal. hx is just another state variable in this case.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:11):

unfold is_an_inf_of at hx

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:14):

waitwaitwait is_an_inf_of is just notation. Hang on

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:16):

I don't know how to do this. I can just look at the definitions and see what the answer is, but I am struggling to get Lean to unfold it. The situation is:

hx : x is_an_inf_of A,
infix `is_an_inf_of`:55 := is_inf
def is_inf (x : ) (A : set ) := x is_a_max_of (low_bounds A)
infix `is_a_max_of`:55 := is_max
def is_max (a : ) (A : set ) := a  A  a  up_bounds A

view this post on Zulip Patrick Massot (Jun 12 2020 at 17:17):

Yes, it looks nice in the demo and when you know what you are doing, but it does make it more difficult to unfold since you need to know the actual name.

view this post on Zulip Patrick Massot (Jun 12 2020 at 17:18):

I usually do that only in pure demo files. I also use this zeroth tutorial file to show Lean to people who don't intend to ever use it.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:18):

So the infix stuff is notation, which Lean can see through. So the answer to your question @Nathan Glenn is

  unfold is_inf at hx,
  unfold is_max at hx,

giving

A : set ,
x y : ,
h :  (a : ), a  A  y  a,
hx : x  low_bounds A  x  up_bounds (low_bounds A)
 y  x

view this post on Zulip Patrick Massot (Jun 12 2020 at 17:20):

You can do both in one line.

view this post on Zulip Nathan Glenn (Jun 12 2020 at 17:39):

That worked great, thanks Kevin!
I was hoping then that I could replace those two lines with something like repeat {unfold (whatever) at hx} but that doesn't work. I guess it would probably explode the goals once the structures got more complex, anyway.

view this post on Zulip Nathan Glenn (Jun 12 2020 at 17:44):

Patrick Massot said:

I also use this zeroth tutorial file to show Lean to people who don't intend to ever use it.

So maybe I should start with tutorial 1? :joy:

view this post on Zulip Patrick Massot (Jun 12 2020 at 17:50):

No, I mean you're not really meant to edit that zeroth file.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:52):

unfold is_inf is_max at hx works

view this post on Zulip Patrick Massot (Jun 12 2020 at 17:54):

Sure, although it's annoying that this is not consistent with the simp/dsimp and rw syntax.

view this post on Zulip Nathan Glenn (Jun 12 2020 at 17:57):

Ah okay, so the zeroth file is like an overview that I should read through and move on with?

view this post on Zulip Dan Stanescu (Jun 12 2020 at 18:22):

Kevin Buzzard said:

unfold is_inf is_max at hx works

Since is_an_inf_of is notation (that Lean has been made aware of) for is_inf, maybe we could ask that Lean unfold it without digging any further (i.e without knowledge of is_inf for the user). Does this seem like a reasonable feature request for the unfold tactic?

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:42):

In some sense it's unfolded already. I think it's the prettyprinter which is making it not display as is_inf. If you set_option pp.notation false you can see what's really going on


Last updated: May 14 2021 at 22:15 UTC