chore: merge main

.github/workflows/build.yml

@@ -28,28 +28,48 @@ jobs:
           find Std -name "*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > Std.lean
 
       - name: build std
-        run: lake build
+        id: build
+        run: lake build -Kwerror
 
       - name: test std
+        if: steps.build.outcome == 'success'
         run: make test
 
       - name: lint std
+        if: steps.build.outcome == 'success'
         run: make lint
 
       - name: check that all files are imported
+        if: always()
         run: git diff --exit-code
 
       - name: Check for forbidden character ↦
+        if: always()
         run: |
           if grep -r -n --include=\*.lean -e '↦' . ; then
             echo "Error: Found forbidden character ↦"
             exit 1
           fi
 
+      - name: Check for 'namespace Mathlib'
+        if: always()
+        run: |
+          if grep -r -n --include=\*.lean -e 'namespace Mathlib' . ; then
+            echo "Error: Found 'namespace Mathlib'"
+            exit 1
+          fi
+
       - name: Check for long lines
+        if: always()
         run: |
           ! (find Std -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; | grep -v -E 'https?://')
 
       - name: Check for trailing whitespace
+        if: always()
         run: |
           scripts/lintWhitespace.sh
+
+      - name: Don't 'import Lean', use precise imports
+        if: always()
+        run: |
+          ! (find . -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/workflows/nightly_bump_toolchain.yml

@@ -8,6 +8,7 @@ on:
 
 jobs:
   update-toolchain:
+    if: github.repository_owner == 'leanprover'
     runs-on: ubuntu-latest
 
     steps:

.github/workflows/nightly_detect_failure.yml

@@ -2,11 +2,13 @@ name: Post to zulip if the nightly-testing branch is failing.
 
 on:
   workflow_run:
-    workflows: ["continuous integration"]
+    workflows: ["ci"]
     types:
       - completed
 
 jobs:
+  # Whenever `nightly-testing` fails CI,
+  # notify the 'mathlib reviewers' stream on Zulip.
   handle_failure:
     if: ${{ github.event.workflow_run.conclusion == 'failure' && github.event.workflow_run.head_branch == 'nightly-testing' }}
     runs-on: ubuntu-latest
@@ -23,3 +25,27 @@ jobs:
         topic: 'CI failure on the nightly-testing branch'
         content: |
           The latest CI for Std's [`nightly-testing`](https://github.com/leanprover/std4/tree/nightly-testing) branch has [failed](https://github.com/${{ github.repository }}/actions/runs/${{ github.event.workflow_run.id }}).
+
+  # Whenever `nightly-testing` passes CI,
+  # push it to `nightly-testing-YYYY-MM-DD` so we have a known good version of Std on that nightly release.
+  handle_success:
+    if: ${{ github.event.workflow_run.conclusion == 'success' && github.event.workflow_run.head_branch == 'nightly-testing' }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout code
+      uses: actions/checkout@v3
+      with:
+        ref: nightly-testing # checkout nightly-testing branch
+        fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
+        token: ${{ secrets.NIGHTLY_TESTING }}
+    - name: Update the nightly-testing-YYYY-MM-DD branch
+      run: |
+        toolchain=$(<lean-toolchain)
+        if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
+          version=${BASH_REMATCH[1]}
+          git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
+        else
+          echo "Error: The file lean-toolchain does not contain the expected pattern."
+          exit 1
+        fi

.github/workflows/nightly_merge_master.yml

@@ -9,6 +9,7 @@ on:
 
 jobs:
   merge-to-nightly:
+    if: github.repository_owner == 'leanprover'
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository

.gitignore

@@ -1,6 +1,10 @@
-/build
-/prelude/build
-lakefile.olean
+# Prior to v4.3.0-rc2 lake stored files in these locations.
+# We'll leave them in the `.gitignore` for a while for users switching between toolchains.
+/build/
+/lake-packages/
+/lakefile.olean
+# After v4.3.0-rc2 lake stores its files here:
+/.lake/
 # Note: because std has no dependencies, the lake-manifest contains no information
 # that is not regenerated automatically by lake, so this avoids conflicts when
 # lake decides to upgrade its manifest version.

GNUmakefile

@@ -13,4 +13,4 @@ test/%.run: build
 	lake env lean test/$*
 
 lint: build
-	./build/bin/runLinter
+	./.lake/build/bin/runLinter

README.md

@@ -48,3 +48,9 @@ Note that documentation for the latest nightly of `std4` is available as part of
 documentation][mathlib4 docs].
 
 [mathlib4 docs]: https://leanprover-community.github.io/mathlib4_docs/Std.html
+
+# Contributing
+
+The easiest way to contribute is to find a missing proof and complete it. The `proof_wanted`
+declaration documents statements that have been identified as being useful, but that have not yet
+been proven.

Std.lean

@@ -13,6 +13,7 @@ import Std.CodeAction.Misc
 import Std.Control.ForInStep
 import Std.Control.ForInStep.Basic
 import Std.Control.ForInStep.Lemmas
+import Std.Control.Lemmas
 import Std.Data.Array.Basic
 import Std.Data.Array.Init.Basic
 import Std.Data.Array.Init.Lemmas
@@ -25,27 +26,34 @@ import Std.Data.BinomialHeap.Basic
 import Std.Data.BinomialHeap.Lemmas
 import Std.Data.BitVec
 import Std.Data.BitVec.Basic
+import Std.Data.BitVec.Bitblast
+import Std.Data.BitVec.Folds
+import Std.Data.BitVec.Lemmas
 import Std.Data.Bool
 import Std.Data.Char
 import Std.Data.DList
 import Std.Data.Fin.Basic
 import Std.Data.Fin.Init.Lemmas
+import Std.Data.Fin.Iterate
 import Std.Data.Fin.Lemmas
 import Std.Data.HashMap
 import Std.Data.HashMap.Basic
+import Std.Data.HashMap.Lemmas
 import Std.Data.HashMap.WF
 import Std.Data.Int.Basic
 import Std.Data.Int.DivMod
 import Std.Data.Int.Lemmas
 import Std.Data.Json
 import Std.Data.List.Basic
 import Std.Data.List.Count
+import Std.Data.List.Init.Attach
 import Std.Data.List.Init.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.List.Pairwise
 import Std.Data.MLList.Basic
 import Std.Data.MLList.Heartbeats
 import Std.Data.Nat.Basic
+import Std.Data.Nat.Bitwise
 import Std.Data.Nat.Gcd
 import Std.Data.Nat.Init.Lemmas
 import Std.Data.Nat.Lemmas
@@ -82,15 +90,16 @@ import Std.Lean.HashMap
 import Std.Lean.HashSet
 import Std.Lean.InfoTree
 import Std.Lean.Json
+import Std.Lean.LocalContext
 import Std.Lean.Meta.AssertHypotheses
 import Std.Lean.Meta.Basic
 import Std.Lean.Meta.Clear
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.Expr
 import Std.Lean.Meta.Inaccessible
 import Std.Lean.Meta.InstantiateMVars
-import Std.Lean.Meta.LCtx
 import Std.Lean.Meta.SavedState
+import Std.Lean.Meta.Simp
 import Std.Lean.Meta.UnusedNames
 import Std.Lean.MonadBacktrack
 import Std.Lean.Name
@@ -111,6 +120,7 @@ import Std.Tactic.Alias
 import Std.Tactic.Basic
 import Std.Tactic.ByCases
 import Std.Tactic.Case
+import Std.Tactic.Change
 import Std.Tactic.CoeExt
 import Std.Tactic.Congr
 import Std.Tactic.Exact
@@ -129,15 +139,18 @@ import Std.Tactic.Lint.Misc
 import Std.Tactic.Lint.Simp
 import Std.Tactic.Lint.TypeClass
 import Std.Tactic.NoMatch
+import Std.Tactic.NormCast
 import Std.Tactic.NormCast.Ext
 import Std.Tactic.NormCast.Lemmas
 import Std.Tactic.OpenPrivate
+import Std.Tactic.PermuteGoals
 import Std.Tactic.PrintDependents
 import Std.Tactic.PrintPrefix
 import Std.Tactic.RCases
 import Std.Tactic.Relation.Rfl
 import Std.Tactic.Relation.Symm
 import Std.Tactic.Replace
+import Std.Tactic.RunCmd
 import Std.Tactic.SeqFocus
 import Std.Tactic.ShowTerm
 import Std.Tactic.SimpTrace
@@ -151,5 +164,6 @@ import Std.Util.Cache
 import Std.Util.ExtendedBinder
 import Std.Util.LibraryNote
 import Std.Util.Pickle
+import Std.Util.ProofWanted
 import Std.Util.TermUnsafe
 import Std.WF

Std/Classes/LawfulMonad.lean

@@ -52,6 +52,20 @@ instance : LawfulMonad Option := LawfulMonad.mk'
 instance : LawfulApplicative Option := inferInstance
 instance : LawfulFunctor Option := inferInstance
 
+instance : LawfulMonad (EStateM ε σ) := .mk'
+  (id_map := fun x => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.map]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (pure_bind := fun _ _ => rfl)
+  (bind_assoc := fun x _ _ => funext <| fun s => by
+    dsimp only [EStateM.instMonadEStateM, EStateM.bind]
+    match x s with
+    | .ok _ _ => rfl
+    | .error _ _ => rfl)
+  (map_const := fun _ _ => rfl)
+
 /-!
 ## SatisfiesM
 
@@ -74,7 +88,7 @@ namespace SatisfiesM
 /-- If `p` is always true, then every `x` satisfies it. -/
 theorem of_true [Applicative m] [LawfulApplicative m] {x : m α}
     (h : ∀ a, p a) : SatisfiesM p x :=
-  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp [← comp_map, Function.comp]⟩
+  ⟨(fun a => ⟨a, h a⟩) <$> x, by simp [← comp_map, Function.comp_def]⟩
 
 /--
 If `p` is always true, then every `x` satisfies it.
@@ -93,7 +107,7 @@ protected theorem map [Functor m] [LawfulFunctor m] {x : m α}
     (hx : SatisfiesM p x) (hf : ∀ {a}, p a → q (f a)) : SatisfiesM q (f <$> x) := by
   let ⟨x', hx⟩ := hx
   refine ⟨(fun ⟨a, h⟩ => ⟨f a, hf h⟩) <$> x', ?_⟩
-  rw [← hx]; simp [← comp_map, Function.comp]
+  rw [← hx]; simp [← comp_map, Function.comp_def]
 
 /--
 `SatisfiesM` distributes over `<$>`, strongest postcondition version.
@@ -127,7 +141,7 @@ protected theorem seq [Applicative m] [LawfulApplicative m] {x : m α}
   match f, x, hf, hx with | _, _, ⟨f, rfl⟩, ⟨x, rfl⟩ => ?_
   refine ⟨(fun ⟨a, h₁⟩ ⟨b, h₂⟩ => ⟨a b, H h₁ h₂⟩) <$> f <*> x, ?_⟩
   simp only [← pure_seq]; simp [SatisfiesM, seq_assoc]
-  simp only [← pure_seq]; simp [seq_assoc, Function.comp]
+  simp only [← pure_seq]; simp [seq_assoc, Function.comp_def]
 
 /-- `SatisfiesM` distributes over `<*>`, strongest postcondition version. -/
 protected theorem seq_post [Applicative m] [LawfulApplicative m] {x : m α}

Std/Classes/Order.lean

@@ -90,6 +90,12 @@ theorem cmp_congr_right [TransCmp cmp] (yz : cmp y z = .eq) : cmp x y = cmp x z
 
 end TransCmp
 
+end Std
+
+namespace Ordering
+
+open Std
+
 /-- Pull back a comparator by a function `f`, by applying the comparator to both arguments. -/
 @[inline] def byKey (f : α → β) (cmp : β → β → Ordering) (a b : α) : Ordering := cmp (f a) (f b)
 
@@ -101,3 +107,17 @@ instance (f : α → β) (cmp : β → β → Ordering) [TransCmp cmp] : TransCm
 
 instance (f : α → β) (cmp : β → β → Ordering) [TransCmp cmp] : TransCmp (byKey f cmp) where
   le_trans h₁ h₂ := TransCmp.le_trans (α := β) h₁ h₂
+
+end Ordering
+
+@[simp] theorem ge_iff_le [LE α] {x y : α} : x ≥ y ↔ y ≤ x := Iff.rfl
+
+@[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y ↔ y < x := Iff.rfl
+
+theorem le_of_eq_of_le {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c := by subst h₁; exact h₂
+
+theorem le_of_le_of_eq {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c := by subst h₂; exact h₁
+
+theorem lt_of_eq_of_lt {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) : a < c := by subst h₁; exact h₂
+
+theorem lt_of_lt_of_eq {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c := by subst h₂; exact h₁

Std/Control/Lemmas.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2023 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+import Std.Tactic.Ext
+
+namespace ReaderT
+
+attribute [ext] ReaderT.ext
+
+@[simp] theorem run_failure [Monad m] [Alternative m] (ctx : ρ) :
+    (failure : ReaderT ρ m α).run ctx = failure := rfl
+
+@[simp] theorem run_orElse [Monad m] [Alternative m] (x y : ReaderT ρ m α) (ctx : ρ) :
+    (x <|> y).run ctx = (x.run ctx <|> y.run ctx) := rfl
+
+end ReaderT
+
+namespace StateT
+
+attribute [ext] StateT.ext
+
+@[simp] theorem run_failure {α σ} [Monad m] [Alternative m] (s : σ) :
+    (failure : StateT σ m α).run s = failure := rfl
+
+@[simp] theorem run_orElse {α σ} [Monad m] [Alternative m] (x y : StateT σ m α) (s : σ) :
+    (x <|> y).run s = (x.run s <|> y.run s) := rfl
+
+end StateT

Std/Data/Array/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn, Jannis Limperg
 -/
+import Std.Data.List.Init.Attach
 import Std.Data.Array.Init.Basic
 import Std.Data.Ord
 
@@ -19,10 +20,6 @@ namespace Array
 def reduceOption (l : Array (Option α)) : Array α :=
   l.filterMap id
 
-/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
-def zipWithIndex (arr : Array α) : Array (α × Nat) :=
-  arr.mapIdx fun i a => (a, i)
-
 /--
 Check whether `xs` and `ys` are equal as sets, i.e. they contain the same
 elements when disregarding order and duplicates. `O(n*m)`! If your element type
@@ -109,6 +106,23 @@ protected def maxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minI (ord := ord.opposite) start stop
 
+/--
+Unsafe implementation of `attach`, taking advantage of the fact that the representation of
+`Array {x // x ∈ xs}` is the same as the input `Array α`.
+-/
+@[inline] private unsafe def attachImpl (xs : Array α) : Array {x // x ∈ xs} := unsafeCast xs
+
+/-- "Attach" the proof that the elements of `xs` are in `xs` to produce a new list
+  with the same elements but in the type `{x // x ∈ xs}`. -/
+@[implemented_by attachImpl] def attach (xs : Array α) : Array {x // x ∈ xs} :=
+  ⟨xs.data.pmap Subtype.mk fun _ => Array.Mem.mk⟩
+
+/--
+`O(|join L|)`. `join L` concatenates all the arrays in `L` into one array.
+* `join #[#[a], #[], #[b, c], #[d, e, f]] = #[a, b, c, d, e, f]`
+-/
+@[inline] def join (l : Array (Array α)) : Array α := l.foldl (· ++ ·) #[]
+
 end Array
 
 

Std/Data/Array/Init/Basic.lean

@@ -12,6 +12,10 @@ This file contains some definitions in `Array` needed for `Std.List.Basic`.
 
 namespace Array
 
+/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
+def zipWithIndex (arr : Array α) : Array (α × Nat) :=
+  arr.mapIdx fun i a => (a, i)
+
 /-- Like `as.toList ++ l`, but in a single pass. -/
 @[inline] def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l