terminology question `have`

Stream: new members

[rzeta0]

What is the correct terminology for what have is?

It is an instruction? Is it a command? Is it a statement?

I ask about have specifically because it causes an important side-effect, it registers a new hypothesis.

(I'm developing beginner-friendly tutorials for people like me, also a beginner, and I'd like to know what have is).

[Ruben Van de Velde]

In tactic mode (i.e. after by), it's a tactic

[rzeta0]

I still don't know what tactic or other mode is.

Here is my example below, there is no by before have so I assume this is not tactic mode.

example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 :=
  have h3: b = 1 := by linarith [h2]
  calc
    a = b + 1 := by rw [h1]
    _ = 1 + 1 := by rw [h3]
    _ = 2 := by norm_num

[Kyle Miller]

If have is inside the by syntax, it's a tactic. If have is outside the by syntax, it's a term.

Hint: if you right click on syntax and select "go to declaration", it brings you to the syntax definition. If you see something like @[builtin_term_parser] or syntax ... : term or macro ... : term or elab ... : term, it's a term. If you see something like @[builtin_tactic_parser] or syntax ... : tactic or macro ... : tactic or elab ... : tactic, it's a tactic.

[Kyle Miller]

Note that the have tactic is implemented using the have term.

The rule is pretty much that by have x := v; rest_of_tactics is have x := v; by rest_of_tactics

[rzeta0]

I don't know what term or tactic mode is so I will return to this question later when I have learned what those are.

[Kyle Miller]

It seems like you might have a belief that somehow these are really deep things, but there's very little to it. What I mean is that a "term" vs "tactic" is two classes of syntax, and in different contexts you can use a term or a tactic. That's pretty much it.

A term is anything that can go immediately after the :=, i.e., some syntax that represents a value. Like 1 + 1, b - 1 = 0, ∀ x, P x. There are many other places terms can appear, like after the colon in binders.

A tactic is what appears in by syntax. The syntax for by is by TACTIC+, where + means one or more times. (Slight correction: if the tactics appear in one line, they have to be semicolon-separated.)

[Kyle Miller]

People talk about "modes" colloquially. You can't put a term right after by because the parser expects a tactic there. You can't put a tactic right after := because the parser expects a term there. It's sort of modal in that way.

[Kyle Miller]

The main syntax categories are

• terms
• universe levels
• tactics
• commands
• attributes

[Kyle Miller]

There are also syntax categories like do elements (for do notation) and priorities (for instances, simp lemmas, parsers, etc.)

[rzeta0]

Thanks, that is the clearest explanation of tactic vs term mode I've seen in months of learning!

As an outsider, it is clear the tutorials are not yet beginner friendly, and much of the discussion happens between people who are all at a high level of expertise - this makes the entry barriers quite high.

Still, I will persist in trying to learn more lean4 for the purposes of writing simple proofs.

[Julian Berman]

@rzeta0 I suspect you may not have known to look for them on this page, but do you find https://leanprover-community.github.io/glossary#mode https://leanprover-community.github.io/glossary#term-mode and https://leanprover-community.github.io/glossary#tactic-mode helpful at all? (If not, please feel free to suggest improvements, as the hope was that these would be quite accessible)

[rzeta0]

Hi Julian - since you asked my opinion, here it is:

• the glossary is certainly useful, better to have it than not
• but for beginners, that glossary defines those words in terms which assume a moderate level of knowledge already, but i'm not expert enough to offer alternatives (the docs do this too*)
• at this stage in my learning, i just don't understand why people even mention "modes", it has very little to do with the concepts required for simple proofs from a mathematical perspective imho, and I suspect it is because some/many of the lean community are language developers/enthusiasts

Take my option with a pinch of salt, I am no expert.

(*) and an internet search keeps taking me to "mathlib3" docs, not 4?

[Julian Berman]

(It's a valuable opinion I think! Just trying to understand it!). I think you're probably right that as a beginner it would be easiest not to at all think about modes -- I think if I recall correctly a bunch of teachers in the community agree with you even, and in their courses they only teach what is called tactic mode, but effectively that's the only thing that exists to their students -- the complication is simply if someone mentions some other one to answer a question -- but yeah you can simply start all your proofs with by and then not learn anything about modes and get quite far.

[Florent Schaffhauser]

rzeta0 said:

What is the correct terminology for what have is?

It is an instruction? Is it a command? Is it a statement?

I ask about have specifically because it causes an important side-effect, it registers a new hypothesis.

(I'm developing beginner-friendly tutorials for people like me, also a beginner, and I'd like to know what have is).

TLDR: have is a command, similar to theorem, but used for local declarations (i.e. a declaration that appears within another proof/program).

More specifically have is the command used for a local declaration of the form have p : P where P : Prop, which is the Prop analogue of the local declaration let t : T where T : Type.

In principle, you should be able to take your have command out of your main declaration, put it above the latter, replace the have command by a theorem command, and your main declaration should still typecheck.

import Mathlib.Tactic.Linarith

theorem h3 {b : ℤ} (h2: b - 1 = 0) : b = 1 := by linarith [h2]

example {a b : ℤ} (h1 : a = b + 1) (h2: b - 1 = 0) : a = 2 :=
  calc
    a = b + 1 := by rw [h1]
    _ = 1 + 1 := by rw [h3 h2]
    _ = 2 := by norm_num

Hope it helps a little!

[rzeta0]

thank Flo - are you using "command" generically or is it a specific category of syntax in Lean4?

I'm happy with the word "command" or "instruction" generically to describe theorem have and example if you think that is correct.

[Florent Schaffhauser]

I am using it a bit generically, indeed. Maybe 'keyword' is a more correct term than 'command' in the present context? But the point is that the same terminology should be applied to have/let as to theorem/def :blush:

[Kyle Miller]

I would avoid calling have a command, since the word command already refers to things like the theorem command, the variable command, the inductive command, etc.

Certainly the the word have itself is a keyword that is part of the have syntax.

[Florent Schaffhauser]

Hi Kyle Miller :wave: So you would recommend saying the theorem command and the have keyword? Not what I expected, but I am fine with it :blush:

[Kyle Miller]

Both theorem and have are keywords to be clear (they're text that the parser sees as being keywords), but theorem is part of the theorem command, and have is part of both the have tactic and the have term. For units-of-Lean, I'd stick with command/term/tactic/etc.

[Kyle Miller]

It's a little bit of synecdoche to say "the theorem command", "the have tactic", and "the have term", which is perfectly fine. (There's a lot more to theorem syntax that just the theorem keyword, but there's only one command with theorem as part of its syntax.)

[Kyle Miller]

(I personally use "expression" and "term" interchangeably. This probably isn't correct in theoretical contexts, but as a working Lean user it seems fine.)

[rzeta0]

... as I was saying, not at all beginner friendly ;-)

trying saying "theorem is part of the theorem command" to a beginner and watch as our minds melt.

[Kyle Miller]

I wouldn't phrase it like that, but what's the issue? The command to introduce a theorem begins with the theorem keyword. That's a basic fact.

[Florent Schaffhauser]

Kyle Miller said:

Both theorem and have are keywords to be clear (they're text that the parser sees as being keywords)

Yes, indeed, so keyword seems to be the proper terminology in the context of rzeta0 's initial question, which was about how to refer to words such as have or theorem in an expository text about how to write basic Lean programs :blush:

[Kyle Miller]

However, rzeta0 talks about have introducing new hypotheses — the keyword itself doesn't introduce new hypotheses.

[Kyle Miller]

If we say "the have tactic" that doesn't mean that the have keyword is a tactic. We're referring to a particular tactic whose syntax contains the have keyword via a figure of speech.

[Florent Schaffhauser]

Thanks, I believe it helps to say this explicitly!

[Kyle Miller]

(There's nothing inherently wrong with thinking of tactics as being commands, but there's just the issue that the word "command" already refers to another concept in Lean 4. They are commands in the looser sense of actions that are performed one at a time.)

[Julian Berman]

rzeta0 said:

... as I was saying, not at all beginner friendly ;-)

trying saying "theorem is part of the theorem command" to a beginner and watch as our minds melt.

Not to get too far into meta-land -- as I say I think I generally agree with your perspective on how to think about this at the beginner level -- but at some point I think you should also recognize you're asking in a thread titled "terminology question", so at some point you have to expect that some level of precision will be involved in answering some questions, because otherwise, if there was no precision needed, there'd be no need for the separate concepts to exist.

Specifically I think a beginner saying "I know how to write a theorem in Lean" and then asking "how would you call the word theorem in the thing I use to write one of those" now likely does deserve a more precise answer to that, a term which really accurately describes what that thing is.

[Kyle Miller]

And to add to that, I personally think it's not pedagogically useful to know the exact parts of speech of everything in Lean. Knowing that "theorem" is a keyword might only become useful once you're writing syntax extensions yourself!

[Kyle Miller]

I notice that @rzeta0's learning style is to know exactly what everything is, but a lot of mathematical users treat it more like a something to get the gist of and get to work. They ask questions about technical details when they get in the way of doing something.

[Florent Schaffhauser]

Kyle Miller said:

And to add to that, I personally think it's not pedagogically useful to know the exact parts of speech of everything in Lean. Knowing that "theorem" is a keyword might only become useful once you're writing syntax extensions yourself!

Well, it's also useful when you want to say things like "in order to declare a theorem, use the keyword theorem".

[Kyle Miller]

With that @Flo (Florent Schaffhauser), I think most people see theorems and then copy the syntax, without needing to know what "theorem" is called.

[rzeta0]

Just to respond to Julian - precision does not necessarily imply difficulty / confusion.

Let's compare to Prolog, a language similarly rooted in logic and proofs. The language itself does indeed have syntax and there is a precise way to refer to the things you see in Prolog code.

However, none of that seems to generate confusion or the same level of difficulty in explaining them as Lean seems to - for those that do indeed ask about "terminology".

This is not to be taken as a criticism. It is an observation from someone who is a beginner, but has been learning languages since 1988 - and has seen both good and bad - and merely wishes that such an amazing thing as a maths theorem proof assistant could be made more accessible to many more people.

I do want to say thank you to everyone who has contributed.

[rzeta0]

Kyle - you're right, I am against the school of learning which is "copy and paste from stackexchenge or chatGPT".

I'm not a fetishiser of syntax - which is why I vastly prefer small, consistent, low-surprise languages.

But I find i have to ask sometimes technical questions because none of the tutorials has actually explained what is happening - and I can't teach a topic if I don't know myself!

[Kyle Miller]

Regarding "tactic mode", believe it or not this terminology is helpful for many learners. I personally never got the point of it (but I come from a compilers background, so to me I just see that a grammar limits what you can write in different contexts), but to these learners, "tactic mode" is a good enough answer for why tactics can only appear inside of "tactic mode".

[Julian Berman]

rzeta0 said:

Kyle - you're right, I am against the school of learning which is "copy and paste from stackexchenge or chatGPT".

I'm not a fetishiser of syntax - which is why I vastly prefer small, consistent, low-surprise languages.

But I find i have to ask sometimes technical questions because none of the tutorials has actually explained what is happening - and I can't teach a topic if I don't know myself!

I find this to be a false dichotomy a bit personally -- I have written fewer than ~1000 lines of Prolog and 0 in the last 10 years, so I can't compare -- but of the languages I do know, Lean is certainly the most syntactically flexible. And so even though I agree with you 100% that I wish Lean was less flexible and therefore had fewer syntactic concepts, I see others find it very useful, and to me it seems simply to be a stylistic choice in language design. But I don't really see it as being very related to the topic here about how to explain what's happening -- meaning once a language does function that way, now you need to describe it, so if you dislike something, it's the functionality you dislike :) the fact that terminology gets more complex is just a byproduct. (I guess I said not to get too deep into meta-land, so probably I should stop doing it, which I'll try to do after this message :D)