feat: elaborate theorem bodies in parallel

doc/lexical_structure.md

@@ -61,7 +61,7 @@ Parts of atomic names can be escaped by enclosing them in pairs of French double
    letterlike_symbols: [℀-⅏]
    escaped_ident_part: "«" [^«»\r\n\t]* "»"
    atomic_ident_rest: atomic_ident_start | [0-9'ⁿ] | subscript
-   subscript: [₀-₉ₐ-ₜᵢ-ᵪ]
+   subscript: [₀-₉ₐ-ₜᵢ-ᵪⱼ]
 ```
 
 String Literals

src/CMakeLists.txt

@@ -699,12 +699,12 @@ else()
 endif()
 
 if(NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
-  add_custom_target(lake_lib ALL
+  add_custom_target(lake_lib
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS leanshared
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Lake
     VERBATIM)
-  add_custom_target(lake_shared ALL
+  add_custom_target(lake_shared
     WORKING_DIRECTORY ${LEAN_SOURCE_DIR}
     DEPENDS lake_lib
     COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make libLake_shared

src/Init/Data/Array/Attach.lean

@@ -6,6 +6,7 @@ Authors: Joachim Breitner, Mario Carneiro
 prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
+import Init.Data.Array.Count
 import Init.Data.List.Attach
 
 namespace Array
@@ -142,10 +143,16 @@ theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
   cases l
   simp [List.pmap_eq_map_attach]
 
+@[simp]
+theorem pmap_eq_attachWith {p q : α → Prop} (f : ∀ a, p a → q a) (l H) :
+    pmap (fun a h => ⟨a, f a h⟩) l H = l.attachWith q (fun x h => f x (H x h)) := by
+  cases l
+  simp [List.pmap_eq_attachWith]
+
 theorem attach_map_coe (l : Array α) (f : α → β) :
     (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
   cases l
-  simp [List.attach_map_coe]
+  simp
 
 theorem attach_map_val (l : Array α) (f : α → β) : (l.attach.map fun i => f i.val) = l.map f :=
   attach_map_coe _ _
@@ -172,6 +179,12 @@ theorem mem_attach (l : Array α) : ∀ x, x ∈ l.attach
     rcases this with ⟨⟨_, _⟩, m, rfl⟩
     exact m
 
+@[simp]
+theorem mem_attachWith (l : Array α) {q : α → Prop} (H) (x : {x // q x}) :
+    x ∈ l.attachWith q H ↔ x.1 ∈ l := by
+  cases l
+  simp
+
 @[simp]
 theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l H b} :
     b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b := by
@@ -223,16 +236,16 @@ theorem attachWith_ne_empty_iff {l : Array α} {P : α → Prop} {H : ∀ a ∈
   cases l; simp
 
 @[simp]
-theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (n : Nat) :
-    (pmap f l h)[n]? = Option.pmap f l[n]? fun x H => h x (mem_of_getElem? H) := by
+theorem getElem?_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) (i : Nat) :
+    (pmap f l h)[i]? = Option.pmap f l[i]? fun x H => h x (mem_of_getElem? H) := by
   cases l; simp
 
 @[simp]
-theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {n : Nat}
-    (hn : n < (pmap f l h).size) :
-    (pmap f l h)[n] =
-      f (l[n]'(@size_pmap _ _ p f l h ▸ hn))
-        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hn))) := by
+theorem getElem_pmap {p : α → Prop} (f : ∀ a, p a → β) {l : Array α} (h : ∀ a ∈ l, p a) {i : Nat}
+    (hi : i < (pmap f l h).size) :
+    (pmap f l h)[i] =
+      f (l[i]'(@size_pmap _ _ p f l h ▸ hi))
+        (h _ (getElem_mem (@size_pmap _ _ p f l h ▸ hi))) := by
   cases l; simp
 
 @[simp]
@@ -256,6 +269,18 @@ theorem getElem_attach {xs : Array α} {i : Nat} (h : i < xs.attach.size) :
     xs.attach[i] = ⟨xs[i]'(by simpa using h), getElem_mem (by simpa using h)⟩ :=
   getElem_attachWith h
 
+@[simp] theorem pmap_attach (l : Array α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
+    pmap f l.attach H =
+      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩) := by
+  ext <;> simp
+
+@[simp] theorem pmap_attachWith (l : Array α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
+    pmap f (l.attachWith q H₁) H₂ =
+      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
+        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩) := by
+  ext <;> simp
+
 theorem foldl_pmap (l : Array α) {P : α → Prop} (f : (a : α) → P a → β)
   (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
     (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
@@ -313,11 +338,7 @@ theorem attachWith_map {l : Array α} (f : α → β) {P : β → Prop} {H : ∀
     (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
       fun ⟨x, h⟩ => ⟨f x, h⟩ := by
   cases l
-  ext
-  · simp
-  · simp only [List.map_toArray, List.attachWith_toArray, List.getElem_toArray,
-      List.getElem_attachWith, List.getElem_map, Function.comp_apply]
-    erw [List.getElem_attachWith] -- Why is `erw` needed here?
+  simp [List.attachWith_map]
 
 theorem map_attachWith {l : Array α} {P : α → Prop} {H : ∀ (a : α), a ∈ l → P a}
     (f : { x // P x } → β) :
@@ -347,7 +368,23 @@ theorem attach_filter {l : Array α} (p : α → Bool) :
   simp [List.attach_filter, List.map_filterMap, Function.comp_def]
 
 -- We are still missing here `attachWith_filterMap` and `attachWith_filter`.
--- Also missing are `filterMap_attach`, `filter_attach`, `filterMap_attachWith` and `filter_attachWith`.
+
+@[simp]
+theorem filterMap_attachWith {q : α → Prop} {l : Array α} {f : {x // q x} → Option β} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filterMap f 0 stop = l.attach.filterMap (fun ⟨x, h⟩ => f ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem filter_attachWith {q : α → Prop} {l : Array α} {p : {x // q x} → Bool} (H)
+    (w : stop = (l.attachWith q H).size) :
+    (l.attachWith q H).filter p 0 stop =
+      (l.attach.filter (fun ⟨x, h⟩ => p ⟨x, H _ h⟩)).map (fun ⟨x, h⟩ => ⟨x, H _ h⟩) := by
+  subst w
+  cases l
+  simp [Function.comp_def, List.filter_map]
 
 theorem pmap_pmap {p : α → Prop} {q : β → Prop} (g : ∀ a, p a → β) (f : ∀ b, q b → γ) (l H₁ H₂) :
     pmap f (pmap g l H₁) H₂ =
@@ -427,16 +464,48 @@ theorem reverse_attach (xs : Array α) :
 
 @[simp] theorem back?_attachWith {P : α → Prop} {xs : Array α}
     {H : ∀ (a : α), a ∈ xs → P a} :
-    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back?_eq_some h)⟩) := by
+    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩) := by
   cases xs
   simp
 
 @[simp]
 theorem back?_attach {xs : Array α} :
-    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back?_eq_some h⟩ := by
+    xs.attach.back? = xs.back?.pbind fun a h => some ⟨a, mem_of_back? h⟩ := by
   cases xs
   simp
 
+@[simp]
+theorem countP_attach (l : Array α) (p : α → Bool) :
+    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p := by
+  cases l
+  simp [Function.comp_def]
+
+@[simp]
+theorem countP_attachWith {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (q : α → Bool) :
+    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q := by
+  cases l
+  simp
+
+@[simp]
+theorem count_attach [DecidableEq α] (l : Array α) (a : {x // x ∈ l}) :
+    l.attach.count a = l.count ↑a := by
+  rcases l with ⟨l⟩
+  simp only [List.attach_toArray, List.attachWith_mem_toArray, List.count_toArray]
+  rw [List.map_attach, List.count_eq_countP]
+  simp only [Subtype.beq_iff]
+  rw [List.countP_pmap, List.countP_attach (p := (fun x => x == a.1)), List.count]
+
+@[simp]
+theorem count_attachWith [DecidableEq α] {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) (a : {x // p x}) :
+    (l.attachWith p H).count a = l.count ↑a := by
+  cases l
+  simp
+
+@[simp] theorem countP_pmap {p : α → Prop} (g : ∀ a, p a → β) (f : β → Bool) (l : Array α) (H₁) :
+    (l.pmap g H₁).countP f =
+      l.attach.countP (fun ⟨a, m⟩ => f (g a (H₁ a m))) := by
+  simp [pmap_eq_map_attach, countP_map, Function.comp_def]
+
 /-! ## unattach
 
 `Array.unattach` is the (one-sided) inverse of `Array.attach`. It is a synonym for `Array.map Subtype.val`.
@@ -455,7 +524,7 @@ and is ideally subsequently simplified away by `unattach_attach`.
 
 If not, usually the right approach is `simp [Array.unattach, -Array.map_subtype]` to unfold.
 -/
-def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) := l.map (·.val)
+def unattach {α : Type _} {p : α → Prop} (l : Array { x // p x }) : Array α := l.map (·.val)
 
 @[simp] theorem unattach_nil {p : α → Prop} : (#[] : Array { x // p x }).unattach = #[] := rfl
 @[simp] theorem unattach_push {p : α → Prop} {a : { x // p x }} {l : Array { x // p x }} :
@@ -578,4 +647,16 @@ and simplifies these to the function directly taking the value.
   cases l₂
   simp
 
+@[simp] theorem unattach_flatten {p : α → Prop} {l : Array (Array { x // p x })} :
+    l.flatten.unattach = (l.map unattach).flatten := by
+  unfold unattach
+  cases l using array₂_induction
+  simp only [flatten_toArray, List.map_map, Function.comp_def, List.map_id_fun', id_eq,
+    List.map_toArray, List.map_flatten, map_subtype, map_id_fun', List.unattach_toArray, mk.injEq]
+  simp only [List.unattach]
+
+@[simp] theorem unattach_mkArray {p : α → Prop} {n : Nat} {x : { x // p x }} :
+    (Array.mkArray n x).unattach = Array.mkArray n x.1 := by
+  simp [unattach]
+
 end Array

src/Init/Data/Array/Basic.lean

@@ -455,7 +455,7 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
 /-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
 @[inline]
 def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
-    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+    (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → m β) : m (Array β) :=
   let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
     match i, inv with
     | 0,    _  => pure bs
@@ -464,12 +464,12 @@ def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
         rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
         apply Nat.le_add_right
       have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get j j_lt)))
+      map i (j+1) this (bs.push (← f j (as.get j j_lt) j_lt))
   map as.size 0 rfl (mkEmpty as.size)
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : Nat → α → m β) (as : Array α) : m (Array β) :=
-  as.mapFinIdxM fun i a => f i a
+  as.mapFinIdxM fun i a _ => f i a
 
 @[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m (Option β)) (as : Array α) : m (Option β) := do
@@ -579,16 +579,25 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 /-- Sum of an array.
 
 `Array.sum #[a, b, c] = a + (b + (c + 0))` -/
+@[inline]
 def sum {α} [Add α] [Zero α] : Array α → α :=
   foldr (· + ·) 0
 
+@[inline]
+def countP {α : Type u} (p : α → Bool) (as : Array α) : Nat :=
+  as.foldr (init := 0) fun a acc => bif p a then acc + 1 else acc
+
+@[inline]
+def count {α : Type u} [BEq α] (a : α) (as : Array α) : Nat :=
+  countP (· == a) as
+
 @[inline]
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
   Id.run <| as.mapM f
 
 /-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
 @[inline]
-def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : (i : Nat) → α → (h : i < as.size) → β) : Array β :=
   Id.run <| as.mapFinIdxM f
 
 @[inline]