From a115150d90f46ce1414efed32070e3e0aa829938 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 17:46:07 +0000 Subject: [PATCH 01/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 80fc5080d..d9b09f15a 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2026-08-11 +leanprover/lean4-pr-releases:pr-release-14844-4853259 From 7572f5bd875295efc4df1f279a9c5256c57a8ca3 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 18:19:07 +0000 Subject: [PATCH 02/20] reimplement filterDiscrTreeM in terms of upstream mapArraysM --- aesop/Aesop/Util/Basic.lean | 48 +++++++++++-------------------------- 1 file changed, 14 insertions(+), 34 deletions(-) diff --git a/aesop/Aesop/Util/Basic.lean b/aesop/Aesop/Util/Basic.lean index 2961f0f7d..9432dec68 100644 --- a/aesop/Aesop/Util/Basic.lean +++ b/aesop/Aesop/Util/Basic.lean @@ -72,30 +72,9 @@ def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) := -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they -- turn into `Key.star`) but not fvars. -def isEmptyTrie : Trie α → Bool - | .node vs children => vs.isEmpty && children.isEmpty - -@[specialize] -private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ) - (p : α → m (ULift Bool)) (init : σ) : Trie α → m (Trie α × σ) - | .node vs children => do - let (vs, acc) ← vs.foldlM (init := (#[], init)) λ (vs, acc) v => do - if (← p v).down then - return (vs.push v, acc) - else - return (vs, ← f acc v) - let (children, acc) ← go acc 0 children - let children := children.filter λ (_, c) => ! isEmptyTrie c - return (.node vs children, acc) - where - go (acc : σ) (i : Nat) (children : Array (Key × Trie α)) : - m (Array (Key × Trie α) × σ) := do - if h : i < children.size then - let (key, t) := children[i]'h - let (t, acc) ← filterTrieM f p acc t - go acc (i + 1) (children.set i (key, t)) - else - return (children, acc) +@[deprecated Trie.isEmptyNode (since := "2026-08-19")] +def isEmptyTrie (t : Trie α) := + t.isEmptyNode /-- Remove elements for which `p` returns `false` from the given `DiscrTree`. @@ -103,16 +82,17 @@ The removed elements are monadically folded over using `f` and `init`, so `f` is called once for each removed element and the final state of type `σ` is returned. -/ -@[specialize] -def filterDiscrTreeM [Monad m] [Inhabited σ] (p : α → m (ULift Bool)) +@[inline] +def filterDiscrTreeM [Monad m] (p : α → m Bool) (f : σ → α → m σ) (init : σ) (t : DiscrTree α) : - m (DiscrTree α × σ) := do - let (root, acc) ← - t.root.foldlM (init := (.empty, init)) λ (root, acc) key t => do - let (t, acc) ← filterTrieM f p acc t - let root := if isEmptyTrie t then root else root.insert key t - return (root, acc) - return (⟨root⟩, acc) + m (DiscrTree α × σ) := + StateT.run (s := init) do + t.mapArraysM (·.filterMapM (fun v => do + if ← p v then + return .some v + else + set (← f (← get) v) + return .none)) /-- Remove elements for which `p` returns `false` from the given `DiscrTree`. @@ -121,7 +101,7 @@ once for each removed element and the final state of type `σ` is returned. -/ def filterDiscrTree [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ) (t : DiscrTree α) : DiscrTree α × σ := Id.run $ - filterDiscrTreeM (λ a => pure ⟨p a⟩) (λ s a => pure (f s a)) init t + filterDiscrTreeM (λ a => pure (p a)) (λ s a => pure (f s a)) init t end DiscrTree From 34bb0ce573895c6687b802f7fad9a9b8d029bc9c Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 19:25:16 +0000 Subject: [PATCH 03/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index d9b09f15a..bdf620ced 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-4853259 +leanprover/lean4-pr-releases:pr-release-14844-7b84a7f From 3cd2bfb13623675333c3ffeddf34a786f0d41a93 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 19:36:33 +0000 Subject: [PATCH 04/20] Add inline annotations, remove inhabited constraint --- aesop/Aesop/Util/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/aesop/Aesop/Util/Basic.lean b/aesop/Aesop/Util/Basic.lean index 9432dec68..ee12220f8 100644 --- a/aesop/Aesop/Util/Basic.lean +++ b/aesop/Aesop/Util/Basic.lean @@ -99,7 +99,8 @@ Remove elements for which `p` returns `false` from the given `DiscrTree`. The removed elements are folded over using `f` and `init`, so `f` is called once for each removed element and the final state of type `σ` is returned. -/ -def filterDiscrTree [Inhabited σ] (p : α → Bool) (f : σ → α → σ) (init : σ) +@[inline] +def filterDiscrTree (p : α → Bool) (f : σ → α → σ) (init : σ) (t : DiscrTree α) : DiscrTree α × σ := Id.run $ filterDiscrTreeM (λ a => pure (p a)) (λ s a => pure (f s a)) init t From a81f4b8d8ae2291ed1a844c687b94ada127bfbd6 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 19:44:50 +0000 Subject: [PATCH 05/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index bdf620ced..9797f55d7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-7b84a7f +leanprover/lean4-pr-releases:pr-release-14844-f1ca8f9 From d5075a295dad68d5e4b146653ffb2b0d39cccd62 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 20:18:40 +0000 Subject: [PATCH 06/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 9797f55d7..1a9e727d2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-f1ca8f9 +leanprover/lean4-pr-releases:pr-release-14844-a2d16ea From 0820e8a46eda83535b91ac49e54acd06be7fc153 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Mon, 17 Aug 2026 21:20:51 +0000 Subject: [PATCH 07/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 1a9e727d2..289901bee 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14844-a2d16ea +leanprover/lean4-pr-releases:pr-release-14805-3048b87 From 7e67b5e78ac7700a24bf58e6960729fe5aebed19 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Tue, 18 Aug 2026 03:45:17 +0000 Subject: [PATCH 08/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 289901bee..8f0f5e0b7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-3048b87 +leanprover/lean4-pr-releases:pr-release-14805-380b07b From b6f758d75c79b67c7fc944377fc5262de23e6563 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 02:28:57 +0000 Subject: [PATCH 09/20] adapt batteries --- batteries/Batteries/Lean/Meta/DiscrTree.lean | 9 +++++++++ batteries/Batteries/Tactic/Lint/Simp.lean | 1 + 2 files changed, 10 insertions(+) diff --git a/batteries/Batteries/Lean/Meta/DiscrTree.lean b/batteries/Batteries/Lean/Meta/DiscrTree.lean index fc6465844..303c3377f 100644 --- a/batteries/Batteries/Lean/Meta/DiscrTree.lean +++ b/batteries/Batteries/Lean/Meta/DiscrTree.lean @@ -39,6 +39,15 @@ namespace Trie Merge two `Trie`s. Duplicate values are preserved. -/ partial def mergePreservingDuplicates : Trie α → Trie α → Trie α + | chain k₁ c₁, chain k₂ c₂ => + if k₁ == k₂ then + .chain k₁ (mergePreservingDuplicates c₁ c₂) + else + node #[] (mergeChildren #[(k₁, c₁)] #[(k₂, c₂)]) + | chain k₁ c₁, node vs₂ cs₂ => + node vs₂ (mergeChildren #[(k₁, c₁)] cs₂) + | node vs₁ cs₁, chain k₂ c₂ => + node vs₁ (mergeChildren cs₁ #[(k₂, c₂)]) | node vs₁ cs₁, node vs₂ cs₂ => node (vs₁ ++ vs₂) (mergeChildren cs₁ cs₂) where diff --git a/batteries/Batteries/Tactic/Lint/Simp.lean b/batteries/Batteries/Tactic/Lint/Simp.lean index e09c4bdf3..bd4bc9c2e 100644 --- a/batteries/Batteries/Tactic/Lint/Simp.lean +++ b/batteries/Batteries/Tactic/Lint/Simp.lean @@ -106,6 +106,7 @@ partial def _root_.Lean.Meta.DiscrTree.elements (d : DiscrTree α) : Array α := where /-- Returns the list of elements in the trie. -/ trieElements (arr) + | Trie.chain _ c => trieElements arr c | Trie.node vs children => children.foldl (init := arr ++ vs) fun arr (_, child) => trieElements arr child From 6a75e5fdbd3517a18449cec62488c9bda859112d Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 02:51:46 +0000 Subject: [PATCH 10/20] implement DiscrTree.elements in terms of DiscrTree.values --- batteries/Batteries/Tactic/Lint/Simp.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/batteries/Batteries/Tactic/Lint/Simp.lean b/batteries/Batteries/Tactic/Lint/Simp.lean index bd4bc9c2e..288e81567 100644 --- a/batteries/Batteries/Tactic/Lint/Simp.lean +++ b/batteries/Batteries/Tactic/Lint/Simp.lean @@ -6,6 +6,7 @@ Authors: Gabriel Ebner module public meta import Lean.Meta.Tactic.Simp.Main +public meta import Lean.Meta.DiscrTree.Util public meta import Batteries.Tactic.Lint.Basic public meta import Batteries.Tactic.OpenPrivate public meta import Batteries.Util.LibraryNote @@ -101,14 +102,9 @@ def isSimpTheorem (declName : Name) : MetaM Bool := do open Lean.Meta.DiscrTree in /-- Returns the list of elements in the discrimination tree. -/ +@[deprecated Lean.Meta.DiscrTree.values (since := "2026-08-18")] partial def _root_.Lean.Meta.DiscrTree.elements (d : DiscrTree α) : Array α := - d.root.foldl (init := #[]) fun arr _ => trieElements arr -where - /-- Returns the list of elements in the trie. -/ - trieElements (arr) - | Trie.chain _ c => trieElements arr c - | Trie.node vs children => - children.foldl (init := arr ++ vs) fun arr (_, child) => trieElements arr child + d.values /-- Add message `msg` to any errors thrown inside `k`. -/ def decorateError (msg : MessageData) (k : MetaM α) : MetaM α := do From 5be68b6cc124c362ca515e7221accd6d8d547f22 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 03:43:49 +0000 Subject: [PATCH 11/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 8f0f5e0b7..479fd7f92 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-380b07b +leanprover/lean4-pr-releases:pr-release-14805-4b6eea7 From 8e1887693bc9f38984c1d9a8f6471d660b56a4d7 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 16:36:09 +0000 Subject: [PATCH 12/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 479fd7f92..b980001d4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-4b6eea7 +leanprover/lean4-pr-releases:pr-release-14805-46cae21 From 8b54c77483b9a25ea555252792abaf9a6fe35f9f Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Wed, 19 Aug 2026 20:03:56 +0000 Subject: [PATCH 13/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index b980001d4..3787f06e2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-46cae21 +leanprover/lean4-pr-releases:pr-release-14805-8c23b20 From 47640670cb7cee5541bbdcd567c8441f42de7d86 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 19 Aug 2026 20:47:16 +0000 Subject: [PATCH 14/20] use asNode/mkNode to avoid previewing trie implementation details --- batteries/Batteries/Lean/Meta/DiscrTree.lean | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/batteries/Batteries/Lean/Meta/DiscrTree.lean b/batteries/Batteries/Lean/Meta/DiscrTree.lean index 303c3377f..c6a2eaa8c 100644 --- a/batteries/Batteries/Lean/Meta/DiscrTree.lean +++ b/batteries/Batteries/Lean/Meta/DiscrTree.lean @@ -38,18 +38,10 @@ namespace Trie /-- Merge two `Trie`s. Duplicate values are preserved. -/ -partial def mergePreservingDuplicates : Trie α → Trie α → Trie α - | chain k₁ c₁, chain k₂ c₂ => - if k₁ == k₂ then - .chain k₁ (mergePreservingDuplicates c₁ c₂) - else - node #[] (mergeChildren #[(k₁, c₁)] #[(k₂, c₂)]) - | chain k₁ c₁, node vs₂ cs₂ => - node vs₂ (mergeChildren #[(k₁, c₁)] cs₂) - | node vs₁ cs₁, chain k₂ c₂ => - node vs₁ (mergeChildren cs₁ #[(k₂, c₂)]) - | node vs₁ cs₁, node vs₂ cs₂ => - node (vs₁ ++ vs₂) (mergeChildren cs₁ cs₂) +partial def mergePreservingDuplicates (t₁ t₂ : Trie α) : Trie α := + match (t₁.asNode, t₂.asNode) with + | ((vs₁, cs₁), (vs₂, cs₂)) => + Trie.mkNode (vs₁ ++ vs₂) (mergeChildren cs₁ cs₂) where /-- Auxiliary definition for `mergePreservingDuplicates`. -/ mergeChildren (cs₁ cs₂ : Array (Key × Trie α)) : From 09ed2079ad34b605a38f214047f0f8b6b46057f9 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Thu, 20 Aug 2026 13:15:12 +0000 Subject: [PATCH 15/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 3787f06e2..20de1a62f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-8c23b20 +leanprover/lean4-pr-releases:pr-release-14805-d62a3fd From 5a9e56159dc81d39a542bc4136fd5f349e0260b5 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 21 Aug 2026 01:07:39 +0000 Subject: [PATCH 16/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 20de1a62f..466cc7513 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-d62a3fd +leanprover/lean4-pr-releases:pr-release-14805-c6f7c1a From d43df78d90318ef937f614f2a5724de3d0841b0b Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 21 Aug 2026 02:37:30 +0000 Subject: [PATCH 17/20] change node to chain in DiscrTree test output --- mathlib4/MathlibTest/Tactic/Push/Basic.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/mathlib4/MathlibTest/Tactic/Push/Basic.lean b/mathlib4/MathlibTest/Tactic/Push/Basic.lean index 06f4e4199..0fec4df68 100644 --- a/mathlib4/MathlibTest/Tactic/Push/Basic.lean +++ b/mathlib4/MathlibTest/Tactic/Push/Basic.lean @@ -55,11 +55,11 @@ info: DiscrTree branch for Or: (node (* => (node (False => (node #[or_false:1000])) - (And => (node (* => (node (* => (node #[or_and_left:1000])))))) + (And => (chain * => (chain * => (node #[or_and_left:1000])))) (True => (node #[or_true:1000])))) - (False => (node (* => (node #[false_or:1000])))) - (And => (node (* => (node (* => (node (* => (node #[and_or_right:1000])))))))) - (True => (node (* => (node #[true_or:1000]))))) + (False => (chain * => (node #[false_or:1000]))) + (And => (chain * => (chain * => (chain * => (node #[and_or_right:1000]))))) + (True => (chain * => (node #[true_or:1000])))) -/ #guard_msgs in #push_discr_tree Or From 08426847ed93eedcb94a28fe110a1cc4154c9d56 Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 28 Aug 2026 13:41:15 +0000 Subject: [PATCH 18/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index 466cc7513..f347450d7 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-c6f7c1a +leanprover/lean4-pr-releases:pr-release-14805-210a648 From 3050bdfd1a8422ac159c9c25c9145e597d377949 Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Fri, 28 Aug 2026 12:57:13 -0400 Subject: [PATCH 19/20] Remove double import --- batteries/Batteries/Tactic/Lint/Simp.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/batteries/Batteries/Tactic/Lint/Simp.lean b/batteries/Batteries/Tactic/Lint/Simp.lean index 240338c3a..fb4095144 100644 --- a/batteries/Batteries/Tactic/Lint/Simp.lean +++ b/batteries/Batteries/Tactic/Lint/Simp.lean @@ -7,7 +7,6 @@ module public meta import Lean.Meta.DiscrTree.Util public meta import Lean.Meta.Tactic.Simp.Main -public meta import Lean.Meta.DiscrTree.Util public meta import Batteries.Tactic.Lint.Basic public meta import Batteries.Tactic.OpenPrivate public meta import Batteries.Util.LibraryNote From 33f1924f82fcfc677e2f6cfba718f8f0a3a647ce Mon Sep 17 00:00:00 2001 From: "downstream-lean4[bot]" Date: Fri, 28 Aug 2026 18:04:51 +0000 Subject: [PATCH 20/20] downstream: follow upstream PR --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index f347450d7..3580a1bc4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4-pr-releases:pr-release-14805-210a648 +leanprover/lean4-pr-releases:pr-release-14805-0ad131b