show details of tactics

Stream: new members

[David Harvey]

hello, I have just installed lean + mathlib + vs code. I am working through 00_first_proof.lean in tutorial. There is an example lemma "unique_max" that invokes tactic "linarith". Is there a way to get vs code to show me what the tactic is actually doing? When I move my cursor past "linarith", it goes straight to "goals accomplished". In the source comments it suggests that linarith is using the lemma "le_antisymm", how can I see that lean decided to do this?

[Eric Wieser]

You can use show_term {linarith}

[Eric Wieser]

But you will likely get more than you bargained for

[Eric Wieser]

(docs#tactic.interactive.show_term)

[Kevin Buzzard]

Tactics like linarith typically generate huge proof terms which are not human-comprehensible. Why do you want to see what Lean did? Do you actually mean "how do I give a low-level proof"?

[David Harvey]

yes, I guess I want to understand how the proof was actually carried out

[David Harvey]

I tried putting show_term {linarith}, in a line before linarith, is that correct?

[David Harvey]

indeed I get unreadable output

[David Harvey]

or another to put my question: how did the author of the comments know that linarith invoked le_antisymm?

[David Harvey]

the text le_antisymm does not appear in that long output. Hmmm.

[David Harvey]

maybe this will all make sense to me after I play around a bit more...

[Kevin Buzzard]

linarith knows a ton of tricks for solving linear inequalities and it's not going to tell you which ones it used. If you want to prove the goal using le_antisymm instead and make a nicer proof term, feel free! If there's a goal of the form a=b and you have hypotheses a<=b and b<=a then you can be pretty sure that a tactic designed to solve a wide class of linear inequalities will use antisymmetry of <= at this point.

[Ruben Van de Velde]

Looking at https://github.com/leanprover-community/tutorials/blob/master/src/exercises/00_first_proofs.lean#L51 , it doesn't seem to say anything about le_antisymm in particular, though, does it? It generally doesn't make much sense to claim anything about what specific lemmas are used in the proof generated by a strong tactic, nor does it matter all that much

[Mario Carneiro]

It's almost certainly a simplification of the author to say that linarith invokes le_antisymm. It does something roughly like that, but there is a whole bunch of other preprocessing that it does that would probably make it hard to find the le_antisymm analogue in the result

[Mario Carneiro]

Looking at the result of:

import tactic.linarith

example (a b : ℚ) (h1 : a ≤ b) (h2 : b ≤ a) : a = b :=
by show_term { linarith }

it appears the le_antisymm analogue is the very first theorem application, docs#linarith.eq_of_not_lt_of_not_gt, which is basically le_antisymm combined with le_of_not_gt

[Patrick Massot]

Mario, as Ruben pointed out, the author didn't say that, it is David's interpretation.

[Patrick Massot]

The author wrote:

  -- Now we know `x ≤ y` and `y ≤ x`, and Lean shouldn't need more help.
  -- `linarith` proves equalities and inequalities that follow linearly from
  -- the assumption we have.

[David Harvey]

In the version I have, it says on line 105: In order to reach this stage, we need to know what "linarith" did for us. It invoked the lemma "le_antisymm" which says.... Anyway, thanks everyone I think you have clarified for me what is going on. I'm still at the stage that I don't understand what is the relationship between what is going on in the left hand panel and the right hand panel, I'm just trying to understand a bit more what is happening under the hood.

[Patrick Massot]

Oh indeed we weren't looking at the same place.

[Patrick Massot]

That line 105 is indeed a lie (for pedagogical purposes).

[Patrick Massot]

But inspecting what linarith actually did is definitely not the way you're meant to improve your understanding here.

[Patrick Massot]

I think you're trying to understand too much too early.

[Patrick Massot]

When you read in the zeroth file of a tutorial a sentence like

linarith proves equalities and inequalities that follow linearly from the assumption we have.

you're certainly not expected to start investigating the inner working of linarith.

[Kevin Buzzard]

If it's any help, I have no idea how linarith does what it does but I have a good understanding of which goals I can expect it to close.