From 34bbe5d12cfaa4e9df2ecd9d54c062843aeea9c6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 May 2022 18:13:32 -0700
Subject: [PATCH] =?UTF-8?q?feat:=20add=20`simp`=20theorem=20`List.of=5FtoA?=
 =?UTF-8?q?rray=5Feq=5FtoArray=20(as=20bs=20:=20List=20=CE=B1)=20:=20(as.t?=
 =?UTF-8?q?oArray=20=3D=20bs.toArray)=20=3D=20(as=20=3D=20bs)=20:=3D=20by`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Init/Data/Array.lean          |  1 +
 src/Init/Data/Array/BasicAux.lean | 38 +++++++++++++++++++++++++++++++
 src/Init/Data/List/Basic.lean     |  9 ++++++++
 tests/lean/run/toArrayEq.lean     | 12 ++++++++++
 4 files changed, 60 insertions(+)
 create mode 100644 src/Init/Data/Array/BasicAux.lean
 create mode 100644 tests/lean/run/toArrayEq.lean

diff --git a/src/Init/Data/Array.lean b/src/Init/Data/Array.lean
index d26bc11b7a..d478edb9a1 100644
--- a/src/Init/Data/Array.lean
+++ b/src/Init/Data/Array.lean
@@ -10,3 +10,4 @@ import Init.Data.Array.BinSearch
 import Init.Data.Array.InsertionSort
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Mem
+import Init.Data.Array.BasicAux
diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
new file mode 100644
index 0000000000..052c003bb7
--- /dev/null
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Array.Basic
+import Init.Data.Nat.Linear
+import Init.NotationExtra
+
+theorem Array.of_push_eq_push {as bs : Array α} (h : as.push a = bs.push b) : as = bs ∧ a = b := by
+  simp [push] at h
+  have ⟨h₁, h₂⟩ := List.of_concat_eq_concat h
+  cases as; cases bs
+  simp_all
+
+private theorem List.size_toArrayAux (as : List α) (bs : Array α) : (as.toArrayAux bs).size = as.length + bs.size := by
+  induction as generalizing bs with
+  | nil => simp [toArrayAux]
+  | cons a as ih => simp_arith [toArrayAux, *]
+
+private theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Array α} (h : as.toArrayAux cs = bs.toArrayAux ds) (hlen : cs.size = ds.size) : as = bs ∧ cs = ds := by
+  match as, bs with
+  | [], []    => simp [toArrayAux] at h; simp [h]
+  | a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp_arith [size_toArrayAux] at hlen
+  | [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp_arith [size_toArrayAux] at hlen
+  | a::as, b::bs =>
+    simp [toArrayAux] at h
+    have : (cs.push a).size = (ds.push b).size := by simp [*]
+    have ⟨ih₁, ih₂⟩ := of_toArrayAux_eq_toArrayAux h this
+    simp [ih₁]
+    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]
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 15a629676e..96888e478a 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -531,4 +531,13 @@ instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
     | nil => rfl
     | cons a as ih => simp [BEq.beq, List.beq, LawfulBEq.rfl]; exact ih
 
+theorem of_concat_eq_concat {as bs : List α} {a b : α} (h : as.concat a = bs.concat b) : as = bs ∧ a = b := by
+  match as, bs with
+  | [], [] => simp [concat] at h; simp [h]
+  | [_], [] => simp [concat] at h
+  | _::_::_, [] => simp [concat] at h
+  | [], [_] => simp [concat] at h
+  | [], _::_::_ => simp [concat] at h
+  | _::_, _::_ => simp [concat] at h; simp [h]; apply of_concat_eq_concat h.2
+
 end List
diff --git a/tests/lean/run/toArrayEq.lean b/tests/lean/run/toArrayEq.lean
new file mode 100644
index 0000000000..26d40ebceb
--- /dev/null
+++ b/tests/lean/run/toArrayEq.lean
@@ -0,0 +1,12 @@
+inductive Foo
+  | foo : Nat → Foo
+  | foos : Array Foo → Foo
+  deriving BEq
+
+example : Foo.foo 0 ≠ Foo.foo 1 := by simp
+
+example : #[0] ≠ #[1] := by simp
+
+example : #[Foo.foo 0] ≠ #[Foo.foo 1] := by simp
+
+example : Foo.foos #[.foo 0] ≠ Foo.foos #[.foo 1] := by simp