Revert 'chore: adaptations for nightly-2024-07-01 (#870)' (#872)

* Revert 'chore: adaptations for nightly-2024-07-01 (#870)'

* Revert 'chore: adaptations for nightly-2024-07-01 (#870)'

Batteries/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 Batteries.Data.List.Init.Attach
 import Batteries.Data.Array.Init.Lemmas
 
 /-!
@@ -129,6 +130,23 @@ protected def maxI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minI (ord := ord.opposite) start stop
 
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`Array {x // P x}` is the same as the input `Array α`.
+-/
+@[inline] private unsafe def attachWithImpl
+    (xs : Array α) (P : α → Prop) (_ : ∀ x ∈ xs, P x) : Array {x // P x} := unsafeCast xs
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x) : Array {x // P x} :=
+  ⟨xs.data.attachWith P fun x h => H x (Array.Mem.mk h)⟩
+
+/-- `O(1)`. "Attach" the proof that the elements of `xs` are in `xs` to produce a new array
+  with the same elements but in the type `{x // x ∈ xs}`. -/
+@[inline] def attach (xs : Array α) : Array {x // x ∈ xs} := xs.attachWith _ fun _ => id
+
 /--
 `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]`

Batteries/Data/List.lean

@@ -1,6 +1,7 @@
 import Batteries.Data.List.Basic
 import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
+import Batteries.Data.List.Init.Attach
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
 import Batteries.Data.List.Pairwise

Batteries/Data/List/Init/Attach.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2023 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+namespace List
+
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`. -/
+@[simp] def pmap {P : α → Prop} (f : ∀ a, P a → β) : ∀ l : List α, (H : ∀ a ∈ l, P a) → List β
+  | [], _ => []
+  | a :: l, H => f a (forall_mem_cons.1 H).1 :: pmap f l (forall_mem_cons.1 H).2
+
+/--
+Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
+`List {x // P x}` is the same as the input `List α`.
+(Someday, the compiler might do this optimization automatically, but until then...)
+-/
+@[inline] private unsafe def attachWithImpl
+    (l : List α) (P : α → Prop) (_ : ∀ x ∈ l, P x) : List {x // P x} := unsafeCast l
+
+/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `l` to produce a new list
+  with the same elements but in the type `{x // P x}`. -/
+@[implemented_by attachWithImpl] def attachWith
+    (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x) : List {x // P x} := pmap Subtype.mk l H
+
+/-- `O(1)`. "Attach" the proof that the elements of `l` are in `l` to produce a new list
+  with the same elements but in the type `{x // x ∈ l}`. -/
+@[inline] def attach (l : List α) : List {x // x ∈ l} := attachWith l _ fun _ => id
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : List α) (H : ∀ a ∈ l, P a) :
+    List β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  let rec go : ∀ L' (hL' : ∀ ⦃x⦄, x ∈ L' → p x),
+      pmap f L' hL' = map (fun ⟨x, hx⟩ => f x hx) (pmap Subtype.mk L' hL')
+  | nil, hL' => rfl
+  | cons _ L', hL' => congrArg _ <| go L' fun _ hx => hL' (.tail _ hx)
+  exact go L h'

Batteries/Data/List/Perm.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Batteries.Tactic.Alias
+import Batteries.Data.List.Init.Attach
 import Batteries.Data.List.Pairwise
+-- Adaptation note: nightly-2024-03-18. We should be able to remove this after nightly-2024-03-19.
+import Lean.Elab.Tactic.Rfl
 
 /-!
 # List Permutations

Batteries/Data/Range/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Batteries.Tactic.SeqFocus
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.Init.Attach
 
 namespace Std.Range
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-07-01
+leanprover/lean4:v4.10.0-rc1