refactor: Adjust to new termination_by syntax

Std/Data/Array/Init/Basic.lean

@@ -29,7 +29,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by _ => n - i
+termination_by n - i
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=

Std/Data/Array/Init/Lemmas.lean

@@ -151,7 +151,7 @@ where
     · rw [← List.get_drop_eq_drop _ i ‹_›]
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
-termination_by aux => arr.size - i
+  termination_by arr.size - i
 
 theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
     (motive : Nat → Prop) (h0 : motive 0)
@@ -261,9 +261,9 @@ theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Arra
         | true, h => .pure h
         | false, h => go hj hstop h hp
     · next hj => exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0
+    termination_by stop - j
   simp only [Array.anyM_eq_anyM_loop]
   exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..
-termination_by go => stop - j
 
 theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
     (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)

Std/Data/Array/Lemmas.lean

@@ -276,8 +276,8 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
       have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
+    termination_by j - i
   simp only [reverse]; split <;> simp [go]
-termination_by _ => j - i
 
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   unfold range
@@ -323,14 +323,14 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
         cases Nat.le_antisymm h₂.1 h₂.2
         exact (List.get?_reverse' _ _ h).symm
       · rfl
+    termination_by j - i
   simp only [reverse]; split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
     refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
     split; {rfl}; rename_i h
     simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
     rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
-termination_by _ => j - i
 
 @[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
     (ofFn.go f i acc).size = acc.size + (n - i) := by
@@ -343,7 +343,7 @@ termination_by _ => j - i
     have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
     unfold ofFn.go
     simp [hin, this]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
 
@@ -363,7 +363,7 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     | inr hj => simp [get_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
@@ -427,8 +427,8 @@ theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Arr
         ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
         List.zipWith f (List.drop i as.data) (List.drop i bs.data)
       simp only [List.get_cons_drop]
+    termination_by as.size - i
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
-termination_by loop i _ _ _ => as.size - i
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by

Std/Data/Array/Match.lean

@@ -45,7 +45,7 @@ def PrefixTable.step [BEq α] (t : PrefixTable α) (x : α) : Fin (t.size+1) →
         ⟨k+1, Nat.succ_lt_succ hsz⟩
       else cont ()
     else cont ()
-termination_by _ k => k.val
+termination_by k => k.val
 
 /-- Extend a prefix table by one element
 

Std/Data/Array/Merge.lean

@@ -40,7 +40,7 @@ where
         have : xs.size + ys.size - (i + j + 1) < xs.size + ys.size - (i + j) :=
           Nat.sub_succ_lt_self _ _ hij
         go (acc.push y) i (j + 1)
-termination_by go => xs.size + ys.size - (i + j)
+  termination_by xs.size + ys.size - (i + j)
 
 /--
 Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -83,7 +83,7 @@ where
           rw [show i + j + 2 = (i + 1) + (j + 1) by simp_arith]
           exact Nat.add_le_add hi hj
         go (acc.push (merge x y)) (i + 1) (j + 1)
-termination_by go => xs.size + ys.size - (i + j)
+    termination_by xs.size + ys.size - (i + j)
 
 /--
 Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
@@ -130,7 +130,7 @@ where
         go (acc.push hd) (i + 1) x
     else
       acc.push hd
-termination_by _ i _ => xs.size - i
+  termination_by xs.size - i
 
 /--
 Deduplicate a sorted array. The array must be sorted with to an order which

Std/Data/BinomialHeap/Basic.lean

@@ -140,7 +140,7 @@ by rank and `merge` maintains this invariant.
       else if t₂.rankGT r
         then merge le t₁ (.cons r a n t₂)
         else .cons r a n (merge le t₁ t₂)
-termination_by _ s₁ s₂ => s₁.length + s₂.length
+termination_by s₁ s₂ => s₁.length + s₂.length
 
 /--
 `O(log n)`. Convert a `HeapNode` to a `Heap` by reversing the order of the nodes
@@ -219,7 +219,7 @@ theorem Heap.realSize_merge (le) (s₁ s₂ : Heap α) :
       rw [combine] at eq; split at eq <;> cases eq <;>
         simp [Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
     split <;> split <;> simp [IH₁, IH₂, IH₃, this, Nat.add_assoc, Nat.add_left_comm]
-termination_by _ => s₁.length + s₂.length
+termination_by s₁.length + s₂.length
 
 private def FindMin.HasSize (res : FindMin α) (n : Nat) : Prop :=
   ∃ m,
@@ -280,7 +280,7 @@ by repeatedly pulling the minimum element out of the heap.
   | some (hd, tl) => do
     have : tl.realSize < s.realSize := by simp_arith [Heap.realSize_deleteMin eq]
     foldM le tl (← f init hd) f
-termination_by _ => s.realSize
+termination_by s.realSize
 
 /--
 `O(n log n)`. Fold over the elements of a heap in increasing order,
@@ -402,7 +402,7 @@ theorem Heap.WF.merge' (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) :
     · let ⟨ih₁, ih₂⟩ := merge' ht₁ ht₂
       exact ⟨⟨Nat.le_succ_of_le hr₁, this, ih₁.of_rankGT (ih₂ (iff_of_false hl₁ hl₂))⟩,
         fun _ => Nat.lt_succ_of_le hr₁⟩
-termination_by _ => s₁.length + s₂.length
+termination_by s₁.length + s₂.length
 
 theorem Heap.WF.merge (h₁ : s₁.WF le n) (h₂ : s₂.WF le n) : (merge le s₁ s₂).WF le n :=
   (merge' h₁ h₂).1

Std/Data/Fin/Basic.lean

@@ -54,7 +54,7 @@ def clamp (n m : Nat) : Fin (m + 1) := ⟨min n m, Nat.lt_succ_of_le (Nat.min_le
   /-- Inner loop for `Fin.foldl`. `Fin.foldl.loop n f x i = f (f (f x i) ...) (n-1)`  -/
   loop (x : α) (i : Nat) : α :=
     if h : i < n then loop (f x ⟨i, h⟩) (i+1) else x
-termination_by loop i => n - i
+  termination_by n - i
 
 /-- Folds over `Fin n` from the right: `foldr 3 f x = f 0 (f 1 (f 2 x))`. -/
 @[inline] def foldr (n) (f : Fin n → α → α) (init : α) : α := loop ⟨n, Nat.le_refl n⟩ init where

Std/Data/Fin/Iterate.lean

@@ -21,7 +21,7 @@ def hIterateFrom (P : Nat → Sort _) {n} (f : ∀(i : Fin n), P i.val → P (i.
   else
     have p : i = n := (or_iff_left g).mp (Nat.eq_or_lt_of_le ubnd)
     cast (congrArg P p) a
-  termination_by hIterateFrom i _ _ => n - i
+  termination_by n - i
 
 /--
 `hIterate` is a heterogenous iterative operation that applies a

Std/Data/Fin/Lemmas.lean

@@ -673,7 +673,7 @@ and `cast` defines the inductive step using `motive i.succ`, inducting downwards
   else
     let j : Fin n := ⟨i, Nat.lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩
     cast _ (reverseInduction last cast j.succ)
-termination_by _ => n + 1 - i
+termination_by n + 1 - i
 decreasing_by decreasing_with
   -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
   exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)

Std/Data/HashMap/Basic.lean

@@ -151,7 +151,7 @@ where
       let target := es.foldl reinsertAux target
       go (i+1) source target
     else target
-termination_by _ i source _ => source.size - i
+  termination_by source.size - i
 
 /--
 Inserts key-value pair `a, b` into the map.

Std/Data/HashMap/WF.lean

@@ -108,7 +108,7 @@ where
       simp
       have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm
       rwa [List.getD_eq_get?, List.get?_eq_get, Option.getD_some] at this
-termination_by go i source _ _ => source.size - i
+  termination_by source.size - i
 
 theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α × β)} {i : Nat}
     (hl₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], l.Pairwise fun a b => ¬(a.1 == b.1))
@@ -170,7 +170,7 @@ where
           refine ⟨Nat.le_of_lt this, fun _ h h' => Nat.ne_of_lt this ?_⟩
           exact LawfulHashable.hash_eq h' ▸ hs₂ _ H _ h
     · exact ht.1
-termination_by go i source _ _ _ _ => source.size - i
+  termination_by source.size - i
 
 theorem insert_size [BEq α] [Hashable α] {m : Imp α β} {k v}
     (h : m.size = m.buckets.size) :

Std/Data/Nat/Basic.lean

@@ -125,7 +125,7 @@ where
       iter n next
     else
       guess
-termination_by iter guess => guess
+  termination_by guess
 
 /-!
 ### testBit

Std/Data/PairingHeap.lean

@@ -173,7 +173,7 @@ by repeatedly pulling the minimum element out of the heap.
   | some (hd, tl) =>
     have : tl.size < s.size := by simp_arith [Heap.size_deleteMin_lt eq]
     do foldM le tl (← f init hd) f
-termination_by _ => s.size
+termination_by s.size
 
 /--
 `O(n log n)`. Fold over the elements of a heap in increasing order,

Std/Data/RBMap/Basic.lean

@@ -360,7 +360,7 @@ def append : RBNode α → RBNode α → RBNode α
     | bc               => balLeft a x (node black bc y d)
   | a@(node black ..), node red b x c => node red (append a b) x c
   | node red a x b, c@(node black ..) => node red a x (append b c)
-termination_by _ x y => x.size + y.size
+termination_by x y => x.size + y.size
 
 /-! ## erase -/
 

Std/Data/RBMap/WF.lean

@@ -308,7 +308,7 @@ protected theorem All.append (hl : l.All p) (hr : r.All p) : (append l r).All p
     have := hb.append hc; split <;> simp_all [All.balLeft]
   · simp_all [hl.append hr.2.1]
   · simp_all [hl.2.2.append hr]
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-- The `append` function preserves the ordering invariants. -/
 protected theorem Ordered.append {l : RBNode α} {v : α} {r : RBNode α}
@@ -341,7 +341,7 @@ protected theorem Ordered.append {l : RBNode α} {v : α} {r : RBNode α}
     exact ⟨(vx.trans_r lv).append bx, yc, hl.append lv vb hb, hc⟩
   · have ⟨xv, _, bv⟩ := lv; have ⟨ax, xb, ha, hb⟩ := hl
     exact ⟨ax, xb.append (xv.trans_l vr), ha, hb.append bv vr hr⟩
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-- The balance properties of the `append` function. -/
 protected theorem Balanced.append {l r : RBNode α}
@@ -380,7 +380,7 @@ protected theorem Balanced.append {l r : RBNode α}
   · have .red ha hb := hl; have IH := hb.append hr
     have .black hc hd := hr; have ⟨c, IH⟩ := IH.of_false (· rfl rfl)
     exact .redred (fun.) ha IH
-termination_by _ => l.size + r.size
+termination_by l.size + r.size
 
 /-! ## erase -/
 

Std/Data/String/Basic.lean

@@ -93,7 +93,7 @@ where
         spos
     else
       spos
-termination_by loop => s.stopPos.byteIdx - spos.byteIdx
+  termination_by s.stopPos.byteIdx - spos.byteIdx
 
 /--
 Returns the longest common suffix of two substrings.
@@ -114,7 +114,7 @@ where
         spos
     else
       spos
-termination_by loop => spos.byteIdx
+  termination_by spos.byteIdx
 
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.

Std/Lean/Meta/Basic.lean

@@ -405,7 +405,7 @@ where
         match ← observing? (f g) with
         | some gs' => go n true gs' (gs::stk) acc
         | none => go n p gs stk (acc.push g)
-termination_by _ n p gs stk _ => (n, stk, gs)
+termination_by n p gs stk _ => (n, stk, gs)
 
 /--
 `repeat' f` runs `f` on all of the goals to produce a new list of goals,

Std/Tactic/RCases.lean

@@ -310,7 +310,7 @@ def processConstructor (ref : Syntax) (info : Array ParamInfo)
       | [p] => ([p.name?.getD `_], [p])
       | ps  => ([`_], [(bif explicit then .explicit ref else id) (.tuple ref ps)])
   else ([], [])
-termination_by _ => info.size - idx
+termination_by info.size - idx
 
 /--
 Takes a list of constructor names, and an (alternation) list of patterns, and matches each

Std/WF.lean

@@ -51,7 +51,7 @@ instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (intro x h))
     {a : α} (t : Acc r a) : motive a t :=
   intro a (fun x h => t.inv h) (fun y hr => recC intro (t.inv hr))
-termination_by _ a h => Subtype.mk a h
+termination_by Subtype.mk a t
 
 private theorem recC_intro {motive : (a : α) → Acc r a → Sort v}
     (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
@@ -97,7 +97,7 @@ than the one inferred by default:
 ```
 def otherWF : WellFounded Nat := …
 def foo (n : Nat) := …
-termination_by foo n => otherWF.wrap n
+termination_by otherWF.wrap n
 ```
 -/
 def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x} :=
@@ -118,7 +118,7 @@ Workaround until Lean has native support for this. -/
 @[specialize] private def fixC {α : Sort u} {C : α → Sort v} {r : α → α → Prop}
     (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
   F x (fun y _ => fixC hwf F y)
-termination_by _ x => hwf.wrap x
+termination_by hwf.wrap x
 
 @[csimp] private theorem fix_eq_fixC : @fix = @fixC := rfl
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-03
+leanprover/lean4-pr-releases:pr-release-3040