Merge branch 'ft-async' into libuv

.github/workflows/ci.yml

@@ -244,21 +244,21 @@ jobs:
                 "check-level": 2,
                 "cross": true,
                 "shell": "bash -euxo pipefail {0}"
-              },
-              {
-                "name": "Web Assembly",
-                "os": "ubuntu-latest",
-                // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
-                "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
-                "wasm": true,
-                "cmultilib": true,
-                "release": true,
-                "check-level": 2,
-                "cross": true,
-                "shell": "bash -euxo pipefail {0}",
-                // Just a few selected tests because wasm is slow
-                "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
               }
+              // {
+              //   "name": "Web Assembly",
+              //   "os": "ubuntu-latest",
+              //   // Build a native 32bit binary in stage0 and use it to compile the oleans and the wasm build
+              //   "CMAKE_OPTIONS": "-DCMAKE_C_COMPILER_WORKS=1 -DSTAGE0_USE_GMP=OFF -DSTAGE0_LEAN_EXTRA_CXX_FLAGS='-m32' -DSTAGE0_LEANC_OPTS='-m32' -DSTAGE0_CMAKE_CXX_COMPILER=clang++ -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_EXECUTABLE_SUFFIX=\"\" -DUSE_GMP=OFF -DMMAP=OFF -DSTAGE0_MMAP=OFF -DCMAKE_AR=../emsdk/emsdk-main/upstream/emscripten/emar -DCMAKE_TOOLCHAIN_FILE=../emsdk/emsdk-main/upstream/emscripten/cmake/Modules/Platform/Emscripten.cmake -DLEAN_INSTALL_SUFFIX=-linux_wasm32 -DSTAGE0_CMAKE_LIBRARY_PATH=/usr/lib/i386-linux-gnu/",
+              //   "wasm": true,
+              //   "cmultilib": true,
+              //   "release": true,
+              //   "check-level": 2,
+              //   "cross": true,
+              //   "shell": "bash -euxo pipefail {0}",
+              //   // Just a few selected tests because wasm is slow
+              //   "CTEST_OPTIONS": "-R \"leantest_1007\\.lean|leantest_Format\\.lean|leanruntest\\_1037.lean|leanruntest_ac_rfl\\.lean|leanruntest_tempfile.lean\\.|leanruntest_libuv\\.lean\""
+              // }
             ];
             console.log(`matrix:\n${JSON.stringify(matrix, null, 2)}`)
             return matrix.filter((job) => level >= job["check-level"])

README.md

@@ -6,7 +6,8 @@ This is the repository for **Lean 4**.
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Manual](https://lean-lang.org/lean4/doc/)
+- [Documentation Overview](https://lean-lang.org/lean4/doc/)
+- [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
 - [Examples](https://lean-lang.org/lean4/doc/examples.html)
 - [External Contribution Guidelines](CONTRIBUTING.md)

doc/book.toml

@@ -3,7 +3,7 @@ authors = ["Leonardo de Moura", "Sebastian Ullrich"]
 language = "en"
 multilingual = false
 src = "."
-title = "Lean Manual"
+title = "Lean Documentation Overview"
 
 [build]
 build-dir = "out"

src/Init/Core.lean

@@ -2116,16 +2116,14 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
-/-- `IsRefl X r` means the binary relation `r` on `X` is reflexive. -/
+/-- `Refl r` means the binary relation `r` is reflexive, that is, `r x x` always holds. -/
 class Refl (r : α → α → Prop) : Prop where
   /-- A reflexive relation satisfies `r a a`. -/
   refl : ∀ a, r a a
 
-/--
-`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
--/
+/-- `Antisymm r` says that `r` is antisymmetric, that is, `r a b → r b a → a = b`. -/
 class Antisymm (r : α → α → Prop) : Prop where
-  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
+  /-- An antisymmetric relation `r` satisfies `r a b → r b a → a = b`. -/
   antisymm (a b : α) : r a b → r b a → a = b
 
 @[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
@@ -2143,8 +2141,8 @@ class Total (r : α → α → Prop) : Prop where
   /-- A total relation satisfies `r a b ∨ r b a`. -/
   total : ∀ a b, r a b ∨ r b a
 
-/-- `Irrefl X r` means the binary relation `r` on `X` is irreflexive (that is, `r x x` never
-holds). -/
+/-- `Irrefl r` means the binary relation `r` is irreflexive, that is, `r x x` never
+holds. -/
 class Irrefl (r : α → α → Prop) : Prop where
   /-- An irreflexive relation satisfies `¬ r a a`. -/
   irrefl : ∀ a, ¬r a a

src/Init/Data/Array/Basic.lean

@@ -949,13 +949,7 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
 instance instLT [LT α] : LT (Array α) := ⟨fun as bs => as.toList < bs.toList⟩
 instance instLE [LT α] : LE (Array α) := ⟨fun as bs => as.toList ≤ bs.toList⟩
 
-instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLT (Array α) :=
-  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList < bs.toList
-
-instance [DecidableEq α] [LT α] [DecidableLT α] : DecidableLE (Array α) :=
-  inferInstanceAs <| DecidableRel fun (as bs : Array α) => as.toList ≤ bs.toList
-
--- See `Init.Data.Array.Lex` for the boolean valued lexicographic comparator.
+-- See `Init.Data.Array.Lex.Basic` for the boolean valued lexicographic comparator.
 
 /-! ## Auxiliary functions used in metaprogramming.
 

src/Init/Data/Array/Lemmas.lean

@@ -12,7 +12,8 @@ import Init.Data.List.Monadic
 import Init.Data.List.OfFn
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
-import Init.Data.Array.Lex
+import Init.Data.Array.Lex.Basic
+import Init.Data.Range.Lemmas
 import Init.TacticsExtra
 import Init.Data.List.ToArray
 
@@ -26,7 +27,7 @@ namespace Array
 
 /-! ### toList -/
 
-theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
+@[simp] theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b := by
   cases a; cases b; simp
 
 @[simp] theorem toList_eq_nil_iff (l : Array α) : l.toList = [] ↔ l = #[] := by
@@ -925,7 +926,6 @@ theorem mem_or_eq_of_mem_setIfInBounds
 
 /-! ### BEq -/
 
-
 @[simp] theorem beq_empty_iff [BEq α] {xs : Array α} : (xs == #[]) = xs.isEmpty := by
   cases xs
   simp
@@ -954,13 +954,18 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     rw [Bool.eq_iff_iff]
     simp +contextual
 
+private theorem beq_of_beq_singleton [BEq α] {a b : α} : #[a] == #[b] → a == b := by
+  intro h
+  have : isEqv #[a] #[b] BEq.beq = true := h
+  simp [isEqv, isEqvAux] at this
+  assumption
+
 @[simp] theorem reflBEq_iff [BEq α] : ReflBEq (Array α) ↔ ReflBEq α := by
   constructor
   · intro h
     constructor
     intro a
-    suffices (#[a] == #[a]) = true by
-      simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+    apply beq_of_beq_singleton
     simp
   · intro h
     constructor
@@ -973,11 +978,9 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     · intro a b h
       apply singleton_inj.1
       apply eq_of_beq
-      simp only [instBEq, isEqv, isEqvAux]
-      simpa
+      simpa [instBEq, isEqv, isEqvAux]
     · intro a
-      suffices (#[a] == #[a]) = true by
-        simpa only [instBEq, isEqv, isEqvAux, Bool.and_true]
+      apply beq_of_beq_singleton
       simp
   · intro h
     constructor
@@ -989,7 +992,12 @@ theorem size_eq_of_beq [BEq α] {xs ys : Array α} (h : xs == ys) : xs.size = ys
     · intro a
       apply Array.isEqv_self_beq
 
-/-! ### Lexicographic ordering -/
+/-! ### isEqv -/
+
+@[simp] theorem isEqv_eq [DecidableEq α] {l₁ l₂ : Array α} : l₁.isEqv l₂ (· == ·) = (l₁ = l₂) := by
+  cases l₁
+  cases l₂
+  simp
 
 /-! Content below this point has not yet been aligned with `List`. -/
 
@@ -1752,9 +1760,8 @@ theorem getElem_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt :
   conv => rhs; rw [← List.getElem_append_left (bs := bs.toList) (h' := h')]
   apply List.get_of_eq; rw [toList_append]
 
-theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i)
-    (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) :
-    (as ++ bs)[i] = bs[i - as.size] := by
+theorem getElem_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) :
+    (as ++ bs)[i] = bs[i - as.size]'(Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) := by
   simp only [← getElem_toList]
   have h' : i < (as.toList ++ bs.toList).length := by rwa [← length_toList, toList_append] at h
   conv => rhs; rw [← List.getElem_append_right (h₁ := hle) (h₂ := h')]
@@ -2097,8 +2104,7 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
 theorem toListRev_toArray (l : List α) : l.toArray.toListRev = l.reverse := by simp
 
 @[simp] theorem take_toArray (l : List α) (n : Nat) : l.toArray.take n = (l.take n).toArray := by
-  apply ext'
-  simp
+  apply Array.ext <;> simp
 
 @[simp] theorem mapM_toArray [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) :
     l.toArray.mapM f = List.toArray <$> l.mapM f := by
@@ -2352,6 +2358,12 @@ theorem foldr_map' (g : α → β) (f : α → α → α) (f' : β → β → β
   rw [← List.foldl_hom (f := Prod.snd) (g₂ := fun bs x => bs.push x.2) (H := by simp), ← List.foldl_map]
   simp
 
+/-! ### take -/
+
+@[simp] theorem take_size (a : Array α) : a.take a.size = a := by
+  cases a
+  simp
+
 end Array
 
 namespace List
@@ -2390,7 +2402,6 @@ theorem flatMap_toArray_cons {β} (f : α → Array β) (a : α) (as : List α)
     apply ext'
     simp [ih, flatMap_toArray_cons]
 
-
 end Array
 
 /-! ### Deprecations -/

src/Init/Data/Array/Lex.lean

@@ -4,27 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Kim Morrison
 -/
 prelude
-import Init.Data.Array.Basic
-import Init.Data.Nat.Lemmas
-import Init.Data.Range
-
-namespace Array
-
-/--
-Lexicographic comparator for arrays.
-
-`lex as bs lt` is true if
-- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or
-- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
--/
-def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
-  for h : i in [0 : min as.size bs.size] do
-    -- TODO: `omega` should be able to find this itself.
-    have : i < min as.size bs.size := Membership.get_elem_helper h rfl
-    if lt as[i] bs[i] then
-      return true
-    else if as[i] != bs[i] then
-      return false
-  return as.size < bs.size
-
-end Array
+import Init.Data.Array.Lex.Basic
+import Init.Data.Array.Lex.Lemmas

src/Init/Data/Array/Lex/Basic.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Kim Morrison
+-/
+prelude
+import Init.Data.Array.Basic
+import Init.Data.Nat.Lemmas
+import Init.Data.Range
+
+namespace Array
+
+/--
+Lexicographic comparator for arrays.
+
+`lex as bs lt` is true if
+- `bs` is larger than `as` and `as` is pairwise equivalent via `==` to the initial segment of `bs`, or
+- there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`.
+-/
+def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do
+  for h : i in [0 : min as.size bs.size] do
+    -- TODO: `omega` should be able to find this itself.
+    have : i < min as.size bs.size := Membership.get_elem_helper h rfl
+    if lt as[i] bs[i] then
+      return true
+    else if as[i] != bs[i] then
+      return false
+  return as.size < bs.size
+
+end Array