From 2a9261d1ba962deff9fcc1784be44563af513af5 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 10 Oct 2025 00:30:19 +0200
Subject: Lean 4.18

---
 Common/List.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'Common/List.lean')

diff --git a/Common/List.lean b/Common/List.lean
index 704f8b2..1c8f4a6 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -10,19 +10,20 @@ theorem listFilterSmallerOrEqualList (l : List α) (p : α → Bool) : l.length
       simp
       constructor
       assumption
-    | true => simp_arith[hi]
+    | true => simp[hi]
 
 def quicksortBy {α : Type} (pred : α → α → Bool): List α → List α
 | [] => []
 | a :: as =>
   let smallerPred := λ b ↦ pred b a
   let largerEqualPred := not ∘ smallerPred
-  have : List.length (List.filter smallerPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList]
-  have : List.length (List.filter largerEqualPred as) < Nat.succ (List.length as) := by simp_arith[listFilterSmallerOrEqualList]
   let smallers := as.filter smallerPred
   let biggers := as.filter largerEqualPred
   (quicksortBy pred smallers) ++ [a] ++ (quicksortBy pred biggers)
   termination_by l => l.length
+  decreasing_by
+    all_goals
+      simp +arith only [unattach_filter, unattach_attach, length_cons, gt_iff_lt, listFilterSmallerOrEqualList]
 
 def quicksort {α : Type} [Ord α] : List α → List α := quicksortBy λ a b ↦ Ord.compare a b == Ordering.lt
 
@@ -86,7 +87,7 @@ protected theorem length_mapWithProof_Aux {α : Type u} {β : Type v} (list : Li
   case cons l ls hi =>
     unfold mapWithProof.worker
     have hi := hi (λe h ↦ f e (mem_cons_of_mem _ h)) (f l (mem_cons_self _ _) :: acc)
-    simp_arith[←hi]
+    simp +arith[←hi]
 
 theorem length_mapWithProof {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list.length = (list.mapWithProof f).length :=
   List.length_mapWithProof_Aux list f []
@@ -95,8 +96,8 @@ theorem mapWithProof_nil {α : Type u} {β : Type v} {f : (e : α) → (e ∈ []
 
 theorem mapWithProof_neNilIffNeNil {α : Type u} {β : Type v} {list : List α} {f : (e : α) → (e ∈ list) → β} : list ≠ [] ↔ (list.mapWithProof f) ≠ [] :=
   ⟨
-    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.subst (List.length_pos.mpr h₁),
-    λh₁ ↦ List.length_pos.mp $ length_mapWithProof.substr (List.length_pos.mpr h₁)
+    λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.subst (List.length_pos_iff.mpr h₁),
+    λh₁ ↦ List.length_pos_iff.mp $ length_mapWithProof.substr (List.length_pos_iff.mpr h₁)
   ⟩
 
 theorem map_ne_nil {α : Type u} {β : Type v} {list : List α} {f : α → β} : list ≠ [] ↔ list.map f ≠ [] :=
-- 
cgit v1.2.3

