refactor(Mathport): move mathport prelude to mathlib4 (#80)

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.
```

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

.github/workflows/build.yml

@@ -25,7 +25,7 @@ jobs:
 
       - name: update Mathlib.lean
         run: |
-          find Mathlib -not -type d | sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
+          find Mathlib -name "*.lean" | sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Mathlib.lean
 
       - name: build mathlib
         run: lake build

Mathlib.lean

@@ -30,6 +30,10 @@ import Mathlib.Init.SetNotation
 import Mathlib.Lean.LocalContext
 import Mathlib.Logic.Basic
 import Mathlib.Logic.Function.Basic
+import Mathlib.Mathport.Attributes
+import Mathlib.Mathport.Rename
+import Mathlib.Mathport.SpecialNames
+import Mathlib.Mathport.Syntax
 import Mathlib.Tactic.Basic
 import Mathlib.Tactic.Cache
 import Mathlib.Tactic.Coe
@@ -41,6 +45,7 @@ import Mathlib.Tactic.NoMatch
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.OpenPrivate
 import Mathlib.Tactic.PrintPrefix
+import Mathlib.Tactic.Rcases
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunTac
 import Mathlib.Tactic.ShowTerm

Mathlib/Mathport/Attributes.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+import Lean.Attributes
+
+namespace Lean.Attr
+
+initialize reflAttr : TagAttribute ← registerTagAttribute `refl "reflexive relation"
+initialize symmAttr : TagAttribute ← registerTagAttribute `symm "symmetric relation"
+initialize transAttr : TagAttribute ← registerTagAttribute `trans "transitive relation"
+initialize substAttr : TagAttribute ← registerTagAttribute `subst "substitution"
+
+initialize linterAttr : TagAttribute ←
+  registerTagAttribute `linter "Use this declaration as a linting test in #lint"
+
+initialize hintTacticAttr : TagAttribute ←
+  registerTagAttribute `hintTactic "A tactic that should be tried by `hint`."

Mathlib/Mathport/README.md

@@ -0,0 +1,22 @@
+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.

Mathlib/Mathport/Rename.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import Lean
+
+namespace Mathlib.Prelude.Rename
+
+open Lean
+open System (FilePath)
+open Std (HashMap)
+
+abbrev RenameMap := HashMap Name Name
+
+def RenameMap.insertPair (m : RenameMap) : Name × Name → RenameMap
+  | (n3, n4) => m.insert n3 n4
+
+initialize renameExtension : SimplePersistentEnvExtension (Name × Name) RenameMap ←
+  registerSimplePersistentEnvExtension {
+    name          := `renameMapExtension
+    addEntryFn    := RenameMap.insertPair
+    addImportedFn := fun es => mkStateFromImportedEntries (RenameMap.insertPair) {} es
+  }
+
+def getRenameMap (env : Environment) : RenameMap := do
+  renameExtension.getState env
+
+def addNameAlignment (n3 n4 : Name) : CoreM Unit := do
+  modifyEnv fun env => renameExtension.addEntry env (n3, n4)
+
+open Lean.Elab Lean.Elab.Command
+
+syntax (name := align) "#align " ident ident : command
+
+@[commandElab align] def elabAlign : CommandElab
+  | `(#align%$tk $id3:ident $id4:ident) =>
+    liftCoreM $ addNameAlignment id3.getId id4.getId
+  | _ => throwUnsupportedSyntax
+
+syntax (name := lookup3) "#lookup3 " ident : command
+
+@[commandElab lookup3] def elabLookup3 : CommandElab
+  | `(#lookup3%$tk $id3:ident) => do
+    let n3 := id3.getId
+    match getRenameMap (← getEnv) |>.find? n3 with
+    | none    => logInfoAt tk s!"name `{n3} not found"
+    | some n4 => logInfoAt tk s!"{n4}"
+  | _ => throwUnsupportedSyntax
+
+end Mathlib.Prelude.Rename

Mathlib/Mathport/SpecialNames.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Selsam
+-/
+import Mathlib.Mathport.Rename
+
+namespace Mathlib.Prelude
+
+-- Note: we do not currently auto-align constants.
+#align quot Quot
+#align quot.mk Quot.mk
+#align quot.lift Quot.lift
+#align quot.ind Quot.ind
+
+-- Otherwise would be`OutParam` and `OptParam`!
+-- Note: we want `auto_param` to *not* align.
+#align out_param               outParam
+#align opt_param               optParam
+
+#align heq                     HEq
+
+#align punit                   PUnit
+#align pprod                   PProd
+
+#align has_coe Coe
+#align has_coe.coe Coe.coe
+
+#align has_coe_t CoeT
+#align has_coe_t.coe CoeT.coe
+
+#align has_coe_to_fun CoeFun
+#align has_coe_to_fun.coe CoeFun.coe
+
+#align has_coe_to_sort CoeSort
+#align has_coe_to_sort.coe CoeSort.coe
+
+#align has_le                  LE
+#align has_le.le               LE.le
+#align has_lt                  LT
+#align has_lt.lt               LT.lt
+
+#align has_beq                 BEq
+#align has_sizeof              SizeOf
+
+-- This otherwise causes filenames to clash
+#align category_theory.Kleisli CategoryTheory.KleisliCat
+
+-- TODO: backport?
+#align int.neg_succ_of_nat     Int.negSucc
+
+-- Generic 'has'-stripping
+-- Note: we don't currently strip automatically for various reasons.
+#align has_add       Add
+#align has_sub       Sub
+#align has_mul       Mul
+#align has_div       Div
+#align has_neg       Neg
+#align has_mod       Mod
+#align has_pow       Pow
+#align has_append    Append
+#align has_pure      Pure
+#align has_bind      Bind
+#align has_seq       Seq
+#align has_seq_left  SeqLeft
+#align has_seq_right SeqRight
+
+-- Implementation detail
+#align _sorry_placeholder_     _sorry_placeholder_
+
+
+
+end Mathlib.Prelude