Add support for Lean 4

.gitmodules

@@ -1257,6 +1257,9 @@
 [submodule "vendor/grammars/vscode-lean"]
 	path = vendor/grammars/vscode-lean
 	url = https://github.com/leanprover/vscode-lean
+[submodule "vendor/grammars/vscode-lean4"]
+	path = vendor/grammars/vscode-lean4
+	url = https://github.com/leanprover/vscode-lean4.git
 [submodule "vendor/grammars/vscode-monkey-c"]
 	path = vendor/grammars/vscode-monkey-c
 	url = https://github.com/ghisguth/vscode-monkey-c

grammars.yml

@@ -1131,6 +1131,10 @@ vendor/grammars/vscode-lean:
 - markdown.lean.codeblock
 - source.lean
 - source.lean.markdown
+vendor/grammars/vscode-lean4:
+- markdown.lean4.codeblock
+- source.lean4
+- source.lean4.markdown
 vendor/grammars/vscode-monkey-c:
 - source.mc
 vendor/grammars/vscode-motoko:

lib/linguist/heuristics.yml

@@ -388,6 +388,12 @@ disambiguations:
     pattern: '^\.[A-Za-z]{2}(\s|$)'
   - language: PicoLisp
     pattern: '^\((de|class|rel|code|data|must)\s'
+- extensions: ['.lean']
+  rules:
+  - language: Lean
+    pattern: '^import [a-z]'
+  - language: Lean 4
+    pattern: '^import [A-Z]'
 - extensions: ['.ls']
   rules:
   - language: LoomScript

lib/linguist/languages.yml

@@ -3709,6 +3709,14 @@ Lean:
   tm_scope: source.lean
   ace_mode: text
   language_id: 197
+Lean 4:
+  type: programming
+  group: Lean
+  extensions:
+  - ".lean"
+  tm_scope: source.lean4
+  ace_mode: text
+  language_id: 455147478
 Less:
   type: markup
   color: "#1d365d"

samples/Lean 4/BirthdayProblem.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2021 Eric Rodriguez. All rights reserved.
+Released under Apache 2.0 license as described in the leanprover-community/mathlib4 repo.
+Authors: Eric Rodriguez
+-/
+import Mathlib.Data.Fintype.CardEmbedding
+import Mathlib.Probability.CondCount
+import Mathlib.Probability.Notation
+
+#align_import wiedijk_100_theorems.birthday_problem from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"
+
+/-!
+# Birthday Problem
+
+This file proves Theorem 93 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
+
+As opposed to the standard probabilistic statement, we instead state the birthday problem
+in terms of injective functions. The general result about `Fintype.card (α ↪ β)` which this proof
+uses is `Fintype.card_embedding_eq`.
+-/
+
+
+namespace Theorems100
+
+local notation "|" x "|" => Finset.card x
+
+local notation "‖" x "‖" => Fintype.card x
+
+/-- **Birthday Problem**: set cardinality interpretation. -/
+theorem birthday :
+    2 * ‖Fin 23 ↪ Fin 365‖ < ‖Fin 23 → Fin 365‖ ∧ 2 * ‖Fin 22 ↪ Fin 365‖ > ‖Fin 22 → Fin 365‖ := by
+  -- This used to be
+  -- `simp only [Nat.descFactorial, Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun]`
+  -- but after leanprover/lean4#2790 that triggers a max recursion depth exception.
+  -- As a workaround, we make some of the reduction steps more explicit.
+  rw [Fintype.card_embedding_eq, Fintype.card_fun, Fintype.card_fin, Fintype.card_fin]
+  rw [Fintype.card_embedding_eq, Fintype.card_fun, Fintype.card_fin, Fintype.card_fin]
+  decide
+#align theorems_100.birthday Theorems100.birthday
+
+section MeasureTheory
+
+open MeasureTheory ProbabilityTheory
+
+open scoped ProbabilityTheory ENNReal
+
+variable {n m : ℕ}
+
+/- In order for Lean to understand that we can take probabilities in `Fin 23 → Fin 365`, we must
+tell Lean that there is a `MeasurableSpace` structure on the space. Note that this instance
+is only for `Fin m` - Lean automatically figures out that the function space `Fin n → Fin m`
+is _also_ measurable, by using `MeasurableSpace.pi`, and furthermore that all sets are measurable,
+from `MeasurableSingletonClass.pi`. -/
+instance : MeasurableSpace (Fin m) :=
+  ⊤
+
+instance : MeasurableSingletonClass (Fin m) :=
+  ⟨fun _ => trivial⟩
+
+/- We then endow the space with a canonical measure, which is called ℙ.
+We define this to be the conditional counting measure. -/
+noncomputable instance : MeasureSpace (Fin n → Fin m) :=
+  ⟨condCount Set.univ⟩
+
+-- The canonical measure on `Fin n → Fin m` is a probability measure (except on an empty space).
+instance : IsProbabilityMeasure (ℙ : Measure (Fin n → Fin (m + 1))) :=
+  condCount_isProbabilityMeasure Set.finite_univ Set.univ_nonempty
+
+theorem FinFin.measure_apply {s : Set <| Fin n → Fin m} :
+    ℙ s = |s.toFinite.toFinset| / ‖Fin n → Fin m‖ := by
+  erw [condCount_univ, Measure.count_apply_finite]
+#align theorems_100.fin_fin.measure_apply Theorems100.FinFin.measure_apply
+
+/-- **Birthday Problem**: first probabilistic interpretation. -/
+theorem birthday_measure :
+    ℙ ({f | (Function.Injective f)} : Set ((Fin 23) → (Fin 365))) < 1 / 2 := by
+  rw [FinFin.measure_apply]
+  generalize_proofs hfin
+  have : |hfin.toFinset| = 42200819302092359872395663074908957253749760700776448000000 := by
+    trans ‖Fin 23 ↪ Fin 365‖
+    · rw [← Fintype.card_coe]
+      apply Fintype.card_congr
+      rw [Set.Finite.coeSort_toFinset, Set.coe_setOf]
+      exact Equiv.subtypeInjectiveEquivEmbedding _ _
+    · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
+      rfl
+  rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
+  rotate_left; (iterate 2 right; norm_num); decide; (iterate 2 left; norm_num)
+  simp only [Fintype.card_pi]
+  norm_num
+#align theorems_100.birthday_measure Theorems100.birthday_measure
+
+end MeasureTheory
+
+end Theorems100

test/test_heuristics.rb

@@ -582,6 +582,13 @@ def test_l_by_heuristics
     })
   end
 
+  def test_lean_by_heuristics
+    assert_heuristics({
+      "Lean" => all_fixtures("Lean", "*.lean"),
+      "Lean 4" => all_fixtures("Lean 4", "*.lean")
+    })
+  end
+
   def test_lisp_by_heuristics
     assert_heuristics({
       "Common Lisp" => all_fixtures("Common Lisp", "*.lisp") + all_fixtures("Common Lisp", "*.lsp"),

vendor/README.md

@@ -302,6 +302,7 @@ This is a list of grammars that Linguist selects to provide syntax highlighting
 - **Lasso:** [bfad/Sublime-Lasso](https://github.com/bfad/Sublime-Lasso)
 - **Latte:** [textmate/php-smarty.tmbundle](https://github.com/textmate/php-smarty.tmbundle)
 - **Lean:** [leanprover/vscode-lean](https://github.com/leanprover/vscode-lean)
+- **Lean 4:** [leanprover/vscode-lean4](https://github.com/leanprover/vscode-lean4)
 - **Less:** [atom/language-less](https://github.com/atom/language-less)
 - **Lex:** [Alhadis/language-grammars](https://github.com/Alhadis/language-grammars)
 - **LigoLANG:** [pewulfman/Ligo-grammar](https://github.com/pewulfman/Ligo-grammar)