Merge branch 'master' of https://github.com/leanprover/lean4 into nor…

…malize_crlf

RELEASES.md

@@ -22,6 +22,18 @@ v4.9.0 (development in progress)
   definition itself can be marked as `@[semireducible]` to get the previous
   behavor.
 
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
 v4.8.0
 ---------
 
@@ -155,18 +167,6 @@ fact.def :
 
 * `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
 
-* The `MessageData.ofPPFormat` constructor has been removed.
-  Its functionality has been split into two:
-
-  - for lazy structured messages, please use `MessageData.lazy`;
-  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
-
-  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
-
-* The `MessageData.ofFormat` constructor has been turned into a function.
-  If you need to inspect `MessageData`,
-  you can pattern-match on `MessageData.ofFormatWithInfos`.
-
 v4.7.0
 ---------
 

doc/syntax_highlight_in_latex.md

@@ -43,17 +43,17 @@ $ pdflatex test.tex
 
 ## Example with `minted`
 
-First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`](https://raw.githubusercontent.com/leanprover/lean4/master/doc/latex/lean4.py), which contains an version of the Lean highlighter updated for Lean 4, and the following sample LaTeX file `test.tex` into the same directory:
+First [install Pygments](https://pygments.org/download/) (version 2.18 or newer).
+Then save the following sample LaTeX file `test.tex` into the same directory:
 
 ```latex
 \documentclass{article}
 \usepackage{fontspec}
 % switch to a monospace font supporting more Unicode characters
 \setmonofont{FreeMono}
 \usepackage{minted}
-% instruct minted to use our local theorem.py
-\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
-\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
+\newmintinline[lean]{lean4}{bgcolor=white}
+\newminted[leancode]{lean4}{fontsize=\footnotesize}
 \usemintedstyle{tango}  % a nice, colorful theme
 
 \begin{document}
@@ -67,9 +67,6 @@ theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f
 \end{document}
 ```
 
-If your version of `minted` is v2.7 or newer, but before v3.0,
-you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.
-
 You can then compile `test.tex` by executing the following command:
 
 ```bash
@@ -81,11 +78,14 @@ Some remarks:
  - either `xelatex` or `lualatex` is required to handle Unicode characters in the code.
  - `--shell-escape` is needed to allow `xelatex` to execute `pygmentize` in a shell.
  - If the chosen monospace font is missing some Unicode symbols, you can direct them to be displayed using a fallback font or other replacement LaTeX code.
-``` latex
-\usepackage{newunicodechar}
-\newfontfamily{\freeserif}{DejaVu Sans}
-\newunicodechar{✝}{\freeserif{✝}}
-\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
-```
- - minted has a "helpful" feature that draws red boxes around characters the chosen lexer doesn't recognize.
- Since the Lean lexer cannot encompass all user-defined syntax, it is advisable to [work around](https://tex.stackexchange.com/a/343506/14563) this feature.
+   ``` latex
+   \usepackage{newunicodechar}
+   \newfontfamily{\freeserif}{DejaVu Sans}
+   \newunicodechar{✝}{\freeserif{✝}}
+   \newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}
+   ```
+ - If you are using an old version of Pygments, you can copy 
+   [`lean.py`](https://raw.githubusercontent.com/pygments/pygments/master/pygments/lexers/lean.py) into your working directory,
+   and use `lean4.py:Lean4Lexer -x` instead of `lean4` above.
+   If your version of `minted` is v2.7 or newer, but before v3.0,
+   you will additionally need to follow the workaround described in https://github.com/gpoore/minted/issues/360.

src/Init/Data/Nat/Lemmas.lean

@@ -794,6 +794,9 @@ theorem shiftLeft_shiftLeft (m n : Nat) : ∀ k, (m <<< n) <<< k = m <<< (n + k)
   | 0 => rfl
   | k + 1 => by simp [← Nat.add_assoc, shiftLeft_shiftLeft _ _ k, shiftLeft_succ]
 
+@[simp] theorem shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x := by
+  rw [Nat.shiftLeft_eq, Nat.shiftRight_eq_div_pow, Nat.mul_div_cancel _ (Nat.two_pow_pos _)]
+
 theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x + y / m := by
   match x with
   | 0 => simp

src/Init/Data/Nat/Linear.lean

@@ -714,4 +714,10 @@ theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 
-end Nat.Linear
+end Linear
+
+def elimOffset {α : Sort u} (a b k : Nat) (h₁ : a + k = b + k) (h₂ : a = b → α) : α := by
+  simp_arith at h₁
+  exact h₂ h₁
+
+end Nat

src/Init/Grind.lean

@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Norm
 import Init.Grind.Tactics
+import Init.Grind.Lemmas

src/Init/Grind/Lemmas.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
+  fun hp => h (he.mp hp)
+
+end Lean.Grind

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -71,7 +71,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
 
 /-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
 def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
-  m.run' HashMap.empty |>.run' {} { cfg } |>.run
+  m.run' HashMap.empty |>.run' {} { cfg } |>.run'
 
 /-- Retrieve the user-specified configuration options. -/
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg

src/Lean/Meta/Canonicalizer.lean

@@ -63,8 +63,11 @@ abbrev CanonM := ReaderT TransparencyMode $ StateRefT State MetaM
 The definitionally equality tests are performed using the given transparency mode.
 We claim `TransparencyMode.instances` is a good setting for most applications.
 -/
-def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) : MetaM α :=
-  StateRefT'.run' (x transparency) {}
+def CanonM.run' (x : CanonM α) (transparency := TransparencyMode.instances) (s : State := {}) : MetaM α :=
+  StateRefT'.run' (x transparency) s
+
+def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) (s : State := {}) : MetaM (α × State) :=
+  StateRefT'.run (x transparency) s
 
 private partial def mkKey (e : Expr) : CanonM UInt64 := do
   if let some hash := unsafe (← get).cache.find? { e } then

src/Lean/Meta/Tactic/Cases.lean

@@ -200,7 +200,7 @@ private def toCasesSubgoals (s : Array InductionSubgoal) (ctorNames : Array Name
     { ctorName           := ctorName,
       toInductionSubgoal := s }
 
-partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := do
+partial def unifyEqs? (numEqs : Nat) (mvarId : MVarId) (subst : FVarSubst) (caseName? : Option Name := none): MetaM (Option (MVarId × FVarSubst)) := withIncRecDepth do
   if numEqs == 0 then
     return some (mvarId, subst)
   else

src/Lean/Meta/Tactic/Grind.lean

@@ -6,6 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
-import Lean.Meta.Tactic.Grind.EnsureNoMVar
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Preprocessor
+import Lean.Meta.Tactic.Grind.Util