Add support for Lean 4

.gitmodules

@@ -1245,6 +1245,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

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

lib/linguist/heuristics.yml

@@ -393,6 +393,12 @@ disambiguations:
   - language: LoomScript
     pattern: '^\s*package\s*[\w\.\/\*\s]*\s*\{'
   - language: LiveScript
+- extensions: ['.lean']
+  rules:
+  - language: Lean
+    pattern: '^import [a-z]'
+  - language: Lean 4
+    pattern: '^import [A-Z]'
 - extensions: ['.lsp', '.lisp']
   rules:
   - language: Common Lisp

lib/linguist/languages.yml

@@ -3690,6 +3690,13 @@ Lean:
   tm_scope: source.lean
   ace_mode: text
   language_id: 197
+Lean 4:
+  type: programming
+  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

samples/Lean 4/Conv.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2021 Gabriel Ebner. All rights reserved.
+Released under Apache 2.0 license as described in the leanprover-community/mathlib4 repo.
+Authors: Gabriel Ebner
+-/
+import Mathlib.Tactic.RunCmd
+import Lean.Elab.Tactic.Conv.Basic
+import Std.Lean.Parser
+
+/-!
+Additional `conv` tactics.
+-/
+
+namespace Mathlib.Tactic.Conv
+open Lean Parser.Tactic Parser.Tactic.Conv Elab.Tactic Meta
+
+syntax (name := convLHS) "conv_lhs" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
+macro_rules
+  | `(tactic| conv_lhs $[at $id]? $[in $[$occs]? $pat]? => $seq) =>
+    `(tactic| conv $[at $id]? $[in $[$occs]? $pat]? => lhs; ($seq:convSeq))
+
+syntax (name := convRHS) "conv_rhs" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
+macro_rules
+  | `(tactic| conv_rhs $[at $id]? $[in $[$occs]? $pat]? => $seq) =>
+    `(tactic| conv $[at $id]? $[in $[$occs]? $pat]? => rhs; ($seq:convSeq))
+
+macro "run_conv" e:doSeq : conv => `(conv| tactic' => run_tac $e)
+
+/--
+`conv in pat => cs` runs the `conv` tactic sequence `cs`
+on the first subexpression matching the pattern `pat` in the target.
+The converted expression becomes the new target subgoal, like `conv => cs`.
+
+The arguments `in` are the same as those as the in `pattern`.
+In fact, `conv in pat => cs` is a macro for `conv => pattern pat; cs`.
+
+The syntax also supports the `occs` clause. Example:
+```lean
+conv in (occs := *) x + y => rw [add_comm]
+```
+-/
+macro "conv" " in " occs?:(occs)? p:term " => " code:convSeq : conv =>
+  `(conv| conv => pattern $[$occs?]? $p; ($code:convSeq))
+
+/--
+* `discharge => tac` is a conv tactic which rewrites target `p` to `True` if `tac` is a tactic
+  which proves the goal `⊢ p`.
+* `discharge` without argument returns `⊢ p` as a subgoal.
+-/
+syntax (name := dischargeConv) "discharge" (" => " tacticSeq)? : conv
+
+/-- Elaborator for the `discharge` tactic. -/
+@[tactic dischargeConv] def elabDischargeConv : Tactic := fun
+  | `(conv| discharge $[=> $tac]?) => do
+    let g :: gs ← getGoals | throwNoGoalsToBeSolved
+    let (theLhs, theRhs) ← Conv.getLhsRhsCore g
+    let .true ← isProp theLhs | throwError "target is not a proposition"
+    theRhs.mvarId!.assign (mkConst ``True)
+    let m ← mkFreshExprMVar theLhs
+    g.assign (← mkEqTrue m)
+    if let some tac := tac then
+      setGoals [m.mvarId!]
+      evalTactic tac; done
+      setGoals gs
+    else
+      setGoals (m.mvarId! :: gs)
+  | _ => Elab.throwUnsupportedSyntax
+
+/-- Use `refine` in `conv` mode. -/
+macro "refine " e:term : conv => `(conv| tactic => refine $e)
+
+open Elab Tactic
+/--
+The command `#conv tac => e` will run a conv tactic `tac` on `e`, and display the resulting
+expression (discarding the proof).
+For example, `#conv rw [true_and] => True ∧ False` displays `False`.
+There are also shorthand commands for several common conv tactics:
+
+* `#whnf e` is short for `#conv whnf => e`
+* `#simp e` is short for `#conv simp => e`
+* `#norm_num e` is short for `#conv norm_num => e`
+* `#push_neg e` is short for `#conv push_neg => e`
+-/
+elab tk:"#conv " conv:conv " => " e:term : command =>
+  Command.runTermElabM fun _ ↦ do
+    let e ← Elab.Term.elabTermAndSynthesize e none
+    let (rhs, g) ← Conv.mkConvGoalFor e
+    _ ← Tactic.run g.mvarId! do
+      evalTactic conv
+      for mvarId in (← getGoals) do
+        liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
+      pruneSolvedGoals
+      let e' ← instantiateMVars rhs
+      logInfoAt tk e'
+
+@[inherit_doc Parser.Tactic.withReducible]
+macro (name := withReducible) tk:"with_reducible " s:convSeq : conv =>
+  `(conv| tactic' => with_reducible%$tk conv' => $s)
+
+/--
+The command `#whnf e` evaluates `e` to Weak Head Normal Form, which means that the "head"
+of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type.
+It is similar to `#reduce e`, but it does not reduce the expression completely,
+only until the first constructor is exposed. For example:
+```
+open Nat List
+set_option pp.notation false
+#whnf [1, 2, 3].map succ
+-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
+#reduce [1, 2, 3].map succ
+-- cons 2 (cons 3 (cons 4 nil))
+```
+The head of this expression is the `List.cons` constructor,
+so we can see from this much that the list is not empty,
+but the subterms `Nat.succ 1` and `List.map Nat.succ (List.cons 2 (List.cons 3 List.nil))` are
+still unevaluated. `#reduce` is equivalent to using `#whnf` on every subexpression.
+-/
+macro tk:"#whnf " e:term : command => `(command| #conv%$tk whnf => $e)
+
+/--
+The command `#whnfR e` evaluates `e` to Weak Head Normal Form with Reducible transparency,
+that is, it uses `whnf` but only unfolding reducible definitions.
+-/
+macro tk:"#whnfR " e:term : command => `(command| #conv%$tk with_reducible whnf => $e)
+
+/--
+* `#simp => e` runs `simp` on the expression `e` and displays the resulting expression after
+  simplification.
+* `#simp only [lems] => e` runs `simp only [lems]` on `e`.
+* The `=>` is optional, so `#simp e` and `#simp only [lems] e` have the same behavior.
+  It is mostly useful for disambiguating the expression `e` from the lemmas.
+-/
+syntax "#simp" (&" only")? (simpArgs)? " =>"? ppSpace term : command
+macro_rules
+  | `(#simp%$tk $[only%$o]? $[[$args,*]]? $[=>]? $e) =>
+    `(#conv%$tk simp $[only%$o]? $[[$args,*]]? => $e)