chore: move to v4.6.0-rc1, merging adaptations (leanprover-community#576

)

* feat: hover info for `rcases h : ...` (leanprover-community#486)

* feat: hover info for `rcases h : ...`

* fix

* chore: adaptations for leanprover/lean4#3123 (leanprover-community#502)

* chore: adaptations for leanprover/lean4#3123

* update toolchain

* chore: remove unnecessary `have` (leanprover-community#516)

After leanprover/lean4#3132 the linter will complain about this.

* chore: simproc PR changes (leanprover-community#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <[email protected]>

* chore: adaptions for nightly-2023-01-11 (leanprover-community#524)

* advance toolchain to nightly-2024-01-12, no updates required

* chore: updates to DiscrTree for changes in nightly (leanprover-community#536)

* doc: extend docstrings for `ext` and `ext1` (leanprover-community#525)

Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`.

* docs(Data/List): typo (leanprover-community#529)

* feat: Eq.rec lemma (leanprover-community#385)

* chore: Add empty collection instance to BinomialHeap (leanprover-community#532)

* Incremental Library Search (leanprover-community#421)

This ports library_search from Mathlib to Std.  It preserves the ability to do caching, but is designed to support a cacheless mode.  The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed.

Co-authored-by: Scott Morrison <[email protected]>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Martin Dvořák <[email protected]>
Co-authored-by: François G. Dorais <[email protected]>
Co-authored-by: Joe Hendrix <[email protected]>

* feat: adaptations for leanprover/lean4#3159 (leanprover-community#557)

* merge origin/main

* chore: fixes for `simp` refactor (leanprover-community#571)

* move to v4.6.0-rc1

* fix proofs

---------

Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: Leonardo de Moura <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Martin Dvořák <[email protected]>
Co-authored-by: François G. Dorais <[email protected]>
Co-authored-by: Joe Hendrix <[email protected]>

Std/CodeAction/Basic.lean

@@ -147,7 +147,7 @@ partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
   (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
     Option (ContextInfo × InfoTree) :=
   match t with
-  | .context ctx t => findInfoTree? kind tgtRange ctx t f canonicalOnly
+  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
   | node@(.node i ts) => do
     if let some ctx := ctx? then
       if let some range := i.stx.getRange? canonicalOnly then

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

@@ -152,7 +152,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)
@@ -262,9 +262,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/ByteArray.lean

@@ -133,12 +133,12 @@ def ofFn (f : Fin n → UInt8) : ByteArray where
 private def ofFnAux (f : Fin n → UInt8) : ByteArray := go 0 (mkEmpty n) where
   go (i : Nat) (acc : ByteArray) : ByteArray :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by _ => n - i
+termination_by n - i
 
 @[csimp] private theorem ofFn_eq_ofFnAux : @ofFn = @ofFnAux := by
   funext n f; ext; simp [ofFnAux, Array.ofFn, ofFnAux_data, mkEmpty]
 where
   ofFnAux_data {n} (f : Fin n → UInt8) (i) {acc} :
       (ofFnAux.go f i acc).data = Array.ofFn.go f i acc.data := by
     rw [ofFnAux.go, Array.ofFn.go]; split; rw [ofFnAux_data f (i+1), push_data]; rfl
-  termination_by _ => n - i
+  termination_by n - i

Std/Data/Fin/Basic.lean

@@ -60,7 +60,7 @@ def list (n) : List (Fin n) := (enum n).data
   /-- 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

@@ -680,7 +680,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)
@@ -802,24 +802,24 @@ theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list
 @[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
     Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HAdd.hAdd, Add.add, Fin.add]
+  simp [Fin.ofNat', Fin.add_def]
 
 @[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
     x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HAdd.hAdd, Add.add, Fin.add]
+  simp [Fin.ofNat', Fin.add_def]
 
 /-! ### sub -/
 
 @[simp] theorem ofNat'_sub (x : Nat) (lt : 0 < n) (y : Fin n) :
     Fin.ofNat' x lt - y = Fin.ofNat' (x + (n - y.val)) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HSub.hSub, Sub.sub, Fin.sub]
+  simp [Fin.ofNat', Fin.sub_def]
 
 @[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
     x - Fin.ofNat' y lt = Fin.ofNat' (x.val + (n - y % n)) lt := by
   apply Fin.eq_of_val_eq
-  simp [Fin.ofNat', HSub.hSub, Sub.sub, Fin.sub]
+  simp [Fin.ofNat', Fin.sub_def]
 
 /-! ### mul -/
 

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

@@ -128,7 +128,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

@@ -91,7 +91,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.
@@ -112,7 +112,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/Delaborator.lean

@@ -7,36 +7,6 @@ import Lean.PrettyPrinter
 
 open Lean PrettyPrinter Delaborator SubExpr
 
-/--
-This is similar to `withAppFnArgs` but it handles construction of an "over-application".
-For example, suppose we want to implement a delaborator for applications of `f : Foo A → A`
-like `f x` as `F[x]`, but because `A` is a type variable we might encounter a term of the form
-`@f (A → B) x y` which has an additional argument `y`.
-
-Most of the built in delaborators will deliberately fail on such an example, resulting in
-delaborated syntax `f x y`, but this combinator can be used if we want to display `F[x] y`
-instead.
-
-* `arity`: the expected number of arguments to `f`.
-  The combinator will fail if fewer than this number of arguments are passed
-* `x`: constructs data corresponding to the main application (`f x` in the example)
--/
-def Lean.PrettyPrinter.Delaborator.withOverApp (arity : Nat) (x : Delab) : Delab := do
-  let n := (← getExpr).getAppNumArgs
-  guard (n ≥ arity)
-  let kinds ← getParamKinds
-  let rec
-  /-- Inner loop of `withOverApp`. -/
-  loop : Nat → DelabM (Term × Array Term)
-  | 0 => return (← x, #[])
-  | n+1 => do
-    let mut (fnStx, args) ← withAppFn (loop n)
-    if kinds.get? (n + arity) |>.all (·.bInfo.isExplicit) then
-      args := args.push (← withAppArg delab)
-    pure (fnStx, args)
-  let (fnStx, argStxs) ← loop (n - arity)
-  return Syntax.mkApp fnStx argStxs
-
 /-- Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first
 argument is implicit, which is what the default `toMessageData` for `Expr` does.

Std/Lean/InfoTree.lean

@@ -14,7 +14,7 @@ partial def InfoTree.foldInfo' (init : α) (f : ContextInfo → InfoTree → α
 where
   /-- `foldInfo'.go` is like `foldInfo'` but with an additional outer context parameter `ctx?`. -/
   go ctx? a
-  | context ctx t => go ctx a t
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
   | t@(node i ts) =>
     let a := match ctx? with
       | none => a

Std/Lean/Meta/Basic.lean

@@ -407,7 +407,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,