## Stream: new members

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

#### 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?

#### Johan Commelin (Jun 12 2020 at 13:53):

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

#### 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.

#### 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").

#### 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.

#### Patrick Massot (Jun 12 2020 at 14:00):

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

#### Patrick Massot (Jun 12 2020 at 14:00):

Of course you can do that from the code itself.

#### 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

#### 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?

#### 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.

#### Patrick Massot (Jun 12 2020 at 14:07):

Default keybinding is F12

#### 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

#### 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.

#### 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.

#### 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).

#### Nathan Glenn (Jun 12 2020 at 14:25):

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

#### 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?

#### Dan Stanescu (Jun 12 2020 at 14:49):

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

#### 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.

#### Kevin Buzzard (Jun 12 2020 at 17:11):

unfold is_an_inf_of at hx

#### Kevin Buzzard (Jun 12 2020 at 17:14):

waitwaitwait is_an_inf_of is just notation. Hang on

#### 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


#### 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.

#### 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.

#### 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


#### Patrick Massot (Jun 12 2020 at 17:20):

You can do both in one line.

#### 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.

#### 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:

#### Patrick Massot (Jun 12 2020 at 17:50):

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

#### Kevin Buzzard (Jun 12 2020 at 17:52):

unfold is_inf is_max at hx works

#### 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.

#### 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?

#### 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?

#### 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