## Stream: general

### Topic: Proposal: fix x for assume x

#### Jasmin Blanchette (Apr 21 2020 at 06:14):

I would like to propose a small extension to Lean's structure language, namely fix as an alias for assume, intended to be used for data (as opposed to propositions).

Where mathematicians would write "Let $x$ be a real number. Assume $x > 0$. If $x > 3$, then $x^2 > 9$, in Lean we would write

assume x,
assume h : x > 0,
show x > 3 → x ^ 2 > 9, from ...


My proposal is to allow fix, so we could write

fix x,
assume h : x > 0,
show x > 3 → x ^ 2 > 9, from ...


"Fix x" is often used in mathematics as a synonym for "let x be a ...", especially in proofs and at the beginning of a section ("in this section, we fix ..."). It's short and works well when we don't write the type, like above. fix-assume-show is also the Isabelle/Isar idiom.

Of course, Lean has Curry-Howard, but in other places identical or nearly identical pairs of commands exist, e.g. constant vs. axiom, let vs. have, def vs. lemma. Why not fix vs. assume?

In The Hitchhiker's Guide to Logical Verification, which is used to teach interactive theorem proving, we introduced fix as an abbreviation for assume. It makes teaching easier, I find. See e.g. the schematic example on p. 35 (45 including the forematter).

What are your thoughts? @Mario Carneiro wouldn't it help you when golfing? @Anne Baanen, @Rob Lewis , @Sander Dahmen , and of course Buzzard et al. (@Kevin Buzzard , @Johan Commelin , @Patrick Massot ), wouldn't it help you write nicer looking math proofs?

#### Mario Carneiro (Apr 21 2020 at 06:15):

I think this actually used to exist

#### Mario Carneiro (Apr 21 2020 at 06:15):

I prefer \lam for golfing

#### Mario Carneiro (Apr 21 2020 at 06:16):

Personally, I just use \lam always and don't think about it. I don't like superfluous options. But fix for me has problematic connotations from its usage in Coq

#### Mario Carneiro (Apr 21 2020 at 06:22):

My recollection is that around lean 2 / early lean 3, there were a lot more synonymous keywords, like hypothesis, conjecture etc, including fix and assume as synonyms for \lam. This list was later cut down because too many options lead to analysis paralysis - people need to know all the synonyms, and know that they are synonyms. For me even assume is not good because of this.

#### Mario Carneiro (Apr 21 2020 at 06:23):

For example def and theorem are subtly different, but lemma is the same as theorem and definition is the same as def. Why?

#### Jasmin Blanchette (Apr 21 2020 at 06:23):

Yes, I understand that "analysis paralysis" can be a problem.

#### Mario Carneiro (Apr 21 2020 at 06:24):

Is it possible to declare fix as a notation for \lam? I think it can be

#### Jasmin Blanchette (Apr 21 2020 at 06:25):

I'm also not a fan of aliases in general. But I'm ready to make an exception for Curry-Howard. Concerning lemma (et al.) vs. def (et al.), I wish the small difference had been made on the universe (Type _ or Prop), so these could be considered "Curry-Howard aliases".

#### Jasmin Blanchette (Apr 21 2020 at 06:25):

Yes, it is possible, and that's what I do in the Hitchhiker's Guide. But we don't get syntax highlighting in VS Code.

#### Mario Carneiro (Apr 21 2020 at 06:26):

That actually doesn't depend on anything in lean

#### Mario Carneiro (Apr 21 2020 at 06:26):

you just need to update the extension for the new highlighting

#### Jasmin Blanchette (Apr 21 2020 at 06:26):

Well, @Gabriel Ebner won't treat fix as a keyword unless it's a keyword.

#### Jasmin Blanchette (Apr 21 2020 at 06:26):

And I won't fork his extension just for that.

#### Mario Carneiro (Apr 21 2020 at 06:27):

It would be nice if there were another way to set up highlighting per project so that we get things like #lint in color

#### Jasmin Blanchette (Apr 21 2020 at 06:27):

Regardless, I want to raise the matter with the whole community, in the hope that they say fix x is great, we want it, etc. If nobody cares, I'll just go away.

#### Mario Carneiro (Apr 21 2020 at 06:27):

I mean, lean knows about "user commands" and is configurable in this way, but the extension doesn't

#### Jasmin Blanchette (Apr 21 2020 at 06:28):

Again, I don't want a private extension. I'm making a proposal to change Lean for everybody.

#### Jasmin Blanchette (Apr 21 2020 at 06:28):

That "fix" isn't shown in blue, I can live with. The syntax highlighting has other, much worse oddities.

#### Mario Carneiro (Apr 21 2020 at 06:28):

What about functions called fix?

#### Mario Carneiro (Apr 21 2020 at 06:29):

I know that this has been used at least 2 or 3 times in mathlib

#### Jasmin Blanchette (Apr 21 2020 at 06:29):

I'm guessing they would behave like functions called assume.

#### Mario Carneiro (Apr 21 2020 at 06:29):

no, they almost always are being used to mean a fixpoint / recursive function of some kind

#### Jasmin Blanchette (Apr 21 2020 at 06:30):

Sure, but if there's a strong concensus, I'm sure it will be easy to rename them to have more specific names.

#### Mario Carneiro (Apr 21 2020 at 06:30):

for example well_founded.fix

#### Jasmin Blanchette (Apr 21 2020 at 06:30):

Anyway, I know you're not going to use fix, so that's 1:0 against. I'm curious to hear what the others will have to say.

#### Mario Carneiro (Apr 21 2020 at 06:31):

of course. I'm obviously not the target audience for this so I'm happy to hear other voices. I'm just curious what the rollout would look like here

#### Mario Carneiro (Apr 21 2020 at 06:32):

I don't think there are any functions called assume, but that's no surprise since declaring a function the same name as a keyword is a pain

#### Johan Commelin (Apr 21 2020 at 06:38):

I like the idea, because it lowers the barrier for newcomers (something that Lean is already pretty good at in general). The "analysis paralysis" is a bit of a problem, but I think we can overcome that. Especially if VScode tooltips explain the aliases / differences. (I don't think we currently have tooltips on keywords, do we?)

#### Mario Carneiro (Apr 21 2020 at 06:40):

Oh, my mistake, I checked the logs and the word for this in early lean 3 was take

#### Johan Commelin (Apr 21 2020 at 06:43):

I prefer fix, but I recognise the name clash with the fix from Coq.

#### Mario Carneiro (Apr 21 2020 at 06:44):

I think this is the issue that resulted in the removal of take as a keyword: https://github.com/leanprover/lean/pull/1706

#### Johan Commelin (Apr 21 2020 at 06:47):

From that issue.
@Sebastian Ullrich said:

I think I would be fine with just calling it list.take and making it protected. Using dot-notation for list functions is more ergonomic than opening the namespace anyway.

So all the fix functions can be made protected and continue their existence.

#### Mario Carneiro (Apr 21 2020 at 06:50):

Also interested to hear @Jeremy Avigad 's position since he uses this kind of style often

#### Jasmin Blanchette (Apr 21 2020 at 06:50):

I'm siding with Jeremy here: "take is nice for teaching students how to write proofs, and for that purpose, lambda, fun, and assume are not very natural as substitutes. So, I will be sorry to see it go. That said, I can live without it."

#### Mario Carneiro (Apr 21 2020 at 06:52):

Considering that lean's term mode was originally based pretty directly on Isar, I'm curious if I will find fix if I dig far enough into the past of lean 2, before I got involved

#### Anne Baanen (Apr 21 2020 at 07:41):

I will vote in favour of adding fix. The naming conflict doesn't seem a big deal (there are namespaces for this, after all), and choosing between fix and assume doesn't sound more difficult than choosing between def and lemma. (Could a linter see the difference between λ, assume, and fix?)

#### Kevin Buzzard (Apr 21 2020 at 08:06):

I never tell Xena people about this verbose term mode style and I personally find it hard to read the moment the number of goals starts to increase and one misplaced comma can throw things into chaos. Because I am always telling beginners to go straight into tactic mode and stay there, it's easy for us to get a fix, we could just add a tactic. Trying to make "verbose term mode" closer to English is an interesting question but it's not the mode for me personally. I am well aware that it can be popular amongst beginners with a CS background though

#### Johan Commelin (Apr 21 2020 at 08:08):

@Kevin Buzzard But do you also tell them to use tactic mode for definitions? Jasmin is talking about definitions here.

#### Kevin Buzzard (Apr 21 2020 at 08:15):

Oh I see. I tell them never to make definitions

#### Kevin Buzzard (Apr 21 2020 at 08:15):

And leave that to the experts

#### Jasmin Blanchette (Apr 21 2020 at 08:15):

Well I was thinking of structured proofs. Indeed, it doesn't concern Kevin.

#### Mario Carneiro (Apr 21 2020 at 08:15):

I think tactic mode is "structured proofs"

#### Mario Carneiro (Apr 21 2020 at 08:16):

I have a lot of trouble structuring term mode proofs well

#### Mario Carneiro (Apr 21 2020 at 08:16):

as in, every kind of indentation is terrible

#### Jasmin Blanchette (Apr 21 2020 at 08:16):

That's debatable, but if "structured proof" is controversial terminology, I mean "assume have show calc" proofs.

#### Jasmin Blanchette (Apr 21 2020 at 08:17):

I find calc hard to indent.

#### Mario Carneiro (Apr 21 2020 at 08:17):

I'm saying that for "assume have show calc" there are literally tactics called each of those

#### Mario Carneiro (Apr 21 2020 at 08:18):

(technically there is no calc tactic but calc as a tactic means exact calc)

#### Mario Carneiro (Apr 21 2020 at 08:20):

From what I've seen of isabelle, I think that Isar structured proofs look much more like tactic proofs than term mode, because of the neat indentation and block structure

#### Mario Carneiro (Apr 21 2020 at 08:21):

For example, how do you do a case split on an or hypothesis in isar? IIRC it looks basically like cases h, { subproof }, { subproof } with different keywords

#### Jasmin Blanchette (Apr 21 2020 at 08:32):

See p. 45, top-right example of https://isabelle.in.tum.de/website-Isabelle2014/dist/Isabelle2014/doc/prog-prove.pdf

#### Jasmin Blanchette (Apr 21 2020 at 08:34):

It's true that Isar feels in some sense more flexible than Lean term-based structured proofs. The grammar feels less constraining, more like tactics and less like writing a term.

#### Jasmin Blanchette (Apr 21 2020 at 08:34):

The error messages are also less wild. More like writing an imperative program and less like writing a Haskell program.

#### Jasmin Blanchette (Apr 21 2020 at 08:35):

Whereas Isabelle tactic mode is just horrible if you're used to Coq's or Lean's. No names for hypotheses? Come on.

#### Mario Carneiro (Apr 21 2020 at 08:36):

Proof commands perform transitions of Isar/VM machine configurations,which are block-structured, consisting of a stack of nodes with three main components: logical proof context, current facts, and open goals. (https://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf p.129)

This sounds an awful lot like a description of tactics a la lean

#### Jasmin Blanchette (Apr 21 2020 at 08:41):

Still, you can't invoke a tactic in the middle of an Isar proof to change the proof goal. You always need a fix, an assume, a have, a let, a define, or a show (I'm perhaps forgetting one or two, like guess).

#### Jasmin Blanchette (Apr 21 2020 at 08:43):

But the { } have a very special semantics. They look superficially like the parentheses surrounding proof subterms, but their main purpose is to delimit the scope of fixes and assumes. You can nest them arbitrarily.

#### Jasmin Blanchette (Apr 21 2020 at 08:43):

A bit like { } in C++ w.r.t. variable definitions, really.

#### Mario Carneiro (Apr 21 2020 at 08:44):

Yes, I think that isar top level commands map well to lean tactics, but not necessarily vice versa - lean tactics can do additional things that isabelle can't. So I think "structured proofs" in lean should be a specially curated subset of tactics with formatting conventions to make it more "structured"

#### Mario Carneiro (Apr 21 2020 at 08:46):

In principle we could even have a linter or something to enforce these guidelines so that you can have something with as much formal structure as isar

#### Jasmin Blanchette (Apr 21 2020 at 08:52):

The current situation is indeed quite messy, and when I teach I have to hide quite a bit of "junk" (e.g. the assume and calc tactics). Even then, it's still messy. Maybe getting rid of "structured proofs" and focusing on the other two, tactics and raw proof terms, is the way to go. Isn't that what Coq does anyway?

#### Sebastien Gouezel (Apr 21 2020 at 09:00):

Reading quickly, I have the impression you are using a correspondence between term mode and structured proofs, but I don't think this holds: you can perfectly make a structured proof in tactic mode also, using have, show, calc, obtain and so on. That's the mode I prefer, by the way: it keeps some readability, but you have a goal state and everything, so writing proofs is way easier than in term mode.

And I wouldn't mind having fix available there as a synonym for assume or intro.

#### Sebastian Ullrich (Apr 21 2020 at 09:04):

When I met Makarius in Bonn, he somehow was convinced that structured proofs would be removed from Lean 4. I don't know anything about that, and personally I wouldn't want them gone. Term mode is not flexible enough to simulate Isar-style proofs a la induction, case, have, have, show.

#### Mario Carneiro (Apr 21 2020 at 09:05):

Given the context of the discussion I'm not sure what sense of "structured proofs" you mean

#### Patrick Massot (Apr 21 2020 at 09:05):

structured proofs would be removed from Lean 4

Which meaning of structured proof is this using?

#### Patrick Massot (Apr 21 2020 at 09:07):

Jasmin, I'm a bit confused by your question because you initially asked for mathematicians opinion but, much later in the conversation, I suddenly realized this was all about crazy term mode proofs, so I don't see how this has anything to do with us.

#### Patrick Massot (Apr 21 2020 at 09:11):

My preferred way of juggling between tactics and terms is explained in https://leanprover-community.github.io/lean-web-editor/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover-community%2Ftutorials%2Fmaster%2Fsrc%2Ffirst_proofs.lean if you are patient enough to read. The default mode is tactic, but with a lot of small scale back and forth using relatively low complexity expressions and by.

#### Mario Carneiro (Apr 21 2020 at 09:11):

Sebastien Gouezel said:

And I wouldn't mind having fix available there as a synonym for assume or intro.

I agree here, as a tactic I think fix is unproblematic as a synonym for assume

#### Sebastian Ullrich (Apr 21 2020 at 09:11):

I assumed Jasmin meant "structured tactics" with that since he mentioned the assume tactic, which is my default meaning of the term as well. Basically, I'm agreeing with Mario:

I think "structured proofs" in lean should be a specially curated subset of tactics with formatting conventions to make it more "structured"

#### Patrick Massot (Apr 21 2020 at 09:13):

And, like Sébastien, I think that non-trivial proofs involving some mathematical idea should be done using structuring tactics, with occasional comments. See for instance https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lebesgue.20number.20lemma/near/194033514

#### Patrick Massot (Apr 21 2020 at 09:15):

About the broad idea of separating assumption introduction from data introduction, there is a difficulty with bounded quantifiers. In my course a lot of goals start with $\forall \varepsilon > 0$. There I really don't want to write fix epsilon, assume epsilon_pos. So the neutral intros epsilon epsilon_pos is convenient.

#### Mario Carneiro (Apr 21 2020 at 09:16):

I think the isar notion of "structured proofs" precludes a proof like this:

lemma inf_lt {A : set ℝ} {x : ℝ} (hx : x is_an_inf_of A) :
∀ y, x < y → ∃ a ∈ A, a < y :=
begin
-- Let y be any real number.
intro y,
-- Let's prove the contrapositive
contrapose,
-- The symbol ¬ means negation. Let's ask Lean to rewrite the goal without negation,
-- pushing negation through quantifiers and inequalities
push_neg,
-- Let's assume the premise, calling the assumption h
intro h,
-- h is exactly saying y is a lower bound of A so the second part of
-- the infimum assumption hx applied to y and h is exactly what we want.
exact hx.2 y h
end


because of the use of "non-approved" tactics like contrapose and push_neg being used for changing the goal statement

#### Patrick Massot (Apr 21 2020 at 09:16):

Also I don't care about the Coq meaning of fix, but we could use take instead. fix sounds more like cases on a existential assumption to me.

#### Mario Carneiro (Apr 21 2020 at 09:17):

much like our rule on "nonterminal simp", isar extends this to basically all tactics except for the small list Jasmin gave above

#### Mario Carneiro (Apr 21 2020 at 09:18):

If you violate this rule too much, your tactic script ends up more like a coq style imperative proof

#### Mario Carneiro (Apr 21 2020 at 09:19):

(I'm not making a value judgment here, but I think this is the line that "structured proofs" is trying to draw)

#### Sebastien Gouezel (Apr 21 2020 at 09:20):

So instead of contrapose, push_neg, you would say : suffices H : ..., by { contrapose, push_neg, exact H}.

#### Patrick Massot (Apr 21 2020 at 09:20):

This was not the example of structured proof, the Lebesgue number lemma was

Yes, sure.

#### Jasmin Blanchette (Apr 21 2020 at 09:30):

Sorry, I see that terminology is confusing. When I teach Lean, I tell my students that there are tactical proofs, structured proofs, and raw proof terms. In tactical, I use intro. In "structures proofs", I use assume (and fix). In raw proof terms, I use $\lambda$. If anybody has a better name for structured proofs a.k.a. syntactically sugared proof terms, I'm a taker.

As for @Patrick Massot : True, I forgot for a moment that many of you guys wouldn't care because you use tactics for nearly everything.

#### Mario Carneiro (Apr 21 2020 at 09:32):

I would say that lean has two modes, term mode and tactic mode. Both modes have idioms that can be used to make the proof more structured for presentation purposes

#### Johan Commelin (Apr 21 2020 at 09:32):

But not for definitions, and I think you were talking about definitions as well, right?

#### Mario Carneiro (Apr 21 2020 at 09:33):

although because term mode is an expression grammar the options for out of band annotations are more limited

#### Jasmin Blanchette (Apr 21 2020 at 09:39):

Johan, I wasn't thinking about definitions. And indeed, Mario, I agree that "structured proofs" are just a subtype, but for teaching it's convenient to have a different name.

#### Mario Carneiro (Apr 21 2020 at 09:41):

sure, but if you include structured proofs that makes 4 modes total, not 3, that's my point

#### Mario Carneiro (Apr 21 2020 at 09:42):

and the mathematicians on the chat seem to prefer the mode that you haven't enumerated

#### Mario Carneiro (Apr 21 2020 at 09:43):

because there is definitely also such a thing as "unstructured tactic proofs", such as those that you get from people learning to write tactics from NNG

#### Jasmin Blanchette (Apr 21 2020 at 09:47):

Well I'm only teaching three modes.

#### Jasmin Blanchette (Apr 21 2020 at 09:47):

But you're right. I teach very briefly the have and let tactics -- I guess that's the fourth mode.

#### Jasmin Blanchette (Apr 21 2020 at 09:49):

Maybe I should just give up on that assume show stuff and use $\lambda$. But Rob teaches the previous course with that (and raw proof terms)...

#### Sebastien Gouezel (Apr 21 2020 at 09:49):

Jasmin, what do you think of the proof given by Patrick at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lebesgue.20number.20lemma/near/194033514? For me, that's the most readable we can achieve with Lean today.

#### Jasmin Blanchette (Apr 21 2020 at 09:54):

I like it. It's basically Isar. And it shows that one doesn't need proof terms to write structured proofs.

#### Kevin Buzzard (Apr 21 2020 at 09:58):

I have been pointing students towards this "obtain" style since I saw it. But for me, the most readable style is the one that Mario posted above, where you just write any old proof but put comments everywhere :-)

#### Kevin Buzzard (Apr 21 2020 at 09:59):

Someone at Bonn really wanted to grill me about the difference between forward proofs and backward proofs, but I often feel I have nothing to say here. For some reason I don't think I understand the question properly.

#### Jasmin Blanchette (Apr 21 2020 at 10:02):

It starts already with the huge fractions that computer scientists use with T's on their side. We call stacks of them "trees", and when we "climb" the "tree" from the "root", you'd think we're going upwards but actually we say "backwards". Very easy, you see. But if you descend the "tree" from the "leaves", then you proceed "forwards", not downwards. Proof terms are also bidirectional (inside out or outside in).

#### Patrick Massot (Apr 21 2020 at 10:08):

Hey Kevin, do you know Rob recorded a video to explain to us one flavor of the big fraction thing?

#### Patrick Massot (Apr 21 2020 at 10:09):

The flavor which is about finding the most complicated way to explain a trivial proof. Unfortunately it's not the one we'd need to understand Mario's thesis. For that we need the typing rules big fractions, but it's related I think.

#### Patrick Massot (Apr 21 2020 at 10:13):

Videos 5 and 7 at http://robertylewis.com/logic_and_modeling/lecture_1. You need to click your way until it shows the slides properly. Unfortunately I haven't found the playback speed option so it's pretty painful to watch. Take this as a patience exercise.

#### Sebastian Ullrich (Apr 21 2020 at 10:16):

Perhaps it would be better to talk not about "structured proofs" like a different category, but "proof structuring" as an (incremental) method of organizing tactic proofs using specific structuring tactics.

#### Jasmin Blanchette (Apr 21 2020 at 10:17):

This doesn't help me. I need a name for assume have show-style proofs, so I can tell my students, "Write a foo-bar proof" and they'll know what I mean. Any ideas anybody?

#### Jasmin Blanchette (Apr 21 2020 at 10:18):

(fix) assume have show is too much of a mouthful.

#### Sebastien Gouezel (Apr 21 2020 at 10:34):

raw term proof/structured term proof/raw tactic proof/structured tactic proof

#### Jasmin Blanchette (Apr 21 2020 at 10:56):

I could live with "structured proof term" (with proof before term). For tactics, I guess "structured" arises once you start using "have", more or less?

#### Patrick Massot (Apr 21 2020 at 11:33):

"have" or "suffices" or "obtain"

#### Patrick Massot (Apr 21 2020 at 11:33):

and sometimes "change" or "show"

#### Mario Carneiro (Apr 21 2020 at 11:54):

and especially { }

#### Jeremy Avigad (Apr 21 2020 at 14:18):

I don't have a strong opinion here. In the early days of Lean, we had lots of aliases. The words structure and record were interchangeable, and we had take and assume. All of these were the same: theorem lemma proposition corollary and probably more. Instead of variable you could write premise, and instead of parameter you could write hypothesis. I think conjecture was allowed for something as well.

At one point early in the Lean 3 years, Leo decided to clean up and simplify syntax. The only synonyms he kept were axiom / constant and theorem / lemma.

Ultimately, I think he was right. The proliferation of keywords made the system feel messy and chaotic. It is easy to explain and get used to assume; I have had no trouble explaining the double use to students. One of the attractive things about Lean is that the syntax is so clean.

@Sebastian Ullrich will also remember the endless discussion over the use of . for projection notation, as inl.cons. IIRC, before that we used l.>cons, and there was a lot of worry that if we used a period the ambiguity with namespaces would confuse people and cause problems. But eventually Leo made a decision, and in hindsight, it was the right one.

Leo has a really good sense for these things. He is almost always right. I suspect that once we start using Lean 4, we will cringe when we look back on all the underscores. (Incidentally, in the early days of Lean, we also debated underscores vs. hyphens, which Agda uses, as in my-long-theorem-name. Leo rejected that, because it would mean requiring spaces around a minus sign, so we could not write x-y.)

#### Jeremy Avigad (Apr 21 2020 at 14:22):

Oh, another Leo innovation: we used to write definition before he shortened it to def. I think that is why def isn't syntax highlighted in the Zulip code blocks.

#### Sebastian Ullrich (Apr 21 2020 at 14:27):

Originally it was l^.cons I think. But yes, that was a fun change. At first we were cautious about ^. itself being too crazy to keep, but soon we started using it so much that not only couldn't we live without it, we even started thinking about making its syntax almost invisible. It simply was that good.

#### Mario Carneiro (Apr 21 2020 at 14:29):

It actually still works:

#check []^.length


#### Mario Carneiro (Apr 21 2020 at 14:32):

Are there any ambiguities in x.foo that are not fixed by x .foo? If so we can probably remove ^.

#### Mario Carneiro (Apr 21 2020 at 14:33):

there are precisely 0 uses of ^. in mathlib

#### Sebastian Ullrich (Apr 21 2020 at 14:34):

Yes, it's already been removed in Lean 4

#### Jasmin Blanchette (Apr 21 2020 at 15:25):

@Jeremy Avigad Thanks for the historical perspective. It explains why Lean is half against aliases and half in favor -- a slightly messy state. I surely never mention definition to my students, nor fun for $\lambda$ etc. Given that the axiom of choice is specified with axiom even though the result type is $\alpha$, I'm guessing there's more dead wood there.

#### Sebastian Ullrich (Apr 21 2020 at 15:36):

Note that axiom/constant will actually be a meaningful choice in Lean 4: constants have to be inhabited. I actually can't think of any synonyms still left apart from ASCII syntax.

#### Jasmin Blanchette (Apr 21 2020 at 15:45):

rw vs. rewrite?

#### Mario Carneiro (Apr 21 2020 at 15:55):

axiom and constant are actually distinct all through the lean process, but I've never been able to figure out what the difference is

#### Mario Carneiro (Apr 21 2020 at 16:00):

The fact that choice has type alpha isn't actually that relevant - while it is easy to explain the difference between def and theorem via the curry howard Prop/Type distinction, in lean the difference is in other things: defs are elaborated synchronously, and they have code generated, while theorems do not. It makes sense then that choice should be an axiom since it has no code, by comparison to a meta constant which has no lean definition but nevertheless has code. constant is used nowhere in lean core so I don't know exactly what its purpose is

#### Sebastian Ullrich (Apr 21 2020 at 16:18):

Jasmin Blanchette said:

rw vs. rewrite?

Ah, that does look redundant. I assume no-one is actually using rewrite, just like with definition.

#### Sebastian Ullrich (Apr 21 2020 at 16:20):

Not that either of them is in Lean 4 right now. We did kill return in favor of pure!

#### Jeremy Avigad (Apr 26 2020 at 17:20):

This thread involved some historical storytelling, and I belatedly realized that I should have given @Sebastian Ullrich credit for the current form of anonymous projections. It was Leo's idea to use them for projections of a structure so that for example we could write p.fst and Lean would infer from the type of p that this means prod.fst p. But Sebastian quickly pointed out that the same trick would work for any theorem or definition in a namespace with the same name as the type, allowing us to write l.length first list.length l. What a stroke of genius! It's a good thing he is so involved in the syntax of Lean 4.

#### Sebastian Ullrich (Apr 26 2020 at 17:34):

Oh, I didn't even remember that change, only the syntactic one... it's interesting that there hasn't been much discussion so far about generalizing the notation even further, e.g. over super structures (seems relatively straightforward) or typeclasses (less clear). No changes there in Lean 4, yet.

#### Patrick Massot (Apr 26 2020 at 17:38):

This is indeed very convenient.

#### Patrick Massot (Apr 26 2020 at 17:39):

Hey, we did ask very loudly for a more powerful dot notation for super structures in Lean 4.

#### Patrick Massot (Apr 26 2020 at 17:41):

Last updated: Dec 20 2023 at 11:08 UTC