Update Lean.sublime-syntax from Lean 3 to Lean 4

Resolves #3286

1. `lean4.json` → `lean4.tmLanguage`

    1. Download `vscode-lean4/syntaxes/lean4.json` from https://github.com/leanprover/vscode-lean4/pull/623 (now merged).
    2. Install the VS Code extension [TextMate Languages (pedro-w)](https://marketplace.visualstudio.com/items?itemName=pedro-w.tmlanguage).
    3. Open `lean4.json` in VS Code, <kbd>F1</kbd>, and “Convert to tmLanguage PLIST File”.

2. `lean4.tmLanguage` → `lean4.sublime-syntax`

    Open `lean4.tmLanguage` in Sublime text, “Tools → Developer → New Syntax from lean4.tmLanguage…”.

.gitmodules

@@ -196,7 +196,7 @@
 	branch = bat-source
 [submodule "assets/syntaxes/02_Extra/Lean"]
 	path = assets/syntaxes/02_Extra/Lean
-	url = https://github.com/leanprover/vscode-lean.git
+	url = https://github.com/leanprover/vscode-lean4.git
 [submodule "assets/syntaxes/02_Extra/Zig"]
 	path = assets/syntaxes/02_Extra/Zig
 	url = https://github.com/ziglang/sublime-zig-language.git

assets/syntaxes/02_Extra/Lean.sublime-syntax

@@ -1,125 +1,130 @@
 %YAML 1.2
 ---
-# http://www.sublimetext.com/docs/3/syntax.html
-name: Lean
+# http://www.sublimetext.com/docs/syntax.html
+name: Lean 4
 file_extensions:
   - lean
-scope: source.lean
+scope: source.lean4
 contexts:
   main:
     - include: comments
-    - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|axioms|abbreviation|lemma|definition|def|instance|class|constant)\b\s+(\{[^}]*\})?'
+    - match: \b(Prop|Type|Sort)\b
+      scope: storage.type.lean4
+    - match: '\battribute\b\s*\[[^\]]*\]'
+      scope: storage.modifier.lean4
+    - match: '@\[[^\]]*\]'
+      scope: storage.modifier.lean4
+    - match: \b(?<!\.)(global|local|scoped|partial|unsafe|private|protected|noncomputable)(?!\.)\b
+      scope: storage.modifier.lean4
+    - match: \b(sorry|admit|stop)\b
+      scope: invalid.illegal.lean4
+    - match: '#(print|eval|reduce|check|check_failure)\b'
+      scope: keyword.other.lean4
+    - match: \bderiving\s+instance\b
+      scope: keyword.other.command.lean4
+    - match: '\b(?<!\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class|constant)\b\s+(\{[^}]*\})?'
       captures:
-        1: keyword.other.definitioncommand.lean
+        1: keyword.other.definitioncommand.lean4
       push:
-        - meta_scope: meta.definitioncommand.lean
-        - match: '(?=\bwith\b|\bextends\b|[:\|\(\[\{⦃<>])'
+        - meta_scope: meta.definitioncommand.lean4
+        - match: '(?=\bwith\b|\bextends\b|\bwhere\b|[:\|\(\[\{⦃<>])'
           pop: true
         - include: comments
         - include: definitionName
-        - match: ","
-    - match: \b(Prop|Type|Sort)\b
-      scope: storage.type.lean
-    - match: '\battribute\b\s*\[[^\]]*\]'
-      scope: storage.modifier.lean
-    - match: '@\[[^\]]*\]'
-      scope: storage.modifier.lean
-    - match: \b(?<!\.)(private|meta|mutual|protected|noncomputable)\b
-      scope: keyword.control.definition.modifier.lean
-    - match: \b(sorry)\b
-      scope: invalid.illegal.lean
-    - match: '#print\s+(def|definition|inductive|instance|structure|axiom|axioms|class)\b'
-      scope: keyword.other.command.lean
-    - match: '#(print|eval|reduce|check|help|exit|find|where)\b'
-      scope: keyword.other.command.lean
-    - match: \b(?<!\.)(import|export|prelude|theory|definition|def|abbreviation|instance|renaming|hiding|exposing|parameter|parameters|begin|constant|constants|lemma|variable|variables|theorem|example|open|axiom|inductive|coinductive|with|structure|universe|universes|alias|precedence|reserve|postfix|prefix|infix|infixl|infixr|notation|end|using|namespace|section|local|set_option|extends|include|omit|class|classes|instances|raw|run_cmd|restate_axiom)(?!\.)\b
-      scope: keyword.other.lean
-    - match: \b(?<!\.)(calc|have|this|match|do|suffices|show|by|in|at|let|forall|fun|exists|assume|from|obtain|haveI|λ)(?!\.)\b
-      scope: keyword.other.lean
+        - match: ','
+    - match: \b(?<!\.)(theorem|show|have|from|suffices|nomatch|def|class|structure|instance|set_option|initialize|builtin_initialize|example|inductive|coinductive|axiom|constant|universe|universes|variable|variables|import|open|export|theory|prelude|renaming|hiding|exposing|do|by|let|extends|mutual|mut|where|rec|syntax|macro_rules|macro|deriving|fun|section|namespace|end|infix|infixl|infixr|postfix|prefix|notation|abbrev|if|then|else|calc|match|with|for|in|unless|try|catch|finally|return|continue|break)(?!\.)\b
+      scope: keyword.other.lean4
     - match: «
       push:
-        - meta_content_scope: entity.name.lean
+        - meta_content_scope: entity.name.lean4
         - match: »
           pop: true
-    - match: \b(?<!\.)(if|then|else)\b
-      scope: keyword.control.lean
-    - match: '"'
+    - match: (s!)"
       captures:
-        0: punctuation.definition.string.begin.lean
+        1: keyword.other.lean4
       push:
-        - meta_scope: string.quoted.double.lean
+        - meta_scope: string.interpolated.lean4
         - match: '"'
-          captures:
-            0: punctuation.definition.string.end.lean
           pop: true
-        - match: '\\[\\"nt'']'
-          scope: constant.character.escape.lean
+        - match: '(\{)'
+          captures:
+            1: keyword.other.lean4
+          push:
+            - match: '(\})'
+              captures:
+                1: keyword.other.lean4
+              pop: true
+            - include: main
+        - match: '\\[\\"ntr'']'
+          scope: constant.character.escape.lean4
         - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
-          scope: constant.character.escape.lean
+          scope: constant.character.escape.lean4
         - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
-          scope: constant.character.escape.lean
+          scope: constant.character.escape.lean4
+    - match: '"'
+      push:
+        - meta_scope: string.quoted.double.lean4
+        - match: '"'
+          pop: true
+        - match: '\\[\\"ntr'']'
+          scope: constant.character.escape.lean4
+        - match: '\\x[0-9A-Fa-f][0-9A-Fa-f]'
+          scope: constant.character.escape.lean4
+        - match: '\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]'
+          scope: constant.character.escape.lean4
+    - match: \b(true|false)\b
+      scope: constant.language.lean4
     - match: '''[^\\'']'''
-      scope: string.quoted.single.lean
-    - match: '''(\\(x..|u....|.))'''
-      scope: string.quoted.single.lean
+      scope: string.quoted.single.lean4
+    - match: '''(\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'''
+      scope: string.quoted.single.lean4
       captures:
-        1: constant.character.escape.lean
+        1: constant.character.escape.lean4
     - match: '`+[^\[(]\S+'
-      scope: entity.name.lean
-    - match: '\b([0-9]+|0([xX][0-9a-fA-F]+))\b'
-      scope: constant.numeric.lean
+      scope: entity.name.lean4
+    - match: '\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?)\b'
+      scope: constant.numeric.lean4
   blockComment:
     - match: /-
       push:
-        - meta_scope: comment.block.lean
-        - match: "-/"
+        - meta_scope: comment.block.lean4
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
         - include: blockComment
   comments:
     - include: dashComment
     - include: docComment
-    - include: stringBlock
     - include: modDocComment
     - include: blockComment
   dashComment:
-    - match: (--)
-      captures:
-        0: punctuation.definition.comment.lean
+    - match: '--'
       push:
-        - meta_scope: comment.line.double-dash.lean
+        - meta_scope: comment.line.double-dash.lean4
         - match: $
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
   definitionName:
     - match: '\b[^:«»\(\)\{\}[:space:]=→λ∀?][^:«»\(\)\{\}[:space:]]*'
-      scope: entity.name.function.lean
+      scope: entity.name.function.lean4
     - match: «
       push:
-        - meta_content_scope: entity.name.function.lean
+        - meta_content_scope: entity.name.function.lean4
         - match: »
           pop: true
   docComment:
     - match: /--
       push:
-        - meta_scope: comment.block.documentation.lean
-        - match: "-/"
+        - meta_scope: comment.block.documentation.lean4
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
         - include: blockComment
   modDocComment:
     - match: /-!
       push:
-        - meta_scope: comment.block.documentation.lean
-        - match: "-/"
+        - meta_scope: comment.block.documentation.lean4
+        - match: '-/'
           pop: true
-        - include: scope:source.lean.markdown
-        - include: blockComment
-  stringBlock:
-    - match: /-"
-      push:
-        - meta_scope: comment.block.string.lean
-        - match: '"-/'
-          pop: true
-        - include: scope:source.lean.markdown
+        - include: scope:source.lean4.markdown
         - include: blockComment

doc/assets.md

@@ -102,4 +102,4 @@ The following files have been manually modified after converting from a `.tmLang
    https://github.com/seanjames777/SML-Language-Definition/blob/master/sml.tmLanguage
 * `Cabal.sublime_syntax` has been added manually from
   https://github.com/SublimeHaskell/SublimeHaskell/ - we don't want to include the whole submodule because it includes other syntaxes ("Haskell improved") as well.
-* `Lean.sublime-syntax` has been added manually from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json via conversion.
+* `Lean.sublime-syntax` has been added manually from https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json via conversion.

tests/syntax-tests/highlighted/Lean/test.lean

@@ -1,67 +1,82 @@
-import data.matrix.notation
-import data.vector2
+import MIL.Common
+import Mathlib.Topology.Instances.Real.Defs
 
-/-!
+open Set Filter Topology
 
-Helpers that don't currently fit elsewhere...
+variable {α : Type*}
+variable (s t : Set ℕ)
+variable (ssubt : s ⊆ t)
+variable {α : Type*} (s : Set (Set α))
+-- Apostrophes are allowed in variable names
+variable (f'_x x' : ℕ)
+variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)
 
--/
+-- In the next example we could use `tauto` in each proof instead of knowing the lemmas
+example {α : Type*} (s : Set α) : Filter α :=
+  { sets := { t | s ⊆ t }
+    univ_sets := subset_univ s
+    sets_of_superset := fun hU hUV ↦ Subset.trans hU hUV
+    inter_sets := fun hU hV ↦ subset_inter hU hV }
 
-lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
-  p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
-
--- For `playfield`s, the piece type and/or piece index type.
-variables (X : Type*)
-variables [has_repr X]
 
 namespace chess.utils
 
 section repr
 
-/--
-An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
-for `option`, and rather, output just the value in the `some` and a custom provided
-`string` for `none`.
--/
-structure option_wrapper :=
-(val : option X)
-(none_s : string)
+@[class] structure One₂ (α : Type) where
+  /-- The element one -/
+  one : α
 
-instance wrapped_option_repr : has_repr (option_wrapper X) :=
-⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
+structure StandardTwoSimplex where
+  x : ℝ
+  y : ℝ
+  z : ℝ
+  x_nonneg : 0 ≤ x
+  y_nonneg : 0 ≤ y
+  z_nonneg : 0 ≤ z
+  sum_eq : x + y + z = 1
 
-variables {X}
-/--
-Construct an `option_wrapper` term from a provided `option X` and the `string`
-that will override the `has_repr.repr` for `none`.
--/
-def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
+#check Pi.ringHom
+#check ker_Pi_Quotient_mk
+#eval 1 + 1
 
--- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
-variables {m' n' : ℕ}
+/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
+  Remainder Theorem. -/
+def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
+  Ideal.Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Ideal.Quotient.mk (I i))
+    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])
 
-/--
-For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
-the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
-This definition is used for displaying rows of the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
-λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
+lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
+    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
+  rfl
 
-instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
+theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
+    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
+  classical
+  simp_rw [isCoprime_iff_add] at *
+  induction s using Finset.induction with
+  | empty =>
+      simp
+  | @insert i s _ hs =>
+      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
+      set K := ⨅ j ∈ s, J j
+      calc
+        1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
+        _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
+        _ = (1 + K) * I + K * J i  := by ring
+        _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
 
-/--
-For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
-we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
-This definition is used for displaying the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
-λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
 
-instance matrix_repr_instance :
-  has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
+class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
+  /-- Multiplication is left distributive over addition -/
+  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
+  /-- Multiplication is right distributive over addition -/
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
+{ Ring₃.toAddGroup₃ with
+  add_comm := by
+    sorry }
 
 end repr
 

tests/syntax-tests/source/Lean/test.lean

@@ -1,67 +1,82 @@
-import data.matrix.notation
-import data.vector2
+import MIL.Common
+import Mathlib.Topology.Instances.Real.Defs
 
-/-!
+open Set Filter Topology
 
-Helpers that don't currently fit elsewhere...
+variable {α : Type*}
+variable (s t : Set ℕ)
+variable (ssubt : s ⊆ t)
+variable {α : Type*} (s : Set (Set α))
+-- Apostrophes are allowed in variable names
+variable (f'_x x' : ℕ)
+variable (bangwI' jablu'DI' QaQqu' nay' Ghay'cha' he' : ℕ)
 
--/
+-- In the next example we could use `tauto` in each proof instead of knowing the lemmas
+example {α : Type*} (s : Set α) : Filter α :=
+  { sets := { t | s ⊆ t }
+    univ_sets := subset_univ s
+    sets_of_superset := fun hU hUV ↦ Subset.trans hU hUV
+    inter_sets := fun hU hV ↦ subset_inter hU hV }
 
-lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
-  p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
-
--- For `playfield`s, the piece type and/or piece index type.
-variables (X : Type*)
-variables [has_repr X]
 
 namespace chess.utils
 
 section repr
 
-/--
-An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
-for `option`, and rather, output just the value in the `some` and a custom provided
-`string` for `none`.
--/
-structure option_wrapper :=
-(val : option X)
-(none_s : string)
+@[class] structure One₂ (α : Type) where
+  /-- The element one -/
+  one : α
 
-instance wrapped_option_repr : has_repr (option_wrapper X) :=
-⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
+structure StandardTwoSimplex where
+  x : ℝ
+  y : ℝ
+  z : ℝ
+  x_nonneg : 0 ≤ x
+  y_nonneg : 0 ≤ y
+  z_nonneg : 0 ≤ z
+  sum_eq : x + y + z = 1
 
-variables {X}
-/--
-Construct an `option_wrapper` term from a provided `option X` and the `string`
-that will override the `has_repr.repr` for `none`.
--/
-def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
+#check Pi.ringHom
+#check ker_Pi_Quotient_mk
+#eval 1 + 1
 
--- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
-variables {m' n' : ℕ}
+/-- The homomorphism from ``R ⧸ ⨅ i, I i`` to ``Π i, R ⧸ I i`` featured in the Chinese
+  Remainder Theorem. -/
+def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
+  Ideal.Quotient.lift (⨅ i, I i) (Pi.ringHom fun i : ι ↦ Ideal.Quotient.mk (I i))
+    (by simp [← RingHom.mem_ker, ker_Pi_Quotient_mk])
 
-/--
-For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
-the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
-This definition is used for displaying rows of the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
-λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
+lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
+    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
+  rfl
 
-instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
+theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
+    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
+  classical
+  simp_rw [isCoprime_iff_add] at *
+  induction s using Finset.induction with
+  | empty =>
+      simp
+  | @insert i s _ hs =>
+      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
+      set K := ⨅ j ∈ s, J j
+      calc
+        1 = I + K                  := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
+        _ = I + K * (I + J i)      := by rw [hf i (Finset.mem_insert_self i s), mul_one]
+        _ = (1 + K) * I + K * J i  := by ring
+        _ ≤ I + K ⊓ J i            := by gcongr ; apply mul_le_left ; apply mul_le_inf
 
-/--
-For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
-we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
-This definition is used for displaying the playfield, when it is defined
-via a `matrix`, likely through notation.
--/
-def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
-λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
 
-instance matrix_repr_instance :
-  has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
+class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
+  /-- Multiplication is left distributive over addition -/
+  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
+  /-- Multiplication is right distributive over addition -/
+  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
+
+instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
+{ Ring₃.toAddGroup₃ with
+  add_comm := by
+    sorry }
 
 end repr