From cfb4e306f730357bcb7ce7f5e2e59a9d25b4a06e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Apr 2022 16:44:24 -0700
Subject: [PATCH] refactor: replace `length_dropLast` theorem

---
 doc/examples/palindromes.lean  | 4 +---
 src/Init/Data/Array/Basic.lean | 6 ++++--
 src/Init/Data/List/Basic.lean  | 8 +++-----
 3 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/doc/examples/palindromes.lean b/doc/examples/palindromes.lean
index 5548ac9f7d..02f06c3b2c 100644
--- a/doc/examples/palindromes.lean
+++ b/doc/examples/palindromes.lean
@@ -81,12 +81,10 @@ theorem List.palindrome_ind (motive : List α → Prop)
   | []  => h₁
   | [a] => h₂ a
   | a₁::a₂::as' =>
-    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     have ih := palindrome_ind motive h₁ h₂ h₃ (a₂::as').dropLast
+    have : [a₁] ++ (a₂::as').dropLast ++ [(a₂::as').last (by simp)] = a₁::a₂::as' := by simp
     this ▸ h₃ _ _ _ ih
 termination_by _ as => as.length
--- TODO: remove the following tactic after we add `linarith`
-decreasing_by simp_wf; rw [Nat.succ_sub_succ, Nat.sub_zero]; simp_arith
 
 /-|
 We use our new induction principle to prove that if `as.reverse = as`, then `Palindrome as` holds.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index e75faae253..8c737a95e8 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -628,8 +628,10 @@ def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
   rw [size_set, size_set]
 
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 :=
-  List.length_dropLast ..
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub]
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index d8dfa8fe54..15a629676e 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -485,14 +485,12 @@ def dropLast {α} : List α → List α
     | zero => rfl
     | succ i => simp [set, ih]
 
-@[simp] theorem length_dropLast (as : List α) : as.dropLast.length = as.length - 1 := by
+@[simp] theorem length_dropLast_cons (a : α) (as : List α) : (a :: as).dropLast.length = as.length := by
   match as with
   | []       => rfl
-  | [a]      => rfl
-  | a::b::as =>
-    have ih := length_dropLast (b::as)
+  | b::bs =>
+    have ih := length_dropLast_cons b bs
     simp[dropLast, ih]
-    rfl
 
 @[simp] theorem length_append (as bs : List α) : (as ++ bs).length = as.length + bs.length := by
   induction as with