Making backwards-incompatible changes to Lean

Stream: general

[Gabriel Ebner]

(I'm positing this here for higher visibility because I get the feeling that not everybody is watching the community fork repository.) We've been talking about it for a long time and I believe we should finally start making some long-due backwards-incompatible changes to Lean. These are the concrete changes that I'd like to merge soon:

• Remove the simp attribute from add_comm (@Edward Ayers made a PR: https://github.com/leanprover-community/lean/pull/65)
• Remove the simp attribute from sub_eq_add_neg (@Mario Carneiro aspires to be a pyromaniac: https://github.com/leanprover-community/mathlib/pull/2017#issuecomment-588417505)
• Replace the insert definition with export has_insert (insert) (my proposal: https://github.com/leanprover-community/lean/pull/115)

Any thoughts?

[Patrick Massot]

Can I vote twice for removing the simp attribute on subeq_add_neg?

[Patrick Massot]

I guess most thing that simplify using add_comm and add_assoc should be using ring or abel anyway. So I vote yes to all those changes.

[Rob Lewis]

I'm on board, it's time to fix the things we've spent years complaining about.

[Gabriel Ebner]

PR for sub_eq_add_neg: https://github.com/leanprover-community/lean/pull/117

[Sebastien Gouezel]

How does this interact with updating mathlib? I mean, when we do such a change to Lean, then mathlib will break, and we will need to fix it. But once it is fixed, it will become incompatible with previous versions of Lean. So, things should be coordinated in a way.

[Rob Lewis]

mathlib specifies which Lean version it uses in the toml file. Right now it's 3.5.1.

[Rob Lewis]

It won't know about any changes to Lean until we update the toml.

[Rob Lewis]

The PR that makes that change should also fix any breakage.

[Rob Lewis]

It's probably a good idea to keep a branch of mathlib updated to Lean nightlies, so we don't have to make these fixes all at once.

[Gabriel Ebner]

I vaguely recall that somebody complained about ∘ being reducible. Do we want to change this as well?
(Occasion: I'm currently debugging a simp loop with [simplify.rewrite] [equiv.conj_comp]: ⇑(equiv.conj e) f ==> ⇑(equiv.conj e) f ∘ ⇑(equiv.conj e) (λ (x : α), x))

[Anne Baanen]

Could we also fix the built-in well-foundedness tactic so that we can get rid of using_well_founded wf_tacs?

[Gabriel Ebner]

@Anne Baanen Of course. Please submit a PR to our glorious fork!

[Yury G. Kudryashov]

What about changing {a, b} from insert b {a} to insert a {b}?

[Floris van Doorn]

Rob Lewis said:

It's probably a good idea to keep a branch of mathlib updated to Lean nightlies, so we don't have to make these fixes all at once.

I think we don't want to keep two versions of mathlib up to date. That will result in a headache of merge conflicts, especially if some of these "Lean-compatibility" changes touch 100+ files.

I think we should bump the Lean version frequently for mathlib.

[Yury G. Kudryashov]

If someone will rewrite notation for {a, b, ...}, then I'm ready to fix compile failures.

[Mario Carneiro]

@Gabriel Ebner Yes please re: making comp semireducible

[Mario Carneiro]

This will finally allow us to have not completely useless typeclass inference for things like unbundled group/ring homs and continuous functions

[Mario Carneiro]

Comp should only reduce when it is applied to an argument

[Gabriel Ebner]

@Chris Hughes removes discrete fields: https://github.com/leanprover-community/lean/pull/119

[Bryan Gin-ge Chen]

Which "primed" tactics should be moved to Lean core?

[Mario Carneiro]

All of them, I think

[Gabriel Ebner]

Yes please re: making comp semireducible

Does anybody want to make a PR for this?

[Gabriel Ebner]

I think we should bump the Lean version frequently for mathlib.

I agree. I don't want to let the two diverge too much either. In fact, I would like to make a 3.6 release next week. I'm happy to do a 3.7 release shortly after if there's still changes left.

[Gabriel Ebner]

@Anne Baanen adds the mathlib fixes to the well-foundedness tactics: https://github.com/leanprover-community/lean/pull/121

[Patrick Massot]

Since we seem to be frantically modifying the community fork, should we try to merge leanpkg and our mathlib tools? Users are very confused by the number of tools. For instance creating a new project depending on mathlib needs a crazy number of commands.

[Gabriel Ebner]

Commands that are in Lean proper also need to be supported by elan.

[Patrick Massot]

elan is one of the commands that need to be merged.

[Patrick Massot]

For instance, how many commands are there for Rust users? Isn't all cargo action arguments?

[Patrick Massot]

oh no, there is also rustup.

[Patrick Massot]

I'm sure we can do better.

[Chris Hughes]

What do we want to do with discrete_linear_ordered_field and the like. The decidability in these structures is used to define abs, max etc? I wouldn't mind the definition of max and abs being part of the structure instead of decidability.

[Mario Carneiro]

I think we should just rename them to decidable_linear_ordered_field for consistency with the others

[Mario Carneiro]

I think there is a decent argument for having division_ring and field inherit from decidable_eq since you need equality with zero to prove anything, and in every relevant case either the structure is actually decidable (like rat) or we are in mathematician mode and everything is (like real)

[Patrick Massot]

Those decidable assumption still caused a huge messed with linear algebra and polynomials.

[Bryan Gin-ge Chen]

I made a list of primed tactics here. There are some where I'm not sure whether the primed version should replace the original version, so if anyone wants to take a look, it'd be greatly appreciated.

[Bryan Gin-ge Chen]

Another question: would it be possible to fix the issue that prevents certain commands from being used immediately after the imports?

[Mario Carneiro]

It's a parsing problem. It's impossible to distinguish import file newly_declared_notation from an import of file and also the file newly_declared_notation, or an import of file followed by a user command called newly_declared_notation

[Mario Carneiro]

I think it would be best if import permitted a trailing dot to end the command, like you can do with def and theorem