exact? and this

Stream: mathlib4

[Max Cairney-Leeming]

Hi, I'm doing a little course on lean4, and we think we might have found a bug in one of our exercises: the two examples below should work identically, but line 18 (the last this in the first example) produces an error, even though exact? suggested exactly this code - in the second example I explicitly named the hypotheses along the way, and then there isn't an error

 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.LibrarySearch

example (x: ℝ)  (x_pos : x > 0):
  x + 1/x ≥ 2 :=
by
  have : (x-1)^2 ≥ 0
  · exact sq_nonneg (x-1)
  have : x^2 + 1 -2 *x ≥ 0
  · convert this
    ring
  have : x^2 + 1 ≥ 2 *x
  · exact Iff.mp sub_nonneg this
  have : (x^2 + 1)/x ≥ 2 * x /x
  · exact Iff.mpr (div_le_div_right x_pos) this
  have : (x^2 + 1)/x ≥ 2
  · exact Iff.mpr (le_div_iff x_pos) this -- <- what exact? suggested
  sorry



example (x: ℝ)  (x_pos : x > 0):
  x + 1/x ≥ 2 :=
by
  have h1: (x-1)^2 ≥ 0
  · exact sq_nonneg (x-1)
  have h2 : x^2 + 1 -2 *x ≥ 0
  · convert h1
    ring
  have h3 : x^2 + 1 ≥ 2 *x
  · exact Iff.mp sub_nonneg h2
  have h4: (x^2 + 1)/x ≥ 2 * x /x
  · exact Iff.mpr (div_le_div_right x_pos) h3
  have : (x^2 + 1)/x ≥ 2
  · exact Iff.mpr (le_div_iff x_pos) h3
  sorry

(also on the web version: https://lean.math.hhu.de/#code=%20import%20Mathlib.Data.Real.Basic%0A%20import%20Mathlib.Tactic.FieldSimp%0A%20import%20Mathlib.Tactic.LibrarySearch%0A%0Aexample%20(x%3A%20%E2%84%9D)%20%20(x_pos%20%3A%20x%20%3E%200)%3A%0A%20%20x%20%2B%201%2Fx%20%E2%89%A5%202%20%3A%3D%0Aby%0A%20%20have%20%3A%20(x-1)%5E2%20%E2%89%A5%200%0A%20%20%C2%B7%20exact%20sq_nonneg%20(x-1)%0A%20%20have%20%3A%20x%5E2%20%2B%201%20-2%20*x%20%E2%89%A5%200%0A%20%20%C2%B7%20convert%20this%0A%20%20%20%20ring%0A%20%20have%20%3A%20x%5E2%20%2B%201%20%E2%89%A5%202%20*x%20%0A%20%20%C2%B7%20exact%20Iff.mp%20sub_nonneg%20this%0A%20%20have%20%3A%20(x%5E2%20%2B%201)%2Fx%20%E2%89%A5%202%20*%20x%20%2Fx%0A%20%20%C2%B7%20exact%20Iff.mpr%20(div_le_div_right%20x_pos)%20this%0A%20%20have%20%3A%20(x%5E2%20%2B%201)%2Fx%20%E2%89%A5%202%20%0A%20%20%C2%B7%20exact%20Iff.mpr%20(le_div_iff%20x_pos)%20this%0A%20%20sorry%0A%0A%0A%20%20%0Aexample%20(x%3A%20%E2%84%9D)%20%20(x_pos%20%3A%20x%20%3E%200)%3A%0A%20%20x%20%2B%201%2Fx%20%E2%89%A5%202%20%3A%3D%0Aby%0A%20%20have%20h1%3A%20(x-1)%5E2%20%E2%89%A5%200%0A%20%20%C2%B7%20exact%20sq_nonneg%20(x-1)%0A%20%20have%20h2%20%3A%20x%5E2%20%2B%201%20-2%20*x%20%E2%89%A5%200%0A%20%20%C2%B7%20convert%20h1%0A%20%20%20%20ring%0A%20%20have%20h3%20%3A%20x%5E2%20%2B%201%20%E2%89%A5%202%20*x%20%0A%20%20%C2%B7%20exact%20Iff.mp%20sub_nonneg%20h2%0A%20%20have%20h4%3A%20(x%5E2%20%2B%201)%2Fx%20%E2%89%A5%202%20*%20x%20%2Fx%0A%20%20%C2%B7%20exact%20Iff.mpr%20(div_le_div_right%20x_pos)%20h3%0A%20%20have%20%3A%20(x%5E2%20%2B%201)%2Fx%20%E2%89%A5%202%20%0A%20%20%C2%B7%20exact%20Iff.mpr%20(le_div_iff%20x_pos)%20h3%0A%20%20sorry%0A%0A)

[Max Cairney-Leeming]

(also @Martin Dvořák , since he's teaching us this course and is also wondering what's gone wrong)

[Scott Morrison]

(No need to provide links to the web version: every code block has a button in the top right that takes you there!

[Scott Morrison]

Yes, this is a known problem. exact? can use all of the shadowed versions of this, yet when offering a suggestion it doesn't have a way of disambiguating for the human which one it used!

[Kevin Buzzard]

Actually exact? suggested exact Iff.mpr (le_div_iff x_pos) this✝, which will not work because this✝ is an inaccessible term

[Eric Wieser]

Not quite Kevin:

image.png

[Eric Wieser]

It suggested the ✝, but the try this removed it

[Kevin Buzzard]

We need to implement try this✝

[Kevin Buzzard]

@Max Cairney-Leeming a quick fix is exact Iff.mpr (le_div_iff x_pos) (by assumption) -- Lean is suggesting you use a term which doesn't have an (accessible) name, but by assumption will find it.

[Kevin Buzzard]

Another fix would be to not keep writing have : ... -- all you're doing here is naming more and more hypotheses this and when you have two hypotheses with the same name, you can't ever mention one of them again; its name is "lost". If you use this approach then the problem goes away:

example (x: ℝ)  (x_pos : x > 0):
  x + 1/x ≥ 2 :=
by
  have h1 : (x-1)^2 ≥ 0
  · exact sq_nonneg (x-1)
  have h2 : x^2 + 1 -2 *x ≥ 0
  · convert h1
    ring
  have h3 : x^2 + 1 ≥ 2 *x
  · exact Iff.mp sub_nonneg h2
  have h4 : (x^2 + 1)/x ≥ 2 * x /x
  · exact Iff.mpr (div_le_div_right x_pos) h3
  have h5 : (x^2 + 1)/x ≥ 2
  · exact? -- suggestion now works
  sorry

[Max Cairney-Leeming]

Ah, I see - it was being more clever than me, and ignoring one of my have blocks, so the simplest is just to remove the superfluous one

[Eric Wieser]

If you use haveI you get unique names for free (oh, this only worked in Lean 3)

[Michael Stoll]

Can "try this" use dot notation? I.e., (le_div_iff x_pos).mpr ... in place of Iff.mpr (le_div_iff x_pos) ....

[Kevin Buzzard]

Another issue with this work is that mathlib has essentially no lemmas about ≥, basically the symbol is banned in mathlib because it means the same thing as ≤ modulo a permutation of inputs. So you would find your life easier if you used ≤ everywhere.

[Thomas Murrills]

We could probably automate the fix! Replace any inaccessible names with ‹_› on whatever level is convenient, try that, and see if it works—otherwise be explicit with the type, and if that doesn't work, prepend something like rename_i with appropriate arguments and a unique name.

[Kevin Buzzard]

Here is how I teach my students to solve that kind of goal:

example (x: ℝ)  (x_pos : x > 0):
    x + 1/x ≥ 2 := by
  calc
  x + 1/x = 1/x * (x^2 + 1) := by field_simp; ring
  _       = 1/x * ((x - 1) ^ 2 + 2 * x) := by ring
  _       ≥ 1/x * (2 * x) := by gcongr; nlinarith
  _       = 2 := by field_simp

Note that I never used exact?, I never need to know the names of any lemmas, and the same few tactics do all the heavy lifting. I learnt this proof strategy from @Heather Macbeth (who also developed tactics to make this approach viable, and advocates for it in her undergrad Lean course).

[Thomas Murrills]

(Note that ‹_› is a shortcut for by assumption.)

[Scott Morrison]

Michael Stoll said:

Can "try this" use dot notation? I.e., (le_div_iff x_pos).mpr ... in place of Iff.mpr (le_div_iff x_pos) ....

attribute [pp_dot] Iff.mpr

[Scott Morrison]

tbh, I'm not sure why we don't already have that somewhere low down in Mathlib.

[Kevin Buzzard]

because it's now opt-in and we're still slowly opting everything in?

[Scott Morrison]

I would vote for

attribute [pp_dot] Iff.mpr Iff.mp False.elim Eq.symm Eq.trans

[Eric Wieser]

I'll use this as an excuse to plug #7239, which adds pp_dot to LinearMap.comp and LinearEquiv.comp too

[Kevin Buzzard]

but we can't just add it to *?

[Eric Wieser]

Eric Wieser said:

It suggested the ✝, but the try this removed it

@Scott Morrison, do you know if this is deliberate?

[Scott Morrison]

There's nothing about this in Try this.

[Scott Morrison]

More @[pp_dot]s in #7288.

[Eric Wieser]

What's the relationship between the two "Try this" messages in my screenshot?

[Thomas Murrills]

One (the logged info) is MessageData direct from syntax from an Expr (exact? doesn't use the default, turns out!), the other is pretty-printed into a Format then a string—I'm not exactly sure how MessageData gets pretty-printed, but I imagine the difference is in there somewhere.

[Scott Morrison]

The first one is generated from an Expr via delabToRefinableSyntax and then PrettyPrint.ppCategory. The second is generated by interpolating the Expr into a MessageData. It's in src#Std.Tactic.TryThis.addExactSuggestion

[Martin Dvořák]

Kevin Buzzard said:

Another issue with this work is that mathlib has essentially no lemmas about ≥, basically the symbol is banned in mathlib because it means the same thing as ≤ modulo a permutation of inputs. So you would find your life easier if you used ≤ everywhere.

Yeah, I am definitely guilty of this. In my defense, I tested (before my class) that everything worked with ≥ and I opted for it because reading x + 1/x ≥ 2 is better than reading 2 ≤ x + 1/x for my mental model.

[Martin Dvořák]

Scott Morrison said:

Yes, this is a known problem. exact? can use all of the shadowed versions of this, yet when offering a suggestion it doesn't have a way of disambiguating for the human which one it used!

In my personal opinion, tactics like exact? should work only with accessible terms.
I avoid shadowing most of the time, and when I do shadow something, it is absolutely deliberate.

[Kevin Buzzard]

Martin Dvořák said:

Kevin Buzzard said:

Another issue with this work is that mathlib has essentially no lemmas about ≥, basically the symbol is banned in mathlib because it means the same thing as ≤ modulo a permutation of inputs. So you would find your life easier if you used ≤ everywhere.

Yeah, I am definitely guilty of this. In my defense, I tested (before my class) that everything worked with ≥ and I opted for it because reading x + 1/x ≥ 2 is better than reading 2 ≤ x + 1/x for my mental model.

This was somewhat of an issue in Lean 3 but to be honest I'm just repeating the mantra here -- my tactic proof didn't seem to care at all that the inequalities were "the wrong way around". It might be the case that we can get away with more in Lean 4; one reason I tried the tactic proof without reversing the inequality (which was my instinct) was to see if it worked, and it worked first time.

[Ruben Van de Velde]

Martin Dvořák said:

Scott Morrison said:

Yes, this is a known problem. exact? can use all of the shadowed versions of this, yet when offering a suggestion it doesn't have a way of disambiguating for the human which one it used!

In my personal opinion, tactics like exact? should work only with accessible terms.
I avoid shadowing most of the time, and when I do shadow something, it is absolutely deliberate.

I'm on the other side of the fence here: there's a good chance when using exact? that I don't know exactly what hypotheses I need (LE vs LT, for example), so I might throw in have := h1.le; have := h2.le; ... before the call. It would be unnecessarily annoying to have to give those all unique names

[Martin Dvořák]

Would you also scale it up for more than one shadowing?
For example, is Try this: exact foo this✝¹ a valid thing for exact? to suggest?

[Ruben Van de Velde]

Something like by assumption would be better, but I actually would prefer this✝¹ over this, because that makes it more obvious what's wrong and which assumption it used

[Martin Dvořák]

Ruben Van de Velde said:

I'm on the other side of the fence here: there's a good chance when using exact? that I don't know exactly what hypotheses I need (LE vs LT, for example), so I might throw in have := h1.le; have := h2.le; ... before the call.

I am on my side of the fence for a reason.

I never use unnamed have because I am too lazy to write down a name.
FYI, you can always let your cat run over the keyboards and, if given have happens to be actually useful, you can properly name it later.

My laziness comes into the picture in a different manner:
I intentionally use shadowing when I am too lazy to write clear this and continue with a fresh identifier.

[Scott Morrison]

I'm unconvinced as yet, and don't intend to change exact? to not use shadowed hypotheses.

[Martin Dvořák]

Kevin Buzzard said:

This was somewhat of an issue in Lean 3 but to be honest I'm just repeating the mantra here -- my tactic proof didn't seem to care at all that the inequalities were "the wrong way around". It might be the case that we can get away with more in Lean 4; one reason I tried the tactic proof without reversing the inequality (which was my instinct) was to see if it worked, and it worked first time.

Unfortunately, that are still situations where Lean 4 cares whether I write b ≤ a or a ≥ b there.
Could a ≥ b be defined as a syntactic sugar for b ≤ a that gets replaced by the compiler before elaboration?

Are there any mathematical structures where we don't want b ≤ a and a ≥ b to be definitionally equivalent?
I hope not...

[Mario Carneiro]

it could, but that's not how it is defined right now

[Mario Carneiro]

For example $ and <| are defined as macros which expand to applications, so you never have to deal with downstream consequences of using one over the other

[Mario Carneiro]

one drawback of using macro expansion for ≥ is that if you write that your goal is a ≥ b it will be pretty printed as |- b ≤ a

[Mario Carneiro]

my guess is that this is the main reason it is an abbrev instead of a macro

[Martin Dvořák]

Makes sense.

[Martin Dvořák]

Ruben Van de Velde said:

Something like by assumption would be better

It would be for exact this✝¹ but not for exact foo this✝¹ as I wrote.

[Ruben Van de Velde]

Why not? What's wrong with exact foo (by assumption)?

[Matthew Pocock]

Kevin Buzzard said:

Another issue with this work is that mathlib has essentially no lemmas about ≥, basically the symbol is banned in mathlib because it means the same thing as ≤ modulo a permutation of inputs. So you would find your life easier if you used ≤ everywhere.

Should there not be a high priority simp set that normalizes all gt and ge to the lt and lte forms?

[Kyle Miller]

Kevin Buzzard said:

but we can't just add it to *?

No, not the way it's implemented unfortunately (I'll spare you the details). Something that requires human intervention is checking that whatever you add pp_dot to has its first explicit argument being the thing that gets the dot notation.

I think making it be more reliable and global would need more help from the core pretty printer for function applications.

[Martin Dvořák]

Kevin Buzzard said:

Here is how I teach my students to solve that kind of goal:

example (x: ℝ)  (x_pos : x > 0):
    x + 1/x ≥ 2 := by
  calc
  x + 1/x = 1/x * (x^2 + 1) := by field_simp; ring
  _       = 1/x * ((x - 1) ^ 2 + 2 * x) := by ring
  _       ≥ 1/x * (2 * x) := by gcongr; nlinarith
  _       = 2 := by field_simp

Note that I never used exact?, I never need to know the names of any lemmas, and the same few tactics do all the heavy lifting. I learnt this proof strategy from Heather Macbeth (who also developed tactics to make this approach viable, and advocates for it in her undergrad Lean course).

I am really conflicted on whether to show calc to beginners.
The clear advantage is that calc proofs read really nicely.
A disadvantage is that, when writing a calc proof, there is a long time between having a syntactically-correct code before writing the calculation and having a syntactically-correct code again. Or is there a shortcut in VS Code that would generate a calc template?

[Kevin Buzzard]

Yes, when I was a beginner this put me off calc a lot. However I think the syntax is now easier in Lean 4 and, even better, check out Patrick's recent video on the community website (the calc part is here) and also a recent gif he posted to see some really good new ways of interacting with calc. Unfortunately they're not yet in master, but they're well on the way.

[Kevin Buzzard]

@Patrick Massot annoyingly I can't find that gif you posted recently where you were showing off several new widget-related things including calc bells and whistles.

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Select.20and.20insert.20widgets/near/391992032

[Martin Dvořák]

Kevin Buzzard said:

Yes, when I was a beginner this put me off calc a lot. However I think the syntax is now easier in Lean 4 and, even better, check out Patrick's recent video on the community website (...)

Oh, that's really neat! I love how it generates the calc lines with the correct syntax!

[Heather Macbeth]

Martin Dvořák said:

when writing a calc proof, there is a long time between having a syntactically-correct code before writing the calculation and having a syntactically-correct code again.

Martin Dvořák This was definitely an issue in Lean 3, but have you tried the Lean 4 version? Since this change last July partially finished calcs are syntactically correct.

[Thomas Murrills]

I've been thinking a little bit about how to solve this, since exact? isn't the only time we'll want to use suggestions involving inaccessible hypotheses.

Thomas Murrills said:

Replace any inaccessible names with ‹_› on whatever level is convenient, try that, and see if it works—otherwise be explicit with the type

The "type-explicit" version of this seems doable—just make an fvar delaborator which inserts ‹type›:

code

/- In the real deal we'd probably register an option and check for it, or use a scoped delaborator,
but that's a bit clunky to show on zulip -/
open Lean PrettyPrinter.Delaborator SubExpr in
@[delab fvar]
def delabInaccessible : Delab := whenPPOption (fun _ => true /- get option here -/) do
  let .fvar i ← getExpr | failure
  guard (← i.getUserName).isInaccessibleUserName
  -- only somewhat sure about the next two lines:
  let tStx ← withType delab
  `(‹$tStx›) >>= annotateCurPos

and then use that when delaborating. We could make it safer by roundtripping the assumption in the middle, to make sure we get the fvarId back:

  let some j ← findLocalDeclWithType? t | failure
  guard <| i == j

but that's a lot of isDefEq checks, potentially.

I'm guessing we want the ability to insert ‹_› when possible, though, since some types might be very verbose. I'm not sure how to do this without roundtripping—we don't currently roundtrip the delaborated syntax in exact? suggestions (I'd guess because it's just too expensive). Maybe we could roundtrip only in cases where we need to check ‹_›.

Another option is to use some kind of elaborator which lets us access inaccessible names in the suggestion itself, but to have this elaborator suggest to replace itself with something better when inserted: with ‹_› if that works, ‹type› if necessary, or an English-language instruction to manually rename the hypothesis. (This elaborator would be banned from committed Mathlib code.) Do we have something like this already? (rename_i and rename are not what I'm thinking of—I'm thinking of something like (up to syntax) inaccessible% x which elaborates to the fvar which we see as x† in the infoview.)

[Kyle Miller]

I had also thinking about the possibility of making an elaborator that lets you refer to inaccessible names, but it would probably be better to have the exact? suggestion be something like rename_i x y z; exact foo. That way (1) it doesn't require custom elaboration/delaboration, (2) it doesn't require any fixing for mathlib, and (3) it's more likely to round trip than ‹_› (what if it's ‹Nat› and there are multiple Nats? or what if it's replacing an fvar that's in an argument that's solved by unification, causing ‹ty› to fail with a "no goals" once assumption finally gets called?)