Proposal: `fix x` for `assume x`

Stream: general

[Jasmin Blanchette]

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]

I think this actually used to exist

[Mario Carneiro]

I prefer \lam for golfing

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Jasmin Blanchette]

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]

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]

That actually doesn't depend on anything in lean

[Mario Carneiro]

you just need to update the extension for the new highlighting

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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

[Mario Carneiro]

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]

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]

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

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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

[Mario Carneiro]

What about functions called fix?

[Mario Carneiro]

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

[Jasmin Blanchette]

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

[Mario Carneiro]

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

[Jasmin Blanchette]

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]

for example well_founded.fix

[Jasmin Blanchette]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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]

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

[Jasmin Blanchette]

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]

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]

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]

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]

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

[Kevin Buzzard]

Oh I see. I tell them never to make definitions

[Kevin Buzzard]

And leave that to the experts

[Jasmin Blanchette]

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

[Mario Carneiro]

I think tactic mode is "structured proofs"

[Mario Carneiro]

I have a lot of trouble structuring term mode proofs well

[Mario Carneiro]

as in, every kind of indentation is terrible

[Jasmin Blanchette]

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

[Jasmin Blanchette]

I find calc hard to indent.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Jasmin Blanchette]

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]

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

[Jasmin Blanchette]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Patrick Massot]

structured proofs would be removed from Lean 4

Which meaning of structured proof is this using?

[Patrick Massot]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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

[Patrick Massot]

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

[Patrick Massot]

Yes, sure.

[Jasmin Blanchette]

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]

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]

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

[Mario Carneiro]

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

[Jasmin Blanchette]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

Well I'm only teaching three modes.

[Jasmin Blanchette]

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

[Jasmin Blanchette]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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]

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]

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

[Sebastien Gouezel]

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

[Jasmin Blanchette]

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]

"have" or "suffices" or "obtain"

[Patrick Massot]

and sometimes "change" or "show"

[Mario Carneiro]

and especially { }

[Jeremy Avigad]

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]

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]

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]

It actually still works:

#check []^.length

[Mario Carneiro]

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

[Mario Carneiro]

there are precisely 0 uses of ^. in mathlib

[Sebastian Ullrich]

Yes, it's already been removed in Lean 4

[Jasmin Blanchette]

@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]

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]

rw vs. rewrite?

[Mario Carneiro]

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]

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]

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]

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

[Jeremy Avigad]

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]

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]

This is indeed very convenient.

[Patrick Massot]

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

[Patrick Massot]

Sebastian, see also https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/to_extending