Documenting lean pitfalls: feedback requested

Stream: general

[Niels Voss]

Over this past week, I've been working on and off on a document that describes common pitfalls and footguns I've seen on this Zulip as well as things I personally struggled with when learning Lean. Topics covered include autoImplicit, integer division, distance in Fin n → ℝ, etc. The document is available here (although I would be willing to move it anywhere else or merge it into any other documentation if it makes sense to do so):
https://github.com/nielsvoss/lean-pitfalls

I am interested in hearing about whether or not this document is useful to you, as well as any mistakes I've made, writing that I should clean up, things I should add, and whether this is similar to something someone else has already made.

This document was partially inspired by this message:
Jason Rute said:

Someone needs to write a document for AI researchers telling them about common pitfalls, axioms, checking proofs, errors in benchmarks, and other things which would embarrass them if they don't handle correctly.

although it is designed to be of interest to all Lean users, and not just AI researchers. Also, I didn't add anything about the correct way to check lean proofs, because I don't think I understand the situation well enough to write about that (although I can add it in the future).

[Julian Berman]

Nice! Certainly seems like a.. virtuous thing to have.

Notes from a scan through:

• I think the inlay hint functionality bears mentioning in the autoimplicit section as it makes them a lot less error prone (or at least a lot less invisibly poisonous, as long as someone knows to look for them)
• Possibly instead of executing lake exe cache get the "recommended" way to perform that these days is to invoke the action inside VSCode? I.e. here
• Maybe it's worth dividing the content into "Lean language gotchas", "Math in Lean gotchas" and "Lean tooling/ecosystem gotchas" (the above are the latter, but then you start with a few of the former two)
• It'd probably be nice to interlink mentions of tactics to the docs
• In Lean, < and ≤ are preferred to > and ≥ -- is this Lean, or Mathlib?
• "Subtraction of natural numbers truncates at 0" -- maybe a few more words just saying this is because its return type has to be Nat?
• The "Other partial functions" section is so nice maybe it could be a table (of partial function, description, and what you add if you want to say your input is sane, if such a declaration exists?) Also maybe it's worth not mentioning the specific junk values or at least saying they're not meant to be relied on?

[Niels Voss]

Julian Berman said:

• I think the inlay hint functionality bears mentioning in the autoimplicit section as it makes them a lot less error prone (or at least a lot less invisibly poisonous, as long as someone knows to look for them)

Done.

• Possibly instead of executing lake exe cache get the "recommended" way to perform that these days is to invoke the action inside VSCode? I.e. here

I edited the cache section to be less terminal-centric, and mentioned this.

• Maybe it's worth dividing the content into "Lean language gotchas", "Math in Lean gotchas" and "Lean tooling/ecosystem gotchas" (the above are the latter, but then you start with a few of the former two)

To be honest I don't really know how to organize this. I originally tried to place the most common errors closest to the top (autoImplicit comes up more often than native_decide, for often) but then I tried to group the library gotchas together, and now it's fairly disorganized. I'll have to think about how best to do this.

In any case, I don't know if they divide that easily into groups. Integer division could be considered a "Math in Lean gotcha" but the way in which type inference relates to integer division could be considered a "Lean language gotcha".

• It'd probably be nice to interlink mentions of tactics to the docs

Some tactics are documented in the reference manual, but some are mathlib specific. Is there a centralized documentation location for tactics?

In the future this document might be verso-ified if it makes sense which will remove the need to manually link tactics but this makes sense for the meantime once I get around to it.

• In Lean, < and ≤ are preferred to > and ≥ -- is this Lean, or Mathlib?

I don't know. I think I'll wait for further community input.

• "Subtraction of natural numbers truncates at 0" -- maybe a few more words just saying this is because its return type has to be Nat?

Done.

• The "Other partial functions" section is so nice maybe it could be a table (of partial function, description, and what you add if you want to say your input is sane, if such a declaration exists?) Also maybe it's worth not mentioning the specific junk values or at least saying they're not meant to be relied on?

I can consider this, but the point of listing these functions is just to make the point that a lot of unrelated functions in Mathlib behave this way and this is generally something to watch out for. The list is not anywhere close to comprehensive.

Is there consensus on whether or not junk values should be considered implementation details? I know there were some comments about how 0 / 0 could return 37 and no one would be bothered but that isn't at all what I've seen in Mathlib; lemmas in Mathlib seem quite happy to rely on the specific junk values.

[Kevin Buzzard]

I definitely made that comment in my "why is 1/0=0" blog post but I was well aware at the time that it was not 100% accurate; some junk values are better than others. I decided to leave it there to stress the point that it was not the actual value that mattered, just that there had to be a value.

[Alex Meiburg]

An "index of junk values" would be good to maintain more broadly, I think.

Division by zero, subtracting Nats, sure. But also things like: Real.sqrt on negatives, Real.log 0, subtracting NNReal or ENNReal, basically any arithmetic with EReal or ENNReal that would conventionally be a NaN (quick: what is top - bottom? Bottom * 0?), division of Nat rounds down... Division of PNat rounds down like Nat except that 1/5=1... etc etc

[Aaron Liu]

Alex Meiburg said:

(quick: what is top - bottom? Bottom * 0?)

Well clearly ⊤ - ⊥ = ⊤, and I also know that ⊥ * 0 = 0

[Edward van de Meent]

Maybe Mathlib should keep test files for these junk values, as a place to document choices made + motivation

[Alex Meiburg]

Aaron Liu said:

Alex Meiburg said:

(quick: what is top - bottom? Bottom * 0?)

Well clearly ⊤ - ⊥ = ⊤, and I also know that ⊥ * 0 = 0

Sure yes, I meant to say top + bottom or top - top. (Which is much less intuitive to me.) I accidentally did "both" when I wrote the message :)

[GasStationManager]

Nice work! I remember being surprised by the division by zero (I was working with Rat).

As for something to add: this may be a hot take, but array indexing by Fins. Basically ask them to read this. I'm not sure if anything has changed since then; Functional Programming in Lean still recommends using Fins for indexing. To rank the various indexing options from most safe to least:

• a[i]'bounds_proof. Safe but tedious. Perhaps package the index value i and the bounds_proof together into a Subtype to pass around.
• a[i]? I truly am not sure whether i is in bounds or not
• a[i]! I am a Java/Python programmer; I sometimes venture into C++ but use .at() instead of []. If I make a mistake, my program will at least give a runtime error.
• a[i] with Fin type index. I write C/C++ and live on the edge. I just want to turn off bounds checking. If I make a mistake, which I won't.... valgrind will catch it, right?...

The last option is so convenient, I sometimes use it because I was too lazy to do the safer way. I'm a C++ programmer, what can say...

[Niels Voss]

How is using Fin for indexing dangerous?

Edit: I see, it's not that it causes undefined behavior, it's that it causes confusing total code

[Mario Carneiro]

I think the current way indexing is designed makes it unfortunate when you have a Fin n and want to pass it to a Fin n -> A packed as a vector or the like

[Mario Carneiro]

like that shouldn't be hard but the typeclasses put so much junk in the term

[Aaron Liu]

Mario Carneiro said:

like that shouldn't be hard but the typeclasses put so much junk in the term

What kind of junk?

[Alex Meiburg]

opened #25173 as an attempt at this, making a MathlibTest file documenting lots of junk values. I'm sure there are many more to add.

[Joseph Myers]

Another pitfall with default/junk values arises with indexed inf / sup: ⨅ i ∈ s, f i is the infimum over all i in the relevant type of the infimum over all proofs of i ∈ s of f i, and that infimum over proofs can be a default value for i not in s, resulting in the outer inf not giving the desired result.

[Niels Voss]

I'm not sure I understand. Can you provide a #mwe or link to a zulip thread that discusses this issue?

[Terence Tao]

Regarding "Parameters for instances that already exist": one sign that this sort of "instance diamond" behavior is occuring is if two quantities that look identical in the infoview, are not being treated as equal by Lean (e.g., they are not being cancelled in the expected fashion by tactics such as rfl, congr, convert, etc.). Often one has to hover over the various terms in the infoview to look at various implicit instances that are used; sometimes one has to go two or three levels deep into a type before one sees the discrepancy.

[Niels Voss]

That's a good point. I've encountered this exact problem with the infoview a lot in the past. It seems to be more common for function calls than notation, because if there was an extra One Nat instance for example, the bad 1 value seems to display as One.one which is at least a clue that something is going on.

A somewhat artificial MWE is

import Mathlib.Topology.MetricSpace.Basic

example [inst : MetricSpace ℝ] : dist (0 : ℝ) 1 = inst.dist (0 : ℝ) 1 := by
  /-
  Tactic state:
  1 goal
  inst : MetricSpace ℝ
  ⊢ dist 0 1 = dist 0 1
  -/
  sorry

where you can no longer tell in the infoview that the two distance functions are the same.

[Niels Voss]

I will add a note about this in the document but I'm hoping that in the future this can be fixed at the level of the delaborator. Perhaps the delaborator could keep track of which instances have been inferred for a given typeclass and if they aren't all definitionally equal, it could print them all explicitly.

[Julian Berman]

I could be misremembering but I think @Kyle Miller did some related work on this sort of thing. Maybe just relating to error messages and not showing ones that say "foo expected got foo"

[Kyle Miller]

Yeah, it shows the difference between both dists when you try using rfl:

example [inst : MetricSpace ℝ] : dist (0 : ℝ) 1 = inst.dist (0 : ℝ) 1 := by
  rfl
  /-
  tactic 'rfl' failed, the left-hand side
    @dist ℝ (@PseudoMetricSpace.toDist ℝ Real.pseudoMetricSpace) 0 1
  is not definitionally equal to the right-hand side
    @dist ℝ (@PseudoMetricSpace.toDist ℝ MetricSpace.toPseudoMetricSpace) 0 1
  inst : MetricSpace ℝ
  ⊢ dist 0 1 = dist 0 1
  -/

[Kyle Miller]

@Terence Tao When congr/convert creates side goals, do you ever try using rfl on them to help play the spot-the-difference puzzle? (This UI could be improved, but that's the one trick I know might help.)

I wonder if Eq in general should pretty print with differences made explicit.

[Terence Tao]

No, but thanks for the tip.

[Kevin Buzzard]

Niels Voss said:

I'm not sure I understand. Can you provide a #mwe or link to a zulip thread that discusses this issue?

I think David Loeffler's example here #mathlib4 > sup and inf over sets @ 💬 explains the (terrifying!) issue very clearly :-)

[Terence Tao]

Another general pitfall is when manipulating elements x of a set S: Set X via the subtype (x:S) rather than (x:X) (hx: x ∈ S). The two are of course related by Subtype.val, but when I first started out I was tripped out for a long time by the fact that various lemmas holding in X that I wanted to use did not seem to be applicable to elements of S.

The situation gets worse when dealing with finite sets of X, which are modeled by no fewer than four different structures: (S : Finset X), (S: Set X) [Fintype S], (S: Set X) (hS: Set.Finite S), and (S: Set X) [Finite S](in two of these cases there is an implicit coercion from a set to its associated subtype). But that (together with some companion discussion on decidable equality) requires a whole separate guide I think...

[Kenny Lau]

Yeah, for example, the confusion with "finite sets" just happened minutes ago in #Is there code for X? > Finite sum over two disjoint sets

[Sabbir Rahman]

There is a general mistake (not sure if a pitfall) that I do of not noticing types of numerals. The same numeral can have different types with no visual distinction in infoview, consider following

import Mathlib

example (x y : ℝ) (h1 : 0 < y) (h2 : y^3 = 10) : y ^ (x + 3) / y ^ x = 10 := by
  rw [← Real.rpow_sub h1]
  ring_nf
  /-
  state now is following, h2 and goal seem same, but they are not
  x y : ℝ
  h1 : 0 < y
  h2 : y ^ 3 = 10
  ⊢ y ^ 3 = 10
  -/
  exact h2  -- doesn't work

Maybe this could also be added

[Floris van Doorn]

This should probably be mentioned as a pitfall:

import Mathlib

example : ⨆ (x : ℝ) (_ : x < - 3), x = 0 := by
  apply le_antisymm
  · refine ciSup_le (fun x ↦ ?_)
    refine Real.iSup_le (fun hx ↦ ?_) le_rfl
    linarith
  · apply Real.iSup_nonneg'
    use 37
    norm_num

[Floris van Doorn]

(oh, @Joseph Myers already mentioned this)

[Floris van Doorn]

Having two non-def-eq instances is another common pitfall (related to the mentioned "don't use have for data" and the "parameters for instances that already exist")

[Floris van Doorn]

Maybe mention #lint somewhere (in the "ignoring warnings" section?), which can also spot some common errors (e.g. syntactic tautologies)

[Floris van Doorn]

This list seems very useful, and we should definitely link it from the learning resources page! I'd also be in favor of making this an official subpage of https://leanprover-community.github.io/

[Niels Voss]

Thank you for all the suggestions everyone! I will try to see if I have time to go through and implement them later today.

[Niels Voss]

Floris van Doorn said:

This list seems very useful, and we should definitely link it from the learning resources page! I'd also be in favor of making this an official subpage of https://leanprover-community.github.io/

I would be willing to move the document anywhere that's best for the community.

[Niels Voss]

GasStationManager said:

Nice work! I remember being surprised by the division by zero (I was working with Rat).

As for something to add: this may be a hot take, but array indexing by Fins. Basically ask them to read this. I'm not sure if anything has changed since then; Functional Programming in Lean still recommends using Fins for indexing. To rank the various indexing options from most safe to least:

• a[i]'bounds_proof. Safe but tedious. Perhaps package the index value i and the bounds_proof together into a Subtype to pass around.
• a[i]? I truly am not sure whether i is in bounds or not
• a[i]! I am a Java/Python programmer; I sometimes venture into C++ but use .at() instead of []. If I make a mistake, my program will at least give a runtime error.
• a[i] with Fin type index. I write C/C++ and live on the edge. I just want to turn off bounds checking. If I make a mistake, which I won't.... valgrind will catch it, right?...

The last option is so convenient, I sometimes use it because I was too lazy to do the safer way. I'm a C++ programmer, what can say...

I just tried this and as far as I can tell, the xs[n] notation doesn't seem to assume that n is a Fin unless you explicitly give it that type. It seems to me that the only unintuitive part is that Fin arithmetic is wrapping and I don't see any issues with the indexing notation.

[Niels Voss]

I will however be adding a section on how Fin arithmetic is wrapping and how Fin is different from ZMod

[Niels Voss]

Changelog:

• Added note about using rfl to detect mismatching instances
• Added section on using Sets as types and the implicit coercion to Subtype
• Added note about #lint to the ignoring warnings section
• Added section about wrapping arithmetic in Fin

TODO:

• Add section on the counterintuitive iInf behavior mentioned in this thread
• Describe the different ways to describe Finite sets (maybe this should just be a short section with a link to a more detailed description in another resource?)
• (Maybe) Add section on the difference between Prop and Bool, True vs true, and = vs ==.

[Kyle Miller]

Niels Voss said:

• a[i] with Fin type index. I write C/C++ and live on the edge. I just want to turn off bounds checking. If I make a mistake, which I won't.... valgrind will catch it, right?...

I'm confused about the claim that a[i] is unsafe in a memory safety sense @GasStationManager. If i : Fin a.size, then a[i] is exactly the same as a[i.1]'i.2, right? The "unsafe" part is just that the arithmetic silently wraps around and you might not get the element you thought you were getting.

[GasStationManager]

@Kyle Miller I didn't mean to suggest that a[i] is memory unsafe, sorry for being unclear. I guess what I meant is that silently wrapping is sometimes even worse, in that it's harder to debug; in C/C++ if you go out of bounds at least tools like valgrind can catch it. And good C programmers know they are living on the edge and are willing to use tools like valgrind, whereas a[i] with Fin gives you a sense of security, that i is "proven" to be in bounds, so don't even think of looking here for bugs.

[GasStationManager]

I do think a[i] with Fin can be done safely, just like C/C++ style array access can be safe. You just need to make sure the rest of your code's logic has not accidentally wrapped the index around. So if it is a simple loop or forall over the values of Fin a.size, it should be fine.

[Kyle Miller]

Ah I see, your question "valgrind will catch it, right?" is following Betteridge's law of headlines: no, no it won't.

[Kevin Buzzard]

People like addition wrapping on Fin because without it you can't use + at all without jumping through hoops supplying proofs. Presumably C++ programmers expect to be able to use "unsafe +" but in Lean "unsafe +" is either "inconvenient + where you have to supply proofs every time" or "+ taking values in Option" (also super-inconvenient) or "+ taking junk values". I have suggested removing + from Fin n completely on the basis that if you want to add things you should just add a.1 and b.1 and then supply the proof that a.1+b.1<n yourself) (didn't go down well) and I've also suggested that + saturates on n-1 (also didn't go down well) and I am always happy to point out that if you want wrapping + then we have ZMod n which everyone expects to have a wrapping +; at the end of the day I don't really get why we have + on Fin n at all but apparently some people want it enough to think it's OK that other people will get totally confused by it. We get regular questions on the Zulip from people who can't figure out why (2 : Fin 3) + (2 :Fin 3) works.

[Niels Voss]

Does what I've added to the document yesterday (under "Wrapping arithmetic on Fin") cover this to a sufficient extent?

[Shreyas Srinivas]

Has the #eval vector indexing issue been fixed? It used to be the case that #eval would sorry out proof obligations like the index check on Vector if it couldn’t find a proof and then promptly crash the editor if the index was out of bounds. If this is unfixed or has been deemed fine then it could count as a pitfall.

[Kyle Miller]

#eval gives an error if the term depends on sorry in any way now

[Shreyas Srinivas]

There was also that issue of creating an array of size exactly 33 or something. Upto 32 it would work fast and after that lean would grind to a halt. This was pointed out only a few months ago

[Shreyas Srinivas]

I think this could be flagged under one pitfall “it is hard to predict when FBIP or some C implementation kicks in when writing functions without looking carefully at the IR” or more succinctly “FBIP is highly non trivial”.

[Shreyas Srinivas]

Another point: the discussion on native_decide should also mention other such tactics like csimp and bv_decide

[Terence Tao]

Here is another pitfall: spending a lot of time looking for an "obvious" lemma that is, in fact, true by definition.

For instance, when I was still new to Lean I had at some point wanted to proveFunction.Injective f for some f. I spent a fair amount of time scouring Mathlib for some sort of Function.injective_iff type lemma that would equate this with the assertion that if f x = f y then x = y (or maybe the contrapositive of this statement). It took an embarrassingly long amount of time before I actually opened the definition of Function.Injective and saw that this lemma I needed was in fact true by definition, and I could just directly open up this claim with intro x y hxy and continue with the proof. So I guess the point is that one should actually inspect the formal definition of key mathematical concepts and not just rely on the API.

EDIT: okay, docs#Function.injective_iff_pairwise_ne and docs#Function.not_injective_iff do exist, but hopefully my broader point still stands.

[Shreyas Srinivas]

I think that situation has improved quite a bit with exact? and apply?

[Shreyas Srinivas]

These days if I don’t know how to prove it, I set up a simple example and play around with these tactics until I find the correct lemma.

[Terence Tao]

Fair enough. For instance with

import Mathlib

example : Function.Injective (fun (x:ℝ) ↦ 2 * x) := by
  hint

The first suggestion is indeed intro, which is a good start.

Another example is subset inclusion: one can get started on proving A ⊆ B with intro x hx rather than try to look for something like an axiom of extensionality (there is no Set.subset_iff method in Mathlib).

[Kyle Miller]

That's docs#Set.subset_def

[Kyle Miller]

(not an iff for some reason)

[Terence Tao]

OK, that was embarrassing. Perhaps my experience is outdated, coming from a time when Mathlib was somewhat less developed. Would it be standard practice nowadays to add some concept_iff or concept_def lemmas that are true by rfl every time a new Concept is defined?

I guess one could also just unfold any definition within tactic mode. Perhaps I should simply withdraw this suggested addition to the document. (Though perhaps it is still worth making the point that Mathlib doesn't operate on a 100% "object-oriented programming" philosophy, in that it still assumes that the Mathlib user is willing to unfold objects and classes to use their implementation, rather than just the provided API.)

[Kyle Miller]

I've never really known when to add _iff/_def lemmas and when not. If they're exact statements of definitions, they're superfluous, since there are auto-generated such lemmas (e.g. Function.Injective.eq_def, which doesn't show up in documentation, but which has the type ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂), but on the other hand since they don't show up in documentation it can be hard to know if it's something you're supposed to rely on or not.

Sometimes there are definitions that seem like they could change. In those cases having definition lemmas is nice, but if you know in advance the definition might change, maybe it should be changed immediately...

Definition lemmas that characterize a definition are nice though. For example, that Nat.find gives the least natural number satisfying a predicate, rather than the concrete implementation.

[Niels Voss]

More generally, mathlib isn't great at making it clear what is supposed to be considered an implementation detail or not. The "classic example" of an implementation detail in Mathlib is Set X being defeq to X -> Prop but I'm willing to bet that if we changed the definition of Set X a ton of mathlib would break. Of course, there's the argument that since Mathlib doesn't make any attempt to be backwards incompatible, we don't have to worry as much about this.

[Shreyas Srinivas]

So the thing is there are easy ways to go between iff and =. There is docs#propext in one direction and docs#Iff.of_eq` in the other.

[Shreyas Srinivas]

Also rw works with both kinds of statements

[Shreyas Srinivas]

So the distinction is practically just in the name.

[Niels Voss]

I think the question is not whether the lemma should be iff of = (although that is a reasonable question), but whether either type of lemma should be added at all, or if we should just rely on tactics like unfold

[Shreyas Srinivas]

Don’t we have rewriting with definitions now? Isn’t that the main purpose of these iff and def lemmas?

[Kyle Miller]

We've had rewriting with definitions for a long time, pre Lean 4

[Shreyas Srinivas]

Then it probably makes sense to have iff lemmas since it takes some standard extra steps over unfold to go from a definition to an iff lemma and from that to an mp or mpr.

[Ruben Van de Velde]

I think it's definitely a good idea to have lemmas like that, even without the "maybe we'll change the definition" argument (which I subscribe to as well). For example, I recently used subset_def so I could apply a simp lemma for x \in (one of the sets in the subset expression)

[Terence Tao]

Perhaps one could add the functionality to allow an automatically generated lemma to be explicitly added to the documentation via some suitable line in the Lean file? Not sure what the right syntax would be here but I'm thinking something like @[document] Function.Injective.eq_def.

[Ruben Van de Velde]

I'm less convinced that we want to rely on the automatically generated lemma, though, since I think the lemma should be stable under changes to the actual underlying definition

[Ruben Van de Velde]

But it could still be useful to have it in the documentation, of course

[Terence Tao]

One could flag it in the documentation as auto-generated

[Yaël Dillies]

Kyle Miller said:

We've had rewriting with definitions for a long time, pre Lean 4

def foo : Nat := 0

example : foo = 0 := by simp [← foo]
-- invalid '←' modifier, 'foo' is a declaration name to be unfolded

:sad:

[Yaël Dillies]

The day simp allows me to refold definitions, I will start claiming that we truly have "rewriting with definitions" and have a strong argument against adding all those _def and _iff lemmas

[Michael Rothgang]

Some tactics are documented in the reference manual, but some are mathlib specific. Is there a centralized documentation location for tactics?

Are you aware of the mathlib manual? https://leanprover-community.github.io/mathlib-manual/html-multi/Tactics/All-tactics That has a list of all tactics.

[Michael Rothgang]

I just finished reading the whole document. Thanks a lot for compiling this; it's great to have such a list (and I also learned a thing or two).
I have two small comments/suggestions:

• about the unicode characters table: move the asterisk next to the "vertical dots"? Right now, between * and various central dots there are various arrows (which look quite different).
• non-terminal simps: do you know about the flexible linter and the distinction between flexible and rigid tactics? (This has definitely been discussed on zulip, I'm not sure if it's documented anywhere else already. It probably should be...)

[Jannis Limperg]

Ruben Van de Velde said:

I'm less convinced that we want to rely on the automatically generated lemma, though, since I think the lemma should be stable under changes to the actual underlying definition

You could have a command like

generated_def foo : Bar

which checks whether a lemma foo with type Bar exists. This would ensure that changes in the auto-generated lemma don't go unnoticed. There could also be a code action that adds the type after generated_def foo.

[Shreyas Srinivas]

If the idea is that these lemmas are a stable API to a potentially changing definition, then they should probably not be autogenerated

[Michael Rothgang]

Could the papercut linter be extended or modified to catch constants in mathlib which are floats? (Perhaps that one will land more quickly; I'm certainly happy to review it.) Or is there some use of them in mathlib that I have overlooked?
CC @Damiano Testa

[Michael Rothgang]

I'm also wondering: could or should the papercut linter be modified to catch addition (or multiplication) on Fin n --- within mathlib, where ZMod is presumably what the user wants instead?

[Jannis Limperg]

Shreyas Srinivas said:

If the idea is that these lemmas are a stable API to a potentially changing definition, then they should probably not be autogenerated

I don't see the downside of auto-generated definitions in combination with my proposal. If the definition changes, the generated_def throws an error and you replace it with an actual theorem to preserve the API. I guess if you care about defeqs of the auto-generated definition, you'd need to include these as well.

[Damiano Testa]

Catching floats with a linter is pretty easy. The linter cannot simply inspect the syntax, since floats do not have a unique dedicated kind, but examining the infotrees, or the resulting expression you can detect the presence of Floats.

[Damiano Testa]

The papercut linter is currently dormant: I got stumped while trying to make it more aware of the local context and then got sidetracked by other issues.

[Damiano Testa]

I do not exclude going back to it, but it will probably not be in the short term. If someone else wants to bump it and revive it, I would be happy to take a look!

[Bhavik Mehta]

Yaël Dillies said:

Kyle Miller said:

We've had rewriting with definitions for a long time, pre Lean 4

def foo : Nat := 0

example : foo = 0 := by simp [← foo]
-- invalid '←' modifier, 'foo' is a declaration name to be unfolded

:sad:

def foo : Nat := 0

example : foo = 0 := by simp [← foo.eq_def]

[Kyle Miller]

Another example of definition lemmas is when you have a field of a structure, and that field is used indirectly in some notation class. You need to write a definition lemma to unfold that notation for that structure in a controlled manner. Recent example: #lean4 > ✔ Simplifier simplifying too much @ 💬

[Niels Voss]

I've been busy these past two weeks, so I didn't finish the document yet, but I'm hoping to finish implementing the rest of the suggestions in this thread within the next few days. I just added a section on the difference between Prop and Bool.

[Niels Voss]

That being said, I'm happy to hear more suggestions if anyone has any

[Wrenna Robson]

I like this document.

[Wrenna Robson]

Regarding using Fin for indexing: this isn't simp-normal, is it? Morally speaking I like using Nat for indexing but trusting in get_elem_tactic most of the time so I don't explicitly have to give a proof for it.

[Wrenna Robson]

I think something I would say is true, I'm not sure if it's a pitfall or not, but morally speaking every def statement, I believe, creates a mortgage that one has to pay back with the creation of suitable API.

[Wrenna Robson]

I think when one is starting out one defines a lot of stuff, but over time you begin to realise that that's just a way to spend a lot of time unwrapping things or ending in lemma hell.

[Niels Voss]

I'd have to check tomorrow but I don't think using Fin for indexing is actually the default; if you don't mention Fin I don't think your code will do wrapping arithmetic

[Wrenna Robson]

Definitions have meaning, I believe, only when they connect into an existing set of definitions that are robust.

[Wrenna Robson]

A "formalisation" that just makes definitions and proves stuff about those definitions with reference to each other isn't in my view very meaningful.

[Wrenna Robson]

There is a real skill in making a "good" definition I find. Perhaps that's more true in some contexts than others.

[Wrenna Robson]

Something you could mention, which I think in some ways is more of a Mathlib thing but is true in general, is how you declare that something is a group.

In maths obviously the normal way is to say "G is a set with an operation yadda yadda". But obviously in Mathlib G is normally a type and we then assert the existence of a Group G instance.

[Wrenna Robson]

Related, there's probably something about propositional and definitional equality and the perils of instance diamonds that you could add.

[Niels Voss]

If I were to add a section on definitions, I guess it could be called "Overuse of definitions"

[Niels Voss]

Would it make more sense if there was a dedicated "tips for writing definitions" document?

[Niels Voss]

I can try to add a section on definitional vs propositional equality. What would you say is the most likely problem new users run into when they aren't aware of this distinction?

[Niels Voss]

Shreyas Srinivas said:

There was also that issue of creating an array of size exactly 33 or something. Upto 32 it would work fast and after that lean would grind to a halt. This was pointed out only a few months ago

I think this could be flagged under one pitfall “it is hard to predict when FBIP or some C implementation kicks in when writing functions without looking carefully at the IR” or more succinctly “FBIP is highly non trivial”.

I can see how this would be a pitfall, but I don't actually know what this error is or what FBIP is. So I don't think I'm qualified to write about this unless you can provide me a link to a discussion. Also, do we know if this is going to be fixed when the new compiler releases?

[Niels Voss]

Shreyas Srinivas said:

Another point: the discussion on native_decide should also mention other such tactics like csimp and bv_decide

I thought csimp was an attribute, not a tactic? Also, is bv_decide really as risky as native_decide (as in, does it let you depend on an unbounded number of extensions to the compiler?)

[Henrik Böving]

No it doesn't

[Kyle Miller]

For that array issue, I think Shreyas is referring to this thread, and as far as I understand it is not related to FBIP.

[Niels Voss]

Is this something you would recommend be mentioned in this document? My opinion is that if it is counterintuitive behavior that is unlikely to be changed any time soon, it belongs in the pitfalls document, but if it is a bug that will most likely be fixed at some point in the near future it should not be added.

[Shreyas Srinivas]

bv_decide definitely extends the TCB, albeit for good reasons, and users should be aware of this.

About that error in vectors. That’s the one Kyle mentioned, and now I recall that it had something to do with macro expansion and has probably been fixed, or it not, will get fixed eventually.

[Niels Voss]

That's true, but it's much less extreme than native_decide, because native_decide also extends your circle of trust to include an arbitrary set of user-defined extensions that are like axioms but are not tracked.

[Niels Voss]

Changelog:

• Added section describing the counterintuitive double iInf and iSup behavior
• Added section on trying to extract data from propositions, and why this isn't possible / what alternatives there are

[Jz Pan]

but you cannot match on terms of type Prop

Maybe you want to give a workaround how to "match" on terms of type Prop: if p : Prop, then the correct spelling of "match p" should be by_cases hp : p

[Terence Tao]

Perhaps this is well trodden territory, but one common pitfall for beginners arises when trying to apply a rewrite to an expression which is only definitionally equal (or even merely propositionally equal) to the expression one is trying to match with. For instance, applying a rewrite that uses a hypothesis a < b to an expression that instead involves b > a. This particular obstacle arises frequently because most Mathlib lemmas are only expressed using the former (which is in simp normal form etc.) rather than the latter. In this particular case of course one just needs to rewrite using gt_iff_lt first, but I've seen this be a significant speedbump for beginners.

[Niels Voss]

Terence Tao said:

Perhaps this is well trodden territory, but one common pitfall for beginners arises when trying to apply a rewrite to an expression which is only definitionally equal (or even merely propositionally equal) to the expression one is trying to match with. For instance, applying a rewrite that uses a hypothesis a < b to an expression that instead involves b > a. This particular obstacle arises frequently because most Mathlib lemmas are only expressed using the former (which is in simp normal form etc.) rather than the latter. In this particular case of course one just needs to rewrite using gt_iff_lt first, but I've seen this be a significant speedbump for beginners.

I decided to split this into two sections: one about how tactics don't always operate up to definitional equality, and another specifically about a < b vs b > a. Please let me know if this covers your suggestion sufficiently.

[Terence Tao]

Looks good to me!

[Niels Voss]

Floris van Doorn said:

This list seems very useful, and we should definitely link it from the learning resources page! I'd also be in favor of making this an official subpage of https://leanprover-community.github.io/

How would I go about making this an official subpage? Should I submit a PR to https://github.com/leanprover-community/leanprover-community.github.io/ ?

[Terence Tao]

One addendum to the natural number subtraction section: One often has to work with the positive natural numbers, and prove statements such as ∀ n ≥ 1, P n where one naturally tends to encounter n-1 at some point (particularly if doing some sort of induction argument), thus apparently forcing one to use the dreaded natural number subtraction. But one can often sidestep this by replacing ∀ n ≥ 1, P n from the start with ∀ n, P (n+1), so that any previous appearance of n-1 is now n, and no natural number subtraction is required. (This also makes positivity and related tools such as gcongr work better, and also slightly reduces the "double iInf/iSup" issue that you also refer to.)

[Bryan Gin-ge Chen]

Niels Voss said:

How would I go about making this an official subpage? Should I submit a PR to https://github.com/leanprover-community/leanprover-community.github.io/ ?

Yes, please! Feel free to ping / DM me if you have any trouble.

[Niels Voss]

I am going to finish implementing the last few suggestions, then I'll submit a PR :)

[Niels Voss]

Jz Pan said:

but you cannot match on terms of type Prop

Maybe you want to give a workaround how to "match" on terms of type Prop: if p : Prop, then the correct spelling of "match p" should be by_cases hp : p

Done, and I also mentioned the dependent if-then-else statement as well.

[Niels Voss]

Changelog:

• Implemented Terence Tao's suggestion on avoiding natural subtraction
• Add section on why you should avoid working with equality of types

[Niels Voss]

Changelog:

• Add section about rewriting under binders, which mentions simp_rw and conv

[Weiyi Wang]

I really enjoy the read! one nitpick: in the partial function / sSup part, it should mention sSup is 0 also for empty set. And I think the sqrt =sSup example there is actually demonstrating this

[Niels Voss]

Weiyi Wang said:

I really enjoy the read! one nitpick: in the partial function / sSup part, it should mention sSup is 0 also for empty set. And I think the sqrt =sSup example there is actually demonstrating this

Done, thanks for the suggestion!

[Terence Tao]

Another pitfall: treating a symbol introduced by let or set as if it were a genuine variable, for instance starting with set n := expr and then attempting induction n or something similar. In such cases, generalize h:expr = n works as a substitute for set n := exprthat gives the symbol n the status of a true variable, allowing for tactics such as induction or revert to work.

[Kyle Miller]

I think you should be able to do induction h : n now, which does the generalization step for you.

[Niels Voss]

The document is now available on the community website here: https://leanprover-community.github.io/extras/pitfalls.html. Thank you to everyone for all your feedback and suggestions, and thank you to @Bryan Gin-ge Chen for helping me get this contributed to the website. I'm still open to suggestions for improvements to the document, which can be mentioned in this thread.

[Kyle Miller]

"and rw is unable to look into the fun expression."

This is a common misconception: the failure is that rw can't rewrite subexpressions that contain bound variables. It's able to rewrite under fun/forall/let except for that.

E.g. if you had fun x => n + 0 + x with n in the local context, you could do rw [Nat.add_zero].

[Weiyi Wang]

Speaking of rw, another thing that I'd like to see more explanation on is the "motive is not type correct" error, which can probably be considered a pitfall. For example

import Mathlib
def f : Fin 3 → ℕ := sorry
theorem foo (x: Nat) (h1 : x < 3) (h2 : f ⟨x, h1⟩ = 7) (h3 : x = 2) : f ⟨2, by simp⟩ = 7 := by
  -- rw [← h3]  -- doesn't work
  simp_rw [← h3]
  exact h2

I myself hasn't fully understood this yet. All I know is this often occurs with dependent types, and simp_rw / conv mode can usually resolve it (but simp_rw also sent me into infinite recursion in some occasion)
(Please find a better example than this weird one)

[Kyle Miller]

@Weiyi Wang It might be helpful searching for "motive not type correct" on this Zulip, since there are a number of explanations. The tactic also tries to explain the issue in its error message.

[Niels Voss]

Kyle Miller said:

This is a common misconception: the failure is that rw can't rewrite subexpressions that contain bound variables. It's able to rewrite under fun/forall/let except for that.

E.g. if you had fun x => n + 0 + x with n in the local context, you could do rw [Nat.add_zero].

I updated the document to fix this.

[Terence Tao]

One might isolate within the "Using have for data" pitfall the special case "Using have for instances" which tripped me up recently. I had a finite type (E:Type) [Finite E] and I needed the Fintype E instance so I carelessly wrote have hEfintype : Fintype E := Fintype.ofFinite _ and then ran into instance diamonds later on because Lean could not work out that hEfintype was equal to Fintype.ofFinite _. Of course replacing have with let solved the problem. This is the identical problem to the existing "Using have for data" section in the pitfalls document, but I think the instance subcase is frequent enough that it is worth noting.

[EDIT: perhaps it is also worth clarifying that only some instances carry data, and for propositional instances this issue does not arise.]

[Jason Reed]

which tripped me up recently...

This also hit me recently, not because I actually needed to refer to the instance in my proof, but because I had simply added the line by way of debugging to make sure that the Fintype instance was derivable as I expected. My not-so-minimal mwe is:

import Mathlib

noncomputable
def proj_subspace {I : Type} [Fintype I] [DecidableEq I] (i : I) : Submodule ℝ (EuclideanSpace ℝ I) :=
 LinearMap.ker (LinearMap.proj i)

noncomputable
def proj_subspace_has_dim_one_less {I : Type} [Fintype I] [DecidableEq I] (i : I) :
  EuclideanSpace ℝ { j // j ≠ i } ≃ₗᵢ[ℝ] ↥(proj_subspace i) := by
  let basis := Pi.basisFun ℝ {j : I // j ≠ i}

  let J := {j : I // j ≠ i}
  ---- UNCOMMENT the following line and break the partial proof
  -- have fintypeJ : Fintype J := inferInstance
  let setmap : J → proj_subspace i := sorry

  have inj : EuclideanSpace ℝ {j : I // j ≠ i} ≃ₗ[ℝ] proj_subspace i := sorry
  have pres_norm : ∀ (x : EuclideanSpace ℝ { j // j ≠ i }), ‖inj x‖ = ‖x‖ := sorry
  have z := LinearIsometryEquiv.mk le pres_norm
  exact z

[Yaël Dillies]

Terence Tao said:

I carelessly wrote have hEfintype : Fintype E := Fintype.ofFinite _ and then ran into instance diamonds later on because Lean could not work out that hEfintype was equal to Fintype.ofFinite _. Of course replacing have with let solved the problem.

I don't understand how this situation could have caused any issue. Either hEfintype is defeq to Fintype.ofFinite _, or it is not, but what you're describing is a mix of both, and no lemma in mathlib should mention Fintype.ofFinite _ explicitly.

[Yaël Dillies]

Do you have a repro we could look at? Probably there is so lemma somewhere in mathlib that was stated wrongly

[Weiyi Wang]

I don't know if it is the same issue, but not long ago I wrote an adhoc have : One M :=.... Then when I want to use the 1 from it, it didn't work because have forgets what 1 is. Changing it to let resolved the issue

[Yaël Dillies]

Did you want to use the definition of 1 : M, or just that it was defined?

[Weiyi Wang]

I wanted use the definition and indeed that was the problem

[Yaël Dillies]

Okay, so indeed that is expected. What Terry is describing above is rather a case where one shouldn't need to use the definition, but one somehow still gets issues (?!)

[Terence Tao]

OK, I see now that the problem was self-inflicted. I was writing code for involving Finset.sum in which the ambient space had a Finite instance but not a Fintype instance, so that Finset.univ was not defined. I dealt with this by manually inserting the Fintype instance into the Finset.univ call, and then later on when I wanted to use this expression I introduced the Fintype instance again, but mistakenly used have instead of let causing an instance diamond. Here is the MWE (which looks silly now that I see it, but in my original code the manual insertion of Fintype and the second introduction of Fintype were in very different locations and I didn't see the issue.

example {X Y:Type} {e: X → Y} (f: Y → ℝ) (he: Function.Bijective e) [Fintype X] [Finite Y] :
  ∑ x, f (e x) = ∑ y ∈ @Finset.univ Y (Fintype.ofFinite Y), f y := by
    let hYfintype : Fintype Y := Fintype.ofFinite Y  -- fails if `let` becomes `have`
    exact he.sum_comp f

[Yaël Dillies]

Glad it's sorted out!

[Jason Reed]

Preferring to avoid defeq abuse seems to be a recurring theme in discussions, but I don't know if it's documented nicely in one place. Is the "Pitfalls" section a good place for an example of what can go wrong? I don't think I'm an expert enough to suggest a good one. I only remember encountering some issues in the context of Fin n → ℝ vs. EuclideanSpace ℝ n.

[Jason Reed]

(or is https://leanprover-community.github.io/extras/pitfalls.html#working-with-equality-of-types already capturing everything worth saying at a beginner level? I got the impression that the phrase "defeq abuse" meant more than the issues discussed there, somehow)

[Niels Voss]

That section is about propositional equality of types, which is much worse behaved than definitional equality of types. I think defeq abuse is more about when you have an x : A and A is definitionally equal to B, so you use x : B instead of x.toB, but later find out that A and B are not actually interchangeable (for example, maybe they have different typeclasses)

[Niels Voss]

That said, I think defeq abuse shows up in other contexts than just that. I think over-reliance upon unfolding rather than developing proper APIs could be seen as a type of defeq abuse

[Eric Wieser]

I think your penultimate message represents the vast majority of the defeq abuse that actually matters

[Yaël Dillies]

Yes, applying hf : Injective f (docs#Function.Injective) is not defeq abuse in my book, even though Kevin has called it that in the past

[Aaron Liu]

If you use it enough it becomes not defeq abuse