inspecting prop.1 and prop.2 in VS code

Stream: new members

[Nathan Glenn]

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]

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

[Johan Commelin]

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

[Jeremy Avigad]

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]

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]

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

[Patrick Massot]

Of course you can do that from the code itself.

[Nathan Glenn]

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]

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]

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

[Patrick Massot]

Default keybinding is F12

[Patrick Massot]

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

[Nathan Glenn]

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]

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]

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]

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

[Dan Stanescu]

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

[Dan Stanescu]

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

[Nathan Glenn]

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]

unfold is_an_inf_of at hx

[Kevin Buzzard]

waitwaitwait is_an_inf_of is just notation. Hang on

[Kevin Buzzard]

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]

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]

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]

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]

You can do both in one line.

[Nathan Glenn]

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]

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]

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

[Kevin Buzzard]

unfold is_inf is_max at hx works

[Patrick Massot]

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

[Nathan Glenn]

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

[Dan Stanescu]

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]

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