Still struggling to understand tactics

Stream: lean4

[Avi Craimer]

I've been trying to read the docs and this section of the book: https://lean-lang.org/theorem_proving_in_lean4/tactics.html

I know this stuff is hard, and I'm coming at it from a programming background with some math background, but not as a pure mathematician. I'm not expecting it to be easy, by I find that I read the explanations of the tactics over and over again, but I still don't really understand what they are doing.

For example, in the docs for intro:
https://leanprover-community.github.io/mathlib4_docs/Init/Tactics.html#Lean.Parser.Tactic.intro

It says, "Introduces one or more hypotheses, optionally naming and/or pattern-matching them. For each hypothesis to be introduced, the remaining main goal's target type must be a let or function type."

That does not help me understand what it is doing. For one thing it offers a tautologous definition of "intro" using the word "introduction".

It goes on to say, "intro by itself introduces one anonymous hypothesis, which can be accessed by e.g. assumption."

Okay, so I guess it has something to do with introducing a logical assumption. But I don't understand what that means in the context, what sort of assumptions can be introduced (presumable not just any). And what does this mean concretely in terms of building a value of type Prop. e.g., under the hood is this adding an argument to a function?

Reflecting on this as I write, the difficulty is on two levels.

1. Understanding what the tactics are doing in the meta-layer of the tactics language
2. Understanding what the tactics are doing in relation to the basic type system and programming language constructs.

Of these, I think that understanding 2 would help me a lot more than 1. If I can relate the tactics to the underlying programming language constructs then I can probably figure out on my own how they relate to each other. I haven't found much documentation on this aspect of things.

Although understanding 1 is important too, and so far the documentation I've read has been impenetrable (to me). One thing that would be helpful would be something that explicitly relates the tactics to examples of what they are analogous to in terms of doing an informal mathematical proof with paper and pencil.

[Kyle Miller]

The tactic documentation is still a work-in-progress, and unfortunately you can't necessarily learn what a tactic does from its documentation. It's more a reference to remind you what it's supposed to do.

The intro x tactic by the way is equivalent to doing refine fun x => ?_. The ?_ creates a new goal in the context of the body of the fun, and refine is like exact but it allows creating new goals in this way.

[Kyle Miller]

intro also has a few extra features, like being able to do pattern matching, or being able to take more than one argument (which does an equivalent number of nested funs)

[Kyle Miller]

One useful tool if you're interested in what the tactics actually do, rather than being happy with observing how tactic states change tactic-by-tactic, is the show_term tactic (I think it's in the std library). If you do show_term intro x it will show you the term that the tactic produced. You can also do by? rather than by to see what a whole tactic block produced.

Before these tools existed, I would usually rely on the #print command; if you have a theorem foo you can do #print foo to see the term proof.

[Kyle Miller]

I wrote a very brief summary on the Proof Assistants stackexchange recently.

[Patrick Massot]

If you are at a stage where you don't understand what the intro tactic does (which is fine, everybody has to start at some point) then there is no hope at all that the reference documentation will help you. You would have a much better hope to learn something from a tutorial or introductory textbook. See https://leanprover-community.github.io/learn.html for pointers.

[Kyle Miller]

(Regarding why it's called intro, it's implementing the introduction rule for implication and universal quantifiers for the natural deduction, so the documentation isn't a tautology even though it appears to be one.)

[Patrick Massot]

Specifically about intro, there are two difficulties. First the word introduction is not used (in this sense) in regular math courses. This is really a technical word from logic. I don't know where you would meet this outside a logic course or a proof assistant context. The second difficulty is worse. In ordinary math we see two very different things: start the proof of a universally quantified statement by fixing an object, and start the proof of an implication by assuming the premise. It happens that the foundation of Lean make essentially no distinction between those two logical steps. So the same word is used for both. But this is is really an accident where foundational stuff that should be hidden to normal maths users leak through the proof assistant interface.