synport experimentation

Stream: mathlib4

[Floris van Doorn]

Using the synport/binport that @Daniel Selsam posted, I did an experiment by taking the synported file of measure_theory/measurable_space_def.lean, and manually fixing all (most) things until the file compiled (I didn't go through correctly camelCasing names). It was quite some work, but there were a lot of minor things that could probably be done by an improved synport.
After I finished, I realized that this wasn't exactly the experimentation that Daniel asked for, but I'll post my findings here anyway. Hopefully they are helpful.
Many of these points are (probably known) issues with synport, but there are definitely also some things that are me just being unfamiliar with Lean 4 (and binport/synport).
First of all, I'd like to say that both binport and synport are very nice tools that already work very well!

• camel casing errors:
  • The field MeasurableSet' of MeasurableSpace was camel cased in the first occurrence, but not any time later in the file.
  • countable and finite were not capitalized
  • Ideally lemmas like measurable_set_empty are automatically camelCased as measurableSet_empty.
  • these got an incorrect capital letter when camel casing: (? : MeasurableSet _).Compl, Set.Union, Set.SInter, Set.SUnion, ... (presumably because these are Prop's after unfolding?)
• Some notation was not working:
  • ⋃ (probably because I'm importing binported files, not synported files? The notation3 I saw to declare it also didn't work, presumably for the same reason?)
  • ∅ (missing instance?)
  • ᶜ (no localized notation)
• Tactics that are not implemented:
  • simpa using
  • rwa
  • byCases
  • ;
  • exacts
  • rfl for other reflexive relations
• Notation that is not implemented
  • ‹...›
  • { a : α | p }
  • {x}
• commands that are not implemented
  • open_locale/localized
• some declarations (MeasurableSet.bUnion_decode₂) have more explicit arguments than the Lean 3 version (⦃⦄ is translated to ()?)
• parentheses:
  • ∀ b ∈ s is translated as ∀ b _ : b ∈ s instead of ∀ b (_ : b ∈ s)
  • assume t (ht : generate_measurable s t) is translated as fun t ht : generate_measurable s t
• All simp calls I've tried gave me the error

(deterministic) timeout at 'typeclass', maximum number of heartbeats (500) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

• spacing

  • a lot of spaces after identifiers/commands are eaten
  • if an argument to a tactic is missing, there is a superfluous space after translation:
    have p -> have p or simpa using -> simpa using.

• λ should sometimes be replaced by @λ

• the default value for Lt in Preorder seems to be missing
• The code

theorem subsingleton.MeasurableSet [Subsingleton α] {s : Set α} : MeasurableSet s :=
subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

gives the error

ambiguous, possible interpretations
  Subsingleton α

  Subsingleton (pure α)

I don't know how to specify that I don't want a "pure" inserted.

• In

theorem Set.finite.MeasurableSet {s : Set α} (hs : Finite s) : MeasurableSet s :=
  Finite.induction_on hs _root_.MeasurableSet.empty λ ha hsf hsm => hsm.insert _

the _root_ is necessary, because otherwise MeasurableSet is interpreted as a recursive call of the function...

• Two Lean 4 questions:
  • Is there a #print notation equivalent? Something like #print notation +?
  • What is the equivalent of open_locale classical?

[Mario Carneiro]

What is the equivalent of open_locale classical?

It should be translated to open_locale Classical

[Mario Carneiro]

Note that synport is not (yet) elaborator-aware, so things like \lam -> @\lam aren't easily addressable right now

[Mario Carneiro]

but missing syntax and weird formatting can probably be addressed sooner (although I haven't thought about what to do about weird formatting in core yet)

[Sebastian Ullrich]

Floris van Doorn said:

- Is there a #print notation equivalent? Something like #print notation +?

No, but you can use go-to-definition on any use of + (and any other syntax as long as it's imported and not contributed by native code, like many builtins are without import Lean)

[Mario Carneiro]

go to definition seems to take me to the definition of app a lot

[Sebastian Ullrich]

Haha, that's the one syntax it shouldn't be able to go to since there is no atom to click on. But it's been a while since I've used it.

[Mario Carneiro]

I often get go to definition hovers that cover the whole command and go to def or something. It's not just atoms

[Mario Carneiro]

for example, hovering on rcases here:

def foo := by rcases x

highlights rcases x and takes me to evalTacticSeq1Indented

[Patrick Massot]

It would be really nice to have a more reliable go-to-definition in Lean 4. In Lean 3 it's always very frustrating when it doesn't work or goes to the definition of the tactic that sits at the beginning of the line.

[Mario Carneiro]

In

def foo := by exact x

hovering over exact also highlights exact x but it takes me to evalExact, so maybe this has something to do with the elabs

[Mario Carneiro]

(since rcases is not implemented in the first example, it just has a syntax declaration)

[Sebastian Ullrich]

Yes, if syntax and elaborator are separate, go-to-definition goes to the elaborator and go-to-declaration to the syntax

[Mario Carneiro]

"no type definition found for 'rcases'"

[Mario Carneiro]

in #check `(by rcases p), hovering on rcases highlights the whole quotation and goes to elab_stx_quot Parser.Term.quot

[Sebastian Ullrich]

Oh yeah, quotations are not special-cased yet

[Mario Carneiro]

what special case is needed? at the syntax level, the rcases parser is called just the same

[Sebastian Ullrich]

Mario Carneiro said:

"no type definition found for 'rcases'"

It's go-to-declaration, my bad

[Mario Carneiro]

That one goes to Parser.Tactic.tacticSeq1Indented

[Sebastian Ullrich]

If it's not implemented yet, that's kind of correct, just not very helpful

[Mario Carneiro]

the parser is implemented, but there is no elab (you get an error saying tactic 'Lean.Parser.Tactic.rcases' has not been implemented)

[Sebastian Ullrich]

Yes, that's what I meant

[Mario Carneiro]

what's the logic behind the kind-of correctness? Is it going up the tree to find something that was elabbed?

[Sebastian Ullrich]

Yes. Many syntax kinds are merely a part of a notation, so we use the surrounding elaborator if any. In quotations, we should just go to the syntax at point instead. The app case might also stem from this.

[Sebastian Ullrich]

It would be great to stop the search at category parser calls, which would fix the tacticSeq1Indented case, but we don't have that kind of information

[Mario Carneiro]

hm, it should be possible to also handle the case where an elaborator is expected but missing, like rcases, and go to the syntax for that node instead of the elab if none is available

[Sebastian Ullrich]

Oh right, we could record missing elaborators

[Mario Carneiro]

and syntax-at-point is useful regardless - that should be an option anywhere (maybe under the go-to-declaration handler)

[Sebastian Ullrich]

It is!

[Mario Carneiro]

right now it looks like syntax-for-elaborator-at-parent-of-point

[Sebastian Ullrich]

Ah yes, I think you are right. Yeah, I'd be happy to replace that one.

[Mario Carneiro]

(I also need to set up a key combination for that, since it seems like VSCode doesn't bind anything to it)

[Sebastian Ullrich]

Haven't even found it in Emacs at all yet, if it is actually exposed

[Sebastian Ullrich]

In any case, do open issues for stuff like this!

[Mario Carneiro]

@Floris van Doorn I pushed a bunch of changes (some from yesterday) that I wish you had available for your test. Some of the issues you mention are already fixed:

• open_locale/localized
• ᶜ
• ‹...›
• the default value for Lt in Preorder seems to be missing

[Mario Carneiro]

For the unimplemented tactics and notation, we are depending on the community to step up and start filling them in. So far I've mostly been trying to avoid outright failures (these are marked by an -- error comment followed by some code that is obviously not correct lean 4 code) and missing things

[Mario Carneiro]

some declarations (MeasurableSet.bUnion_decode₂) have more explicit arguments than the Lean 3 version (⦃⦄ is translated to ()?)

Lean 4 got strict implicits recently, they haven't been hooked up yet fixed

[Floris van Doorn]

Mario Carneiro said:

What is the equivalent of open_locale classical?

It should be translated to open_locale Classical

Presumably after the community has implemented open_locale? Or did you also implement the command (not just the notation?).
I was mostly wondering how to do attribute [instance] classical.dec in Lean 4 (I haven't tried it, so maybe this code just works).

[Floris van Doorn]

Do you know why simp gave me this type-class error? (this would happen on simp without arguments)

[Floris van Doorn]

Nice that you've already implemented a couple of my missing points.

[Floris van Doorn]

Mario Carneiro said:

For the unimplemented tactics and notation, we are depending on the community to step up and start filling them in. So far I've mostly been trying to avoid outright failures (these are marked by an -- error comment followed by some code that is obviously not correct lean 4 code) and missing things

That makes sense. I'll work on porting some stuff to Lean 4 at some point! Is there anything that is useful to have first? Maybe @[to_additive] and @[simps] since they create new declarations themselves?

[Mario Carneiro]

Yes, open_locale will need to be implemented. This is the biggest issue with getting error-free synported files right now - there is no hope of elaborating the files when none of the called tactics exist

[Mario Carneiro]

Everything in the Mathport/Prelude/Syntax.lean file needs to be implemented at some point. I would personally focus on the easy tactics first and work my way to the bigger ones, since that will probably get more things working earlier

[Mario Carneiro]

But things like open_locale and notation3 are particularly important because they can declare new syntax, without which the file won't even parse

[Mario Carneiro]

notation3 should work already, but there might be an issue with the camel case heuristics (which are more problematic in notation since those are elaborated lazily in lean 3)

[Mario Carneiro]

Floris van Doorn said:

Do you know why simp gave me this type-class error? (this would happen on simp without arguments)

My guess is that some translated @[simp] lemma is poison to lean 4 simp

[Mario Carneiro]

Floris van Doorn said:

I was mostly wondering how to do attribute [instance] classical.dec in Lean 4 (I haven't tried it, so maybe this code just works).

I believe the @[instance] attribute still exists in lean 4, so I think the same code works

[Mario Carneiro]

btw localized has the snazzy new notation

localized [Classical] attribute [instance] Classical.dec

no more string quotes needed! (Also be amazed at how we're correctly translating the contents of a string literal that is double-parsed by lean. No external lean 3 parser would be able to achieve this.)

[Daniel Selsam]

Floris van Doorn said:

• some declarations (MeasurableSet.bUnion_decode₂) have more explicit arguments than the Lean 3 version (⦃⦄ is translated to ()?)

The f argument seems to be correctly translated to strict-implicit in Lean4, but strict-implicits were only added to lean4 a few weeks ago and haven't been stress-tested. Can you please be more specific about what behaved unexpectedly?

[Daniel Selsam]

Floris van Doorn said:

• All simp calls I've tried gave me the error

(deterministic) timeout at 'typeclass', maximum number of heartbeats (500) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

The current Lean4 default for synthInstance.maxHeartbeats makes sense for programming applications but is rather ambitious for Mathlib. I should have mentioned that for now I start every file with set_option synthInstance.maxHeartbeats 5000. You may also need to increase the maxHeartbeats flag as well (the default is 50,000 and 200,000 seems reasonable).

[Leonardo de Moura]

@Floris van Doorn Sorry, I didn't read the whole thread, but I want to remind you that we have scoped instances, notation, unification hints, and simp theorems in Lean 4. Scoped elements are activated when we open the namespace. Exaple:

noncomputable def foo (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Error

open Classical

noncomputable def boo (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Ok

[Leonardo de Moura]

You can find more examples in the lean4 tests folder directory. Here are some examples:

scoped syntax:max term noWs "[" term ", " term "]" : term

@[scoped simp] axiom ax1 (x : Nat) : f (g x) = x

scoped infix:65 (priority := default+1) "+" => f

scoped instance : ToString A where
  toString a := s!"A.mk {a.x} {a.y}"

noncomputable scoped instance (priority := low) propDecidable (a : Prop) : Decidable a :=
  choice <| match em a with
    | Or.inl h => ⟨isTrue h⟩
    | Or.inr h => ⟨isFalse h⟩

scoped macro_rules | `(bar! $x) => `($x + 10)

scoped unif_hint (s : Magma) where
  s =?= Nat.Magma |- s.α =?= Nat

[Leonardo de Moura]

Mario Carneiro said:

But things like open_locale and notation3 are particularly important because they can declare new syntax, without which the file won't even parse

Lean 4 has scoped attributes. Why do you need open_locale? Is there something missing in the new scoped attribute feature?

[Daniel Selsam]

Floris van Doorn said:

• The code

theorem subsingleton.MeasurableSet [Subsingleton α] {s : Set α} : MeasurableSet s :=
subsingleton.set_cases MeasurableSet.empty MeasurableSet.univ s

gives the error

ambiguous, possible interpretations
  Subsingleton α

  Subsingleton (pure α)

I don't know how to specify that I don't want a "pure" inserted.

Setting pp.all true provides more information:

error: ambiguous, possible interpretations
  Subsingleton.{?u.15 + 1} α

  @Set.Subsingleton.{?u.15 + 1} (Type ?u.15)
    (@Pure.pure.{?u.15 + 1, ?u.15 + 1} Set.{?u.15 + 1}
      (@Applicative.toPure.{?u.15 + 1, ?u.15 + 1} Set.{?u.15 + 1}
        (@Monad.toApplicative.{?u.15 + 1, ?u.15 + 1} Set.{?u.15 + 1} Set.monad.{?u.15 + 1}))
      (Type ?u.15) α)

It can be made to work by prefixing _root_.Subsingleton or by not opening the Set namespace. I don't have time to investigate right now but Set is a Monad and the pure-injection may be a little too strong here. We may not even want to align Mathlib's monad with Lean4's at all. Also, it is a shame that this isn't visible with default pp settings: the new smart pretty-printer is actually still very dumb regarding open namespaces, since I only tested it on roundtripping from the root namespace.

[Daniel Selsam]

Floris van Doorn said:

• In

theorem Set.finite.MeasurableSet {s : Set α} (hs : Finite s) : MeasurableSet s :=
  Finite.induction_on hs _root_.MeasurableSet.empty λ ha hsf hsm => hsm.insert _

the _root_ is necessary, because otherwise MeasurableSet is interpreted as a recursive call of the function...

Minimized version:

def Foo.empty : Unit := ()
def Bar.Foo : Unit := Foo.empty -- error: invalid field 'empty', the environment does not contain 'Unit.empty'

I agree this is surprising.

[Leonardo de Moura]

The example above may look surprising to Lean 3 users, but it is consistent with the name resolution procedure we designed for Lean 4.
Recall that

def Bar.Foo : Unit := Foo.empty

is expanded to

namespace Bar
def Foo  : Unit := Foo.empty
end Bar

In Lean 4, you don't need to use equations to write recursive functions. As in Lean 3, local declarations have precedence over global ones. So, Foo is the body of the definition is referring to the Foo being defined.
Then, since Foo has type Unit, the dot-notation complains that there is no Unit.empty.

[Floris van Doorn]

Leonardo de Moura said:

Floris van Doorn Sorry, I didn't read the whole thread, but I want to remind you that we have scoped instances, notation, unification hints, and simp theorems in Lean 4. Scoped elements are activated when we open the namespace. [...]

Oh yes, I forgot to ask about this. I agree that with the scoped behavior I don't think we need the localized / open_locale commands anymore. From your example it is clear that both scoped notation and scoped instances work, which are the only uses in mathlib.
@Mario Carneiro do you agree we can get rid of localized / open_locale?

[Floris van Doorn]

@Daniel Selsam thanks for your responses.

• About Singleton/Set.Singleton: Ah, that makes sense. I think having a coercion α → Set α is undesirable, so we should consider making Set.Monad a scoped instance.

[Mario Carneiro]

Leonardo de Moura said:

Mario Carneiro said:

But things like open_locale and notation3 are particularly important because they can declare new syntax, without which the file won't even parse

Lean 4 has scoped attributes. Why do you need open_locale? Is there something missing in the new scoped attribute feature?

My plan, at least, was to translate open_locale directly to a new open_locale command, at least at first, just to keep the translation simple and literal. Scoped attributes can probably replace open_locale, but the implementation is sufficiently syntactically different that it seems easier to do that in a separate refactor after the port. Perhaps there is a way to backport uses of open_locale in mathlib such that they can be more directly replaced by scoped notation.

[Mario Carneiro]

Leonardo de Moura said:

The example above may look surprising to Lean 3 users, but it is consistent with the name resolution procedure we designed for Lean 4.

One of the issues I have hit with this name resolution procedure is that you can't have a definition def foo that makes use of def foo.aux, because it always resolves to the local variable foo. In lean 3, namespaced names take precedence over dot notation, so most of the time this works fine; in equation compiler definitions you can hit this issue because foo is a local variable, but you can still use @foo.aux to refer to it:

def foo.aux := 1
def foo : ℕ → ℕ
| n := @foo.aux

In lean 4 I don't know any workaround other than using _root_ or some other namespace.

I think namespaced names should take precedence over dot notation even on local variables (which is not the case in lean 3 or lean 4 ATM), since you can always force dot notation by using any of the other notations for it - foo .aux, foo |>.aux, (foo).aux, while there is no such backup option for namespaced names (besides using a different name to refer to it).

[Mario Carneiro]

To say more about the open_locale issue, in mathlib open classical and open_locale classical currently do different things, and in particular the second does not imply the first. Excessive use of open leads to frequent name clashes, and I tend to avoid them in most mathlib code I write. So we may need to refactor mathlib such that locales differ from namespaces, and are specifically tailored for the notations, like the old eq.ops namespace from lean 2.

[Leonardo de Moura]

I think namespaced names should take precedence over dot notation even on local variables (which is not the case in lean 3 or lean 4 ATM),

I don't agree.
Here are different ways to write your foo example above in Lean4:

def foo : Nat → Nat
| n => _root_.foo.aux

open foo in
def foo : Nat → Nat
| n => aux

def foo : Nat → Nat
| n => open foo in aux

macro n:ident noWs "#" noWs s:ident : term =>
  `(open $n:ident in $s:ident)

def foo : Nat → Nat
  | n => foo#aux

Note that we can create many different variants of the last one using macros. This is just a simple one.

[Leonardo de Moura]

Mario Carneiro said:

To say more about the open_locale issue, in mathlib open classical and open_locale classical currently do different things, and in particular the second does not imply the first. Excessive use of open leads to frequent name clashes, and I tend to avoid them in most mathlib code I write. So we may need to refactor mathlib such that locales differ from namespaces, and are specifically tailored for the notations, like the old eq.ops namespace from lean 2.

I added the command open scoped that will activate the scoped attributes, but will not "open" the names.

open scoped Classical

#check @epsilon -- Error

noncomputable def foo (f g : Nat → Nat) : Nat :=
  if f = g then 1 else 2 -- Ok

[Daniel Selsam]

Floris van Doorn said:

Daniel Selsam thanks for your responses.

• About Singleton/Set.Singleton: Ah, that makes sense. I think having a coercion α → Set α is undesirable, so we should consider making Set.Monad a scoped instance.

I don't know what mathlib uses that instance for, but it would be great if the scoping could be backported.

[Mario Carneiro]

Leonardo de Moura said:

I added the command open scoped that will activate the scoped attributes, but will not "open" the names.

Thanks. So now open_locale foo can be translated to open scoped Foo. For localized, we would want to translate localized "cmd" in foo to scoped cmd, but with the constraint that we must be in namespace foo when we do it. I think we should backport this, by introducing localized "cmd" without the in foo part, which uses the current namespace (a la #where) to determine what foo should be (and errors in the global namespace).

[Floris van Doorn]

Daniel Selsam said:

I don't know what mathlib uses that instance for, but it would be great if the scoping could be backported.

I expect it is used very little. I'll take a look.

[Floris van Doorn]

Leonardo de Moura said:

I think namespaced names should take precedence over dot notation even on local variables (which is not the case in lean 3 or lean 4 ATM),

I don't agree.
Here are different ways to write your foo example above in Lean4:
[...]
Note that we can create many different variants of the last one using macros. This is just a simple one.

These accidental self-references occur a lot in mathlib. The statement that object foo has property bar is usually called bar.foo (e.g. docs#continuous.max), so that we can use the projection notation. Often in the proof foo is mentioned explicitly. So the more common example of a clash will look like this

def Foo (n : Nat) : Prop := True
def aux := 1
def Foo.aux : Foo aux :=
have h : aux = 1 := rfl
trivial

For example, these are all lemmas in a single file with accidental self-references: (at least on the current commit 897e4ed)
src#set.ord_connected.measurable_set
src#ae_measurable.max
src#ae_measurable.min
src#measurable.is_lub
src#ae_measurable.is_lub
src#measurable.is_glb
src#ae_measurable.is_glb

We could probably make a macro that #foo means _root_.foo, but I'm still worried that it will confuse users.

[Leonardo de Moura]

@Floris van Doorn This is very unfortunate. We have discussed the name resolution in the past and decided that local declarations should take precedence. Note that we did not change that in Lean 4. It looks like a new problem, but it is due to two new features that were requested by users.

1) def Foo.f ... := ... expands to namespace Foo def f ... := ... end Foo

2) We don't need to use equations to write recursive declarations.

To change the name resolution procedure now, we would have to carefully analyze all new issues (and counterintuitive behavior) the change would produce, and carefully spec how it is supposed to work. Even if we do all this work, I can see other users complaining that they have to write foo .aux, foo |>.aux, or (foo).aux because local variables do not take precedence.

Remarks:

• If we add a mechanism for stating that a declaration is not recursive (i.e., disabling feature 2 above), then the problem is gone.
• The protected keyword is another possible workaround. The local declaration will not be atomic.

[Mario Carneiro]

Even if we do all this work, I can see other users complaining that they have to write foo .aux, foo |>.aux, or (foo).aux because local variables do not take precedence.

Note that foo.aux should still work to refer to field projection of aux on local variable foo, provided that foo.aux does not also resolve to something in the current namespace/opens. Since most local variables have lowercase names and most namespaces have uppercase names, I think that collisions of this sort should be rare, but when they do occur, a single character to disambiguate them seems like a small price to pay.

[Leonardo de Moura]

@Floris van Doorn Consider the following example you linked

lemma ae_measurable.min {f g : δ → α} {μ : measure δ}
  (hf : ae_measurable f μ) (hg : ae_measurable g μ) : ae_measurable (λ a, min (f a) (g a)) μ :=
⟨λ a, min (hf.mk f a) (hg.mk g a), hf.measurable_mk.min hg.measurable_mk,
  eventually_eq.comp₂ hf.ae_eq_mk _ hg.ae_eq_mk⟩

Unless we add the feature stating that ae_measurable.min is not recursive, the min inside will still refer to the lemma being defined.

[Mario Carneiro]

Another issue caused by (1) is that it is impossible to have a mutual def between declarations named foo and foo.aux

[Leonardo de Moura]

@Mario Carneiro The example above shows that the change in the name resolution procedure will not even fix the problem.

[Mario Carneiro]

because you can't put a namespace declaration in the middle of a mutual block

[Leonardo de Moura]

Mario Carneiro said:

Another issue caused by (1) is that it is impossible to have a mutual def between declarations named foo and foo.aux

Let's focus on the problems that affect Mathlib.

[Mario Carneiro]

I think that (1) is a bit too aggressive for a lot of uses, but I would like to get more objective data on the relative benefits

[Mario Carneiro]

in particular once you are in the def there is no way to "cancel" the namespace that you have been put into

[Mario Carneiro]

and so you basically get problems similar to overuse of open

[Mario Carneiro]

Looking at ae_measurable.min, I think it would be fine to use _root_.min in that particular case. We already have plenty of other examples like it which use the equation compiler, and we just use _root_ in that case

[Leonardo de Moura]

@Mario Carneiro This kind of discussion is very time-consuming. It takes time to find holes in the suggestions. I will try to summarize the thread

• The change in the name resolution procedure will not fix the problem. See ae_measurable.min example above.
• Feature (1) was supported by many users. If I remember correctly @Reid Barton was the first one that suggested it. We had written a lot of Lean code, and can confirm it works really well.

[Mario Carneiro]

Feature (1) was supported by many users. If I remember correctly @Reid Barton was the first one that suggested it. We had written a lot of Lean code, and can confirm it works really well.

Hence the need to get examples together that show the advantages and disadvantages. Clearly both options have downsides, and I don't know what the relative magnitude of the downsides are, and the cost of the workarounds when you get the wrong thing by default and want the other one

[Mario Carneiro]

What kind of code benefits the most from (1) and/or would be much more verbose without it? The simple desugaring suggests that it is possible to get the effect of (1) with a def-like macro (possibly even switching the names around so that def is the macro and def' is the core command)

[Mario Carneiro]

it would be easy enough to have synport produce def' instead of def whenever the name of the def contains a dot

[Floris van Doorn]

I agree that this is an unfortunate situation, and I don't know the best solution.
An option to disable (2) would be ok (so that you have to write at least one equation | ... => ...to enable a recursive call), but it's not ideal. (I expect we will want to use this option in most mathlib files).

[Leonardo de Moura]

Floris van Doorn said:

I agree that this is an unfortunate situation, and I don't know the best solution.
An option to disable (2) would be ok (so that you have to write at least one equation | ... => ...to enable a recursive call), but it's not ideal. (I expect we will want to use this option in most mathlib files).

Yes, the | ... => ... style was criticized a lot in the past. We should not go back to it.
One option is to still use the name ae_measuable.min for the local declaration even after we perform the macro expansion on theorem ae_measurable.min. But some users may protest that def Foo.f ... := ... would not be equivalent to namespace Foo def f ... := ... end Foo anymore.

[Leonardo de Moura]

Mario Carneiro said:

it would be easy enough to have synport produce def' instead of def whenever the name of the def contains a dot

This might work. We would also have theorem', correct?

[Mario Carneiro]

yes, and instance', example' etc. This also seems a bit unfortunate but workable

[Mario Carneiro]

To be clear, I'm not prescribing any particular option, and I hope we can find something that works the best for lean 4 users even if mathlib has to change. To my lean 3 colored perspective the fact that the name of a def only affects the name itself and not the body of the definition makes its own kind of sense, and I would present that point of view to anyone protesting about the lack of equivalence of def Foo.f and namespace Foo def f. But there seem to be no perfect options here.

[Floris van Doorn]

Leonardo de Moura said:

One option is to still use the name ae_measuable.min for the local declaration even after we perform the macro expansion on theorem ae_measurable.min.

I think this will solve 90+% of the cases in mathlib.
There will be still a couple of problematic cases, like src#con_gen, src#magma.free_semigroup, src#localization, but it's rare that a declaration foo uses a declaration foo.bar in it's definition/proof.
Another potential problem is that we are in a namespace foo and define bar, while _root_.bar also exists (and is used in foo.bar), but usually we protect declarations foo.bar like this, so then there should be no name clash.

[Mario Carneiro]

Is it possible for local declarations to have names with dots? AFAIR this is illegal in lean 3

[Leonardo de Moura]

@Mario Carneiro @Floris van Doorn What about a nonrec modifier for declarations? We already have partial. The macro lemma would expand to nonrec theorem. I think most of the examples that Floris linked are lemmas.
EDIT: missed

def free_semigroup (α : Type u) [has_mul α] : Type u :=
quot $ free_semigroup.r α

[Mario Carneiro]

ooh, that's nice too

[Floris van Doorn]

I would be happy with that.

[Mario Carneiro]

well, not sure about using lemma for this, I think the mathematicians have their own opinions about when to apply this label that probably don't correlate with nonrec

[Mario Carneiro]

but using nonrec lemma directly should be fine

[Floris van Doorn]

As I said, the declarations I linked in that message are rare. I just happened to make a list of declarations foo that used foo.bar in their definition, so I had some potential examples lying around.
I would be ok with requiring these defs to be replaced by nonrec def

EDIT: Oh wait, with the new suggestion we do run into the problems that in def foo.bar := the declaration bar is a recursive call. That might be more frequent.

[Sebastian Ullrich]

Leonardo de Moura said:

As in Lean 3, local declarations have precedence over global ones.

I just wanted to mention that we already have a special case in name resolution for recursive references: in x.f, f may be a recursive reference if its (the current) namespace is the type of x. And that makes sense of course (apart from being very convenient) given that users think of recursive references as global references, not local ones - as if f was already part of the environment. Then would it not be consistent to extend the special case to the reverse case as well - to interpret f.x as the global reference f.x, if it exists, in favor of a projection of the recursive reference (which I don't think I have ever seen used anyway)? IOW, I believe it would be consistent and convenient to prefer global to local references in the auxDecl special case.

[Sebastian Ullrich]

More generally we could have name resolution "pretend" that Current.Namespace.f is already in the environment, such that references such as _root_.Current.Namespace.f and Namespace.f work as well

[Sebastian Ullrich]

(This would not resolve the min case, no)

[Leonardo de Moura]

@Floris van Doorn What about combining @Sebastian Ullrich suggestion and having norec modifier (for examples like min). It should solve all cases, correct?

[Mario Carneiro]

I think this will work

[Floris van Doorn]

Yes, that sounds good to me. I think we still want the nonrec modifier a lot, for cases like ae_measurable.min, so I think we want it to be the default in mathlib for lemma and/or theorem(but as long as we can do that in mathlib by macros, I'd be happy)

[Daniel Selsam]

Floris van Doorn said:

Daniel Selsam thanks for your responses.

• About Singleton/Set.Singleton: Ah, that makes sense. I think having a coercion α → Set α is undesirable, so we should consider making Set.Monad a scoped instance.

BTW with https://github.com/leanprover/lean4/pull/643 your example gives the following error with default settings:

error: ambiguous, possible interpretations
  _root_.Subsingleton α

  Set.Subsingleton (pure α)

[Leonardo de Moura]

@Mario Carneiro @Floris van Doorn Pushed the changes. We can now write

def foo.aux := 1
def foo : Nat → Nat
  | n => foo.aux

and

def Foo (n : Nat) : Prop := True
def aux := 1
nonrec def Foo.aux : Foo aux :=
  have h : aux = 1 := rfl
  trivial

[Eric Wieser]

So does this mean that

nonrec def Foo.aux : Foo aux :=
  have h : aux = 1 := rfl
  trivial

is the preferred spelling, and we should prefer not to write the following?

def Foo.aux : Foo aux :=
  have h : _root_.aux = 1 := rfl
  trivial

[Reid Barton]

I don't think we really need a "preferred spelling" here