[Merged by Bors] - refactor(Mathport): move mathport prelude to mathlib4

[semorrison]

Moving Mathport/Prelude/* out of mathport into mathlib4. I've added a README that will hopefully help bystanders:

Mathport prelude
===

This directory contains instructions for `mathport`,
helping it to translate `mathlib` and align declarations and tactics with `mathlib4`.
(These files were formerly part of `mathport`, in the directory `Mathport/Prelude/`.)

`SpecialNames.lean`
: Contains `#align X Y` statements, where `X` is an identifier from mathlib3
  which should be aligned with the identifier `Y` from mathlib4.
  Sometimes we need `#align` statements just to handle exceptions to casing rules,
  but there are also many exceptional cases.

`Syntax.lean`
: Contains unimplemented stubs of tactics which need to be migrated from Lean3 to Lean4.
  When porting tactics, you can move the relevant stubs to a new file and
  use them as a starting point.
  Please make sure this file stays in sync with new tactic implementations
  (and in particular that the syntax is not defined twice).
  Please preserve the syntax of existing mathlib tactics,
  so that there are no unnecessary parse errors in the source files generated by `synport`.
  It is fine to fail with an error message for unimplemented features for now.

[digama0]

Most of the commented out tactics are not actually a match, so the mathlib4 tactic needs to be adjusted to fit, or else we should delay replacing the tactic stub and importing the new tactic.

The other thing that should potentially cause build errors in mathport is if the mathlib4 tactic has a different name than these tactics. Most of the mathlib tactics are not named, but I think we should keep a standard naming convention (and placing them in the Lean.Tactic.foo namespace, as is done here) to make it easier to detect collisions between lean4 and mathlib4 tactics, or mathlib4 tactics and mathport tactic stubs.

[digama0]

Doesn't match:

syntax "ext" (colGt term:max)* : tactic

[semorrison]

I'm not too sure what to do with this one at this point. ext is going to require a rewrite to support rcases style patterns before we can use the

syntax (name := ext?) "ext?" (ppSpace rcasesPat)* (" : " num)? : tactic

version.

That will, I guess, happen. :-) But what do we do in the meantime? Or should we hold off doing this move, and instead prioritize redoing ported tactics that don't match closely enough to the mathlib3 versions?

[digama0]

We can just move the definition of rcasesPat to the file that defines rcases and/or ext. It doesn't need to be changed at all, it just gets consumed (or not) in the elaborator for rcases.

[gebner]

That's unfortunately not that easy because it would break the current uses of the ext tactic (ext (a, ⟨b, c⟩) works as expected).

[digama0]

With the rcasesPat syntax that can be written as ext ⟨a, ⟨b, c⟩⟩. We can work up to having terms there later, but I think it will be difficult to support all the abilities of rcasesPat using only the term parser.

[semorrison]

Okay. The existing implementation of ext in mathlib4 doesn't use rcasesPat, and will need to be rewritten at some point. For now, I've just left comments at both places noting that there's a discrepancy.

I did move rcasesPat to a file Mathlib.Tactic.Rcases, which Mathlib.Tactic.Ext now imports (but doesn't yet use).

[semorrison]

This syntax statement is redundant, if I understand correctly, as the elab will create it. Should it just be removed? Or is it better to keep it? (In which case, is it better to not use elab and instead write the def "long-hand"?)

[digama0]

If the elab will create the same syntax, then it should be fine to remove it. (In fact, I would be worried about getting two syntaxes if you don't remove it, like in librarySearch. I think you have to use elab_rules to ensure that a syntax is not created.) Can you still name the resulting syntax?

[gebner]

Yes, duplicate syntaxes are bad and should be removed. Is there a concrete reason you need to name the syntax? I've noticed that you've added a lot of (name := frob) arguments.

[digama0]

I would rather not have to refer to generated names in mathport, especially since they automatically change in response to collisions. I think we should put all tactics in the Lean.Tactic namespace and give them actual names, so that we have a reasonable chance of detecting collisions.

[gebner]

You shouldn't need to refer to any names in mathport, that's what `(tactic| rcases $...) is for.

[digama0]

Yes, of course I use that notation whenever I can, but unfortunately I quite often ran into the limitations of syntax quotation. Every single use of mkNode et al instead of `(foo) in mathport (probably around 50% of uses) is necessary, and probably a good starting point for finding future improvements of the notation.

[semorrison]

Okay --- I have removed the separate syntax statement, and changed the elab line to:

elab (name := showTerm) tk:"showTerm " t:tacticSeq : tactic => 

[digama0]

Suggested change

	elab_rules : tactic | `(normNum) => do
	elab_rules : tactic | `(tactic| normNum) => do

It is inferring the kind to ident, i.e. reading the syntax as a term normNum that doesn't exist and is maybe a local variable. @Kha Should the : tactic be used to influence the interpretation of syntax quotations in inferMacroRulesAltKind?

[Kha]

It probably should, but it would require nontrivial changes in the parser.

[semorrison]

Great, thanks @digama0 for the explanation to use tactic| in the pattern matches. I think this may be good to go now?

[gebner]

There's still quite a few duplicate clashing tactics left.

[gebner]

Suggested change

	syntax (name := squeezeScope) "squeezeScope " tacticSeq : tactic
	syntax (name := squeezeSimp) "squeezeSimp" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeSimp?) "squeezeSimp?" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeSimp!) "squeezeSimp!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeSimp?!) "squeezeSimp?!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeSimpa) "squeezeSimpa" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " term)? : tactic
	syntax (name := squeezeSimpa?) "squeezeSimpa?" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " term)? : tactic
	syntax (name := squeezeSimpa!) "squeezeSimpa!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " term)? : tactic
	syntax (name := squeezeSimpa?!) "squeezeSimpa?!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " term)? : tactic
	syntax (name := squeezeDSimp) "squeezeDSimp" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeDSimp?) "squeezeDSimp?" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeDSimp!) "squeezeDSimp!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := squeezeDSimp?!) "squeezeDSimp?!" (" (" &"config" " := " term ")")? (&" only")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (ppSpace location)? : tactic
	syntax (name := suggest) "suggest" (" (" &"config" " := " term ")")? (ppSpace num)?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " (colGt ident)+)? : tactic
	-- Moved to Mathlib.Tactic.LibrarySearch
	-- syntax (name := librarySearch) "librarySearch" (" (" &"config" " := " term ")")?
	-- (" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " (colGt ident)+)? : tactic
	syntax (name := librarySearch!) "librarySearch!" (" (" &"config" " := " term ")")?
	(" [" simpArg,* "]")? (" with " (colGt ident)+)? (" using " (colGt ident)+)? : tactic

These transient tactics are not (supposed to be!) used in mathlib and they will almost certainly look different in Lean 4, I really don't think we should spend time on porting their syntax 1-to-1.

We could also append 3 to all names, then the syntax doesn't matter and we can just remove the dangling syntax after the port.

But this is not a blocker, none of the syntaxes clash now.

[digama0]

I would prefer that the syntaxes continue to exist, although as you say they can be renamed if you want them to look different. But why wouldn't we want them to have a grammar like this? If someone is using librarySearch! they should be able to add all these config options and so on, I don't see a compelling reason not to have the tactic and a roughly equivalent syntax, not for porting but for lean 3 parity.

[gebner]

As discussed in the other comment, the functionality should certainly be available in Lean 4 but there's no point in spending any effort on porting them since they don't occur in mathlib.

Since you've mentioned the bang-version of librarySearch. The bang-less version (doing only reducible matching) is an optimization we had to do in Lean 3 because semireducible matching was too slow. We can hopefully eliminate this variant entirely in Lean 4 using better indexing.

[gebner]

Can we just translate the Lean 3 library_search to librarySearch3 instead so that we don't have to match the syntax?

[digama0]

Is there a reason that by librarySearch [args] shouldn't work in lean 4? I understand that it's not done yet but I want all the lean 3 tactics to have equivalents in lean 4.

[gebner]

No that should still work, as well as the using argument that is also on the todo list. The configuration object is almost certainly going to change (the lean 3 one refers to the built-in apply tactic). We might also want to replace solve-by-elim with Jannis' auto port as discussed on Monday, affecting the with syntax.

Most importantly though, aligning these tactics is completely unnecessary.

[gebner]

Duplicate.

[digama0]

Not a match, and that one's in core so it is more problematic to override. Probably this one needs to be renamed to byCases'

[semorrison]

Renamed, and added a comment explaining the difference.

[semorrison]

Could we just punt for now on the transient tactics? I don't think having the syntax statements here for them causes any problem, and we can delete them / modify them / whatever in later PRs. I'd prefer to get this PR out of the way so we can finish off providing CI and a downloadable artifact for mathport!

[gebner]

Could we just punt for now on the transient tactics? I don't think having the syntax statements here for them causes any problem, and we can delete them / modify them / whatever in later PRs.

I completely agree with you, that's why I said earlier:

But this is not a blocker, none of the syntaxes clash now.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build