feat: List.toArray def equal to Array.mk

src/Init/Core.lean

@@ -1603,6 +1603,98 @@ instance : Subsingleton (Squash α) where
     apply Quot.sound
     trivial
 
+/-! # List primitives -/
+
+/-- Auxiliary for `List.reverse`. `List.reverseAux l r = l.reverse ++ r`, but it is defined directly. -/
+def List.reverseAux : List α → List α → List α
+  | nil,    r => r
+  | a :: l, r => reverseAux l (a :: r)
+
+/--
+`O(|as|)`. Reverse of a list:
+* `[1, 2, 3, 4].reverse = [4, 3, 2, 1]`
+
+Note that because of the "functional but in place" optimization implemented by Lean's compiler,
+this function works without any allocations provided that the input list is unshared:
+it simply walks the linked list and reverses all the node pointers.
+-/
+def List.reverse (as : List α) : List α := reverseAux as nil
+
+theorem List.reverseAux_reverseAux (as bs cs : List α) :
+    reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as nil) cs) := by
+  induction as generalizing bs with
+  | nil => rfl
+  | cons a as ih =>
+    rw [reverseAux, reverseAux, ih (a :: bs),
+        reverseAux, ih (a :: nil),
+        reverseAux, reverseAux]
+
+/--
+`O(|xs|)`: append two lists. `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`.
+It takes time proportional to the first list.
+-/
+protected def List.append : (xs ys : List α) → List α
+  | nil,    bs => bs
+  | a ::as, bs => a :: List.append as bs
+
+/-- Tail-recursive version of `List.append`. -/
+def List.appendTR (as bs : List α) : List α := reverseAux as.reverse bs
+
+@[csimp] theorem List.append_eq_appendTR : @List.append = @appendTR := by
+  apply funext; intro α; apply funext; intro as; apply funext; intro bs
+  induction as with
+  | nil  => rfl
+  | cons a as ih =>
+    rw [appendTR, reverse, reverseAux, reverseAux_reverseAux]
+    exact congrArg (cons a) ih
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+@[inline, match_pattern]
+abbrev List.toArray := @Array.mk
+
+/-- Auxiliary definition for `toArray`. -/
+@[inline_if_reduce]
+def List.toArrayAux : List α → Array α → Array α
+  | nil,     r => r
+  | a :: as, r => toArrayAux as (r.push a)
+
+/-- A non-tail-recursive version of `List.length`, used for `List.toArray`. -/
+@[inline_if_reduce]
+def List.redLength : List α → Nat
+  | nil     => 0
+  | _ :: as => as.redLength.succ
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
+@[inline, export lean_list_to_array]
+def List.toArrayTR (as : List α) : Array α := as.toArrayAux (Array.mkEmpty as.redLength)
+
+theorem List.toArrayAux_eq_mk (l r : List α) : toArrayAux l ⟨r⟩ = { data := List.append r l } := by
+  induction l generalizing r with
+  | nil =>
+    rw [toArrayAux]
+    apply congrArg Array.mk
+    induction r with
+    | nil => rw [List.append]
+    | cons b r ind => rw [List.append, ←ind]
+  | cons a l ind =>
+    rw [toArrayAux, Array.push, ind]
+    clear ind
+    apply congrArg Array.mk
+    induction r generalizing l with
+    | nil => rfl
+    | cons b r ind =>
+      rw [concat, List.append, List.append]
+      exact congrArg (cons b) (ind l)
+
+@[csimp] theorem List.toArray_eq_mk : @toArray = @toArrayTR := by
+  apply funext ; intro α
+  apply funext ; intro l
+  unfold toArrayTR
+  unfold Array.mkEmpty
+  rw [toArrayAux_eq_mk, List.append]
+
 /-! # Relations -/
 
 /--

src/Init/Data/Array/BasicAux.lean

@@ -32,11 +32,6 @@ private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Arra
     have := Array.of_push_eq_push ih₂
     simp [this]
 
-@[simp] theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs) := by
-  apply propext; apply Iff.intro
-  · intro h; simp [toArray] at h; have := of_toArrayAux_eq_toArrayAux h rfl; exact this.1
-  · intro h; rw [h]
-
 def Array.mapM' [Monad m] (f : α → m β) (as : Array α) : m { bs : Array β // bs.size = as.size } :=
   go 0 ⟨mkEmpty as.size, rfl⟩ (by simp_arith)
 where

src/Init/Data/List/Basic.lean

@@ -77,56 +77,14 @@ theorem length_add_eq_lengthTRAux (as : List α) (n : Nat) : as.length + n = as.
 @[simp] theorem length_nil : length ([] : List α) = 0 :=
   rfl
 
-/-- Auxiliary for `List.reverse`. `List.reverseAux l r = l.reverse ++ r`, but it is defined directly. -/
-def reverseAux : List α → List α → List α
-  | [],   r => r
-  | a::l, r => reverseAux l (a::r)
-
-/--
-`O(|as|)`. Reverse of a list:
-* `[1, 2, 3, 4].reverse = [4, 3, 2, 1]`
-
-Note that because of the "functional but in place" optimization implemented by Lean's compiler,
-this function works without any allocations provided that the input list is unshared:
-it simply walks the linked list and reverses all the node pointers.
--/
-def reverse (as : List α) : List α :=
-  reverseAux as []
-
 theorem reverseAux_reverseAux_nil (as bs : List α) : reverseAux (reverseAux as bs) [] = reverseAux bs as := by
   induction as generalizing bs with
   | nil => rfl
   | cons a as ih => simp [reverseAux, ih]
 
-theorem reverseAux_reverseAux (as bs cs : List α) : reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs) := by
-  induction as generalizing bs cs with
-  | nil => rfl
-  | cons a as ih => simp [reverseAux, ih (a::bs), ih [a]]
-
 @[simp] theorem reverse_reverse (as : List α) : as.reverse.reverse = as := by
   simp [reverse]; rw [reverseAux_reverseAux_nil]; rfl
 
-/--
-`O(|xs|)`: append two lists. `[1, 2, 3] ++ [4, 5] = [1, 2, 3, 4, 5]`.
-It takes time proportional to the first list.
--/
-protected def append : (xs ys : List α) → List α
-  | [],    bs => bs
-  | a::as, bs => a :: List.append as bs
-
-/-- Tail-recursive version of `List.append`. -/
-def appendTR (as bs : List α) : List α :=
-  reverseAux as.reverse bs
-
-@[csimp] theorem append_eq_appendTR : @List.append = @appendTR := by
-  apply funext; intro α; apply funext; intro as; apply funext; intro bs
-  simp [appendTR, reverse]
-  induction as with
-  | nil  => rfl
-  | cons a as ih =>
-    rw [reverseAux, reverseAux_reverseAux]
-    simp [List.append, ih, reverseAux]
-
 instance : Append (List α) := ⟨List.append⟩
 
 @[simp] theorem nil_append (as : List α) : [] ++ as = as := rfl

src/Init/Prelude.lean

@@ -2713,25 +2713,6 @@ def Array.extract (as : Array α) (start stop : Nat) : Array α :=
   let sz' := Nat.sub (min stop as.size) start
   loop sz' start (mkEmpty sz')
 
-/-- Auxiliary definition for `List.toArray`. -/
-@[inline_if_reduce]
-def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
-
-/-- A non-tail-recursive version of `List.length`, used for `List.toArray`. -/
-@[inline_if_reduce]
-def List.redLength : List α → Nat
-  | nil       => 0
-  | cons _ as => as.redLength.succ
-
-/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
--- This function is exported to C, where it is called by `Array.mk`
--- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
-def List.toArray (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.redLength)
-
 /-- The typeclass which supplies the `>>=` "bind" function. See `Monad`. -/
 class Bind (m : Type u → Type v) where
   /-- If `x : m α` and `f : α → m β`, then `x >>= f : m β` represents the

tests/lean/csimpAttrToArray.lean

@@ -0,0 +1,3 @@
+set_option trace.compiler.ir.init true
+def f (as : List Nat) : Array Nat :=
+  as.toArray

tests/lean/csimpAttrToArray.lean.expected.out

@@ -0,0 +1,7 @@
+
+[init]
+def f (x_1 : obj) : obj :=
+  let x_2 : obj := List.redLength._rarg x_1;
+  let x_3 : obj := Array.mkEmpty ◾ x_2;
+  let x_4 : obj := List.toArrayAux._rarg x_1 x_3;
+  ret x_4