From 3c4f3be74d9d7a7761339370d9daa8e2745b43d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Thu, 24 Jul 2025 06:27:52 +0800 Subject: [PATCH 1/5] chore: bump toolchain to v4.22.0-rc2 --- Algorithm/Data/Classes/AssocArray.lean | 2 +- Algorithm/Data/Classes/IndexedMinHeap.lean | 2 +- Algorithm/Data/Classes/ToMultiset.lean | 2 +- Algorithm/Data/DFinsupp'/Basic.lean | 2 +- Algorithm/Data/DFinsupp'/Defs.lean | 4 +-- Algorithm/Data/Graph/AdjList.lean | 4 +-- Algorithm/Data/UnionFind.lean | 10 +++---- Algorithm/Graph/DFS.lean | 2 +- Algorithm/Graph/Dijkstra.lean | 22 +++++++------- Algorithm/Tactic/Attr/Register.lean | 4 +-- lake-manifest.json | 34 +++++++++++----------- lakefile.lean | 4 +-- lean-toolchain | 2 +- 13 files changed, 46 insertions(+), 48 deletions(-) diff --git a/Algorithm/Data/Classes/AssocArray.lean b/Algorithm/Data/Classes/AssocArray.lean index 33f0122..c89aa33 100644 --- a/Algorithm/Data/Classes/AssocArray.lean +++ b/Algorithm/Data/Classes/AssocArray.lean @@ -135,7 +135,7 @@ variable {C} lemma getElem_listIndicator [DecidableEq ι] (l : List ι) (f : ∀ i ∈ l, α) (i) : (listIndicator C l f)[i] = if hi : i ∈ l then f i hi else d := match l with - | [] => by simp [listIndicator, getElem_default, Function.const] + | [] => by simp [listIndicator, getElem_default] | _ :: l => by rw [listIndicator, getElem_setElem_eq_update, Function.update_apply] split_ifs with h₁ h₂ h₂ diff --git a/Algorithm/Data/Classes/IndexedMinHeap.lean b/Algorithm/Data/Classes/IndexedMinHeap.lean index f8f482a..a673b4f 100644 --- a/Algorithm/Data/Classes/IndexedMinHeap.lean +++ b/Algorithm/Data/Classes/IndexedMinHeap.lean @@ -52,7 +52,7 @@ lemma decreaseKeysD_getElem [DecidableEq ι] {ια : Type*} [ToList ια (ι × | cons hd tl ih => rw [List.foldl_cons, ih, decreaseKeyD_getElem] split_ifs with h - · simp only [List.filterMap_cons, h, List.foldr_cons, min_assoc] + · simp only [List.filterMap_cons, h, min_assoc] congr · simp [h] diff --git a/Algorithm/Data/Classes/ToMultiset.lean b/Algorithm/Data/Classes/ToMultiset.lean index f3f7b0d..a513498 100644 --- a/Algorithm/Data/Classes/ToMultiset.lean +++ b/Algorithm/Data/Classes/ToMultiset.lean @@ -85,7 +85,7 @@ theorem count_toMultiset_eq_zero {a : α} {c : C} : (toMultiset c).count a = 0 simp theorem count_toMultiset_ne_zero {a : α} {c : C} : (toMultiset c).count a ≠ 0 ↔ a ∈ c := by - simp [count_toMultiset_eq_zero, mem_toMultiset] + simp [mem_toMultiset] class Mergeable (C : Type*) (α : outParam Type*) [ToMultiset C α] where merge : C → C → C diff --git a/Algorithm/Data/DFinsupp'/Basic.lean b/Algorithm/Data/DFinsupp'/Basic.lean index bf582c5..44e82a9 100644 --- a/Algorithm/Data/DFinsupp'/Basic.lean +++ b/Algorithm/Data/DFinsupp'/Basic.lean @@ -157,7 +157,7 @@ def subtypeSupportEqEquiv (s : Finset ι) : simpa using Eq.symm right_inv f := by ext1 - simp [Subtype.eta]; rfl + simp; rfl /-- Equivalence between all dependent finitely supported functions `f : Π₀' i, [β i, d i]` and type of pairs `⟨s : Finset ι, f : ∀ i : s, {x : β i // x ≠ d i}⟩`. -/ diff --git a/Algorithm/Data/DFinsupp'/Defs.lean b/Algorithm/Data/DFinsupp'/Defs.lean index e3080ed..35be80d 100644 --- a/Algorithm/Data/DFinsupp'/Defs.lean +++ b/Algorithm/Data/DFinsupp'/Defs.lean @@ -315,7 +315,7 @@ theorem equivFunOnFintype_single [Fintype ι] (i : ι) (m : β i) : DFinsupp'.equivFunOnFintype (DFinsupp'.single d i m) = Function.update d i m := by ext x dsimp [Function.update] - simp [DFinsupp'.single_eq_functionUpdate, @eq_comm _ i] + simp [@eq_comm _ i] @[simp] theorem equivFunOnFintype_symm_single [Fintype ι] (i : ι) (m : β i) : @@ -603,7 +603,7 @@ theorem support_erase (i : ι) (f : Π₀' i, [β i, d i]) : (f.erase i).support = f.support.erase i := by ext j by_cases h1 : j = i - · simp only [h1, mem_support_toFun, erase_apply, ite_true, ne_eq, not_true, not_not, + · simp only [h1, mem_support_toFun, erase_apply, ite_true, ne_eq, not_true, Finset.mem_erase, false_and] · by_cases h2 : f j ≠ d j <;> simp at h2 <;> simp [h1, h2] diff --git a/Algorithm/Data/Graph/AdjList.lean b/Algorithm/Data/Graph/AdjList.lean index 8695837..265673a 100644 --- a/Algorithm/Data/Graph/AdjList.lean +++ b/Algorithm/Data/Graph/AdjList.lean @@ -179,7 +179,7 @@ instance [DecidableEq V] [DecidableEq Info] {v w : g..Quiver} : Fintype (v ⟶ w complete := by rintro ⟨e, rfl, rfl⟩ simp only [coe_toQuiver, Multiset.mem_toFinset, Multiset.mem_pmap, Multiset.mem_filter, - mem_toMultiset, id_eq] + mem_toMultiset] refine ⟨e.info, ⟨e.mem_star, rfl⟩, rfl⟩ end Quiver @@ -282,7 +282,7 @@ lemma ReachableWithin.inter_compl_singleton_self {s : Set V} {v w : V} g..ReachableWithin (s ∩ {v}ᶜ) v w := by obtain (⟨-, h⟩ | ⟨x, hx, h⟩) := h.find {v}ᶜ · exact h - · simp only [sdiff_compl, Set.inf_eq_inter, Set.mem_inter_iff, Set.mem_compl_iff, + · simp only [sdiff_compl, Set.inf_eq_inter, Set.mem_inter_iff, Set.mem_singleton_iff] at hx exact hx.2 ▸ h diff --git a/Algorithm/Data/UnionFind.lean b/Algorithm/Data/UnionFind.lean index b84fed5..f86e787 100644 --- a/Algorithm/Data/UnionFind.lean +++ b/Algorithm/Data/UnionFind.lean @@ -198,7 +198,7 @@ lemma setParent_parent_eq_parent (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦ i ≠ j ∧ i = parent[j]) (i j : ι) (hi : parent[i] = i) (hj : parent[j] = j) (s : ℕ) (k : ι) : (setParent parent size wf i j hi hj s).parent[k] = parent[k] ↔ i = k → j = parent[k] := by - simp [setParent, Function.update] + simp [setParent] @[simp] lemma setParent_parent_eq_self (parent : P) (size : S) @@ -217,12 +217,12 @@ lemma setParent_root (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦ obtain (hk | hk) := decEq parent[k] k <;> simp only [rootCore_parent, hk, ↓reduceIte] · have hik : i ≠ k := by aesop have : (setParent parent size wf i j hi hj s).parent[k] ≠ k := by - simp [ite_eq_iff, hik, hk] + simp [hik, hk] simp only [this, ↓reduceIte] convert setParent_root parent size wf i j hi hj s parent[k] using 1 · simp [← (setParent_parent_eq_parent parent size wf i j hi hj s k).mpr (absurd · hik)] · simp - · simp only [setParent_parent_eq_self, setParent] + · simp only [setParent] unfold rootCore dsimp split_ifs <;> aesop @@ -468,7 +468,7 @@ lemma find_isRoot (self : UnionFind ι P S) (i : ι) : self.IsRoot (self.find i) @[inline] def union (self : UnionFind ι P S) (i j : ι) : UnionFind ι P S := MutableQuotient.map self (fun x ↦ x.union i j) fun _ _ h ↦ by - simp only [UnionFindImpl.UnionFindWF.union_root, h] + simp only [UnionFindImpl.UnionFindWF.union_root] congr! 1 simp [h] -- `simp only [h]` made no progress rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq (h := h)] @@ -480,7 +480,7 @@ def size (self : UnionFind ι P S) (i : ι) (hi : self.IsRoot i) : ℕ := (fun x hx ↦ x.size i (by induction self using MutableQuotient.ind rw [UnionFindImpl.UnionFindWF.isRoot_iff_root, hx, ← hi] - simp [find, getModify])) + simp [find])) (fun _ hx₁ _ hx₂ ↦ by dsimp rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq] diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean index 9adb2b1..63dea3a 100644 --- a/Algorithm/Graph/DFS.lean +++ b/Algorithm/Graph/DFS.lean @@ -310,7 +310,7 @@ lemma dfsTR_spec' (g : G) mem_succList_iff, DFinsupp'.coe_update] rw [DFinsupp'.support_update_ne _ _ (by simp), Finset.coe_insert, traversal_insert] · simp [hv] - · ext; simp (config := { contextual := true }) [hv] + · ext; simp (config := { contextual := true }) · unfold Function.update aesop diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index c0c6423..40b6a45 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -561,11 +561,10 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) rw [isLeastOfEdges_congr (dijkstraStep_snd_support _ _ _ _ _)] rw [isLeastOfEdges_congr Set.union_singleton.symm] rw [isLeastOfEdges_union] - simp only [ne_eq, Set.mem_setOf_eq, dijkstraStep_snd_getElem, - dijkstraStep_fst_getElem (spec₁ := h₁)] + simp only [ne_eq, Set.mem_setOf_eq, dijkstraStep_snd_getElem] by_cases wmin : w = minIdx heap · subst wmin - simp [hMinIdx] at resw + simp at resw · simp only [ne_eq, wmin, not_false_eq_true, true_and, min_def, Finset.le_inf_iff, Finset.mem_univ, forall_true_left] at resw ⊢ split_ifs with he @@ -621,8 +620,7 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) · simp only [ne_eq, wmin, not_false_eq_true, true_and] at resw ⊢ exact h₃ w resw rw [not_not] at wmin; subst wmin - simp only [ne_eq, not_true_eq_false, false_and, not_false_eq_true, Set.mem_setOf_eq, - ↓reduceIte] + simp only [ne_eq, Set.mem_setOf_eq, ↓reduceIte] simp only [ne_eq, Set.mem_setOf_eq, isLeastOfEdges_iff, WithTop.coe_untop, exists_prop, isDist'_iff] at h₂ h₃ ⊢ constructor @@ -664,7 +662,7 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) (min_le_right _ _).trans <| (h₂ v hv evw).trans (add_le_add_right h₃ _) · intro v -- simp? [dijkstraStep_snd_getElem_eq_top, dijkstraStep_fst_getElem_eq_top (spec₁ := h₁), h₄] - simp only [ne_eq, h₄, dijkstraStep_snd_support, not_and, + simp only [ne_eq, h₄, dijkstraStep_snd_support, dijkstraStep_fst_getElem_eq_top (spec₁ := h₁), mem_succSet_iff, Set.mem_singleton_iff, exists_eq_left] rw [traversal_insert] @@ -693,7 +691,7 @@ where let hr := g..dijkstraStep c heap res hh have : Fintype.card {v : V | hr.2[v] = ⊤} < Fintype.card {v : V | res[v] = ⊤} := by letI : DecidableEq V := by classical infer_instance - simp only [dijkstraStep_snd_getElem_eq_top, ne_eq, Set.coe_setOf, Set.mem_setOf_eq, hr] + simp only [dijkstraStep_snd_getElem_eq_top, ne_eq, Set.coe_setOf, hr] exact Fintype.card_lt_of_injective_of_notMem (fun ⟨v, hv⟩ ↦ ⟨v, hv.2⟩) (by intro ⟨v, hv⟩ ⟨w, hw⟩; simp) (b := ⟨minIdx heap, (spec.1 _).resolve_left hh⟩) (by simp) @@ -701,15 +699,15 @@ where termination_by Fintype.card {v : V | res[v] = ⊤} spec_init : dijkstraStep.Spec g c init init default := by constructor - · simp [default] - · simp only [AssocDArray.getElem_default, default, Function.const_apply, ne_eq, + · simp + · simp only [AssocDArray.getElem_default, ne_eq, not_true_eq_false, IsEmpty.forall_iff, implies_true, and_true, Set.mem_setOf_eq, forall_true_left] intro h use ⊤ - simp [isLeastOfEdges_iff, default] - · simp [default] - · simp [traversal, default] + simp [isLeastOfEdges_iff] + · simp + · simp [traversal] lemma dijkstra_spec (g : G) (c : Info → CostType) [Fintype V] [AddCommMonoid CostType] [LinearOrder CostType] [CanonicallyOrderedAdd CostType] diff --git a/Algorithm/Tactic/Attr/Register.lean b/Algorithm/Tactic/Attr/Register.lean index b6b3fc3..2aac1ea 100644 --- a/Algorithm/Tactic/Attr/Register.lean +++ b/Algorithm/Tactic/Attr/Register.lean @@ -5,7 +5,7 @@ Authors: Yuyang Zhao -/ import Lean.Meta.Tactic.Simp.RegisterCommand -/-- The simpset `getElem_simps` is used by the tactic `get_elem_tactic_trivial`. -/ +/-- The simpset `getElem_simps` is used by the tactic `get_elem_tactic_extensible`. -/ register_simp_attr getElem_simps -macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| simp_all [getElem_simps]; done) +macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp_all [getElem_simps]; done) diff --git a/lake-manifest.json b/lake-manifest.json index bb62a92..b151e80 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "05a43fcf9c484d69252bbc3556ca0fdb2417048a", + "rev": "928dded10db6ac432d0d0eb13ebe97784c84021c", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", + "inputRev": "v4.22.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "308445d7985027f538e281e18df29ca16ede2ba3", + "rev": "1a5c8fe51b870f5c4ffd6fe44936e09a776d8f3e", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.21.0", + "inputRev": "v4.22.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0", + "rev": "a8733224c9aad9d372d82f208e32da1eed667875", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c4aa78186d388e50a436e8362b947bae125a2933", + "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -85,50 +85,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457", + "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", + "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.62", + "inputRev": "v0.0.63-pre", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8ff27701d003456fd59f13a9212431239d902aef", + "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", + "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "master", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", + "rev": "bfd7f60186ea20946cc36288f83ad3659520f0ce", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "nightly-testing", "inherited": true, "configFile": "lakefile.toml"}], "name": "algorithm", diff --git a/lakefile.lean b/lakefile.lean index efcbb1a..cbaaa4c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,8 +2,8 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.21.0" -require "leanprover" / "doc-gen4" @ git "v4.21.0" +require "leanprover-community" / "mathlib" @ git "v4.22.0-rc2" +require "leanprover" / "doc-gen4" @ git "v4.22.0-rc2" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index 980709b..bfcebb1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.21.0 +leanprover/lean4:v4.22.0-rc2 From a3e649ecdfc8bf83cf5d7d4355e5b1709fe5b2ef Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 16 Aug 2025 11:58:32 +0800 Subject: [PATCH 2/5] chore: bump toolchain to v4.22.0-rc3 --- lake-manifest.json | 36 ++++++++++++++++++------------------ lakefile.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 21 insertions(+), 21 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index b151e80..ca9eaac 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "928dded10db6ac432d0d0eb13ebe97784c84021c", + "rev": "061dfa3b4207216f7c7a7f63e99421f551059687", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0-rc2", + "inputRev": "v4.22.0-rc3", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "1a5c8fe51b870f5c4ffd6fe44936e09a776d8f3e", + "rev": "19f4ef2c52b278bd96626e02d594751e6e12ac98", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0-rc2", + "inputRev": "v4.22.0-rc3", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "a8733224c9aad9d372d82f208e32da1eed667875", + "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "1cf274454c624e4b94c79f14b6db70d9fe0bdd51", + "rev": "bb6eb5b25892aa968e9d35f6ef9ca5c6b896c16d", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d", + "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -85,50 +85,50 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199", + "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17", + "rev": "96c67159f161fb6bf6ce91a2587232034ac33d7e", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.63-pre", + "inputRev": "v0.0.67", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8", + "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4", + "rev": "867d9dc77534341321179c9aa40fceda675c50d4", "name": "Qq", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bfd7f60186ea20946cc36288f83ad3659520f0ce", + "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}], "name": "algorithm", diff --git a/lakefile.lean b/lakefile.lean index cbaaa4c..88acb2f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,8 +2,8 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.22.0-rc2" -require "leanprover" / "doc-gen4" @ git "v4.22.0-rc2" +require "leanprover-community" / "mathlib" @ git "v4.22.0-rc3" +require "leanprover" / "doc-gen4" @ git "v4.22.0-rc3" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index bfcebb1..fff0a20 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0-rc2 +leanprover/lean4:v4.22.0-rc3 From 17ba2975b4813cc9c042b1dcfe5cf3ac0df20298 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 16 Aug 2025 12:03:59 +0800 Subject: [PATCH 3/5] chore: bump toolchain to v4.22.0-rc4 --- lake-manifest.json | 20 ++++++++++---------- lakefile.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index ca9eaac..fab768e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,27 +5,27 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "061dfa3b4207216f7c7a7f63e99421f551059687", + "rev": "ab0dca34de1a12caedcf3f94a10bc9ed303f67da", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0-rc3", + "inputRev": "v4.22.0-rc4", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "19f4ef2c52b278bd96626e02d594751e6e12ac98", + "rev": "928758ac3743dc7f171fc66f450506723896f1c5", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.22.0-rc3", + "inputRev": "v4.22.0-rc4", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/mhuisi/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "e22ed0883c7d7f9a7e294782b6b137b783715386", + "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "61c44bec841faabd47d11c2eda15f57ec2ffe9d5", + "rev": "c37191eba2da78393070da8c4367689d8c4276e4", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "140dc642f4f29944abcdcd3096e8ea9b4469c873", + "rev": "4241928fd3ebae83a037a253e39d9b773e34c3b4", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -105,7 +105,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a62ecd0343a2dcfbcac6d1e8243f5821879c0244", + "rev": "0a136f764a5dfedc4498e93ad8e297cff57ba2fc", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "867d9dc77534341321179c9aa40fceda675c50d4", + "rev": "1ef3dac0f872ca6aaa7d02e015427e06dd0b6195", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3cabaef23886b82ba46f07018f2786d9496477d6", + "rev": "e96b5eca4fcfe2e0e96a1511a6cd5747515aba82", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lakefile.lean b/lakefile.lean index 88acb2f..41c54f8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,8 +2,8 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.22.0-rc3" -require "leanprover" / "doc-gen4" @ git "v4.22.0-rc3" +require "leanprover-community" / "mathlib" @ git "v4.22.0-rc4" +require "leanprover" / "doc-gen4" @ git "v4.22.0-rc4" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index fff0a20..2c6e1c4 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.22.0-rc3 +leanprover/lean4:v4.22.0-rc4 From 4c1e14cdb009419883eb57112fe8bc17c14c98e5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 16 Aug 2025 13:32:46 +0800 Subject: [PATCH 4/5] Update ToList.lean --- Algorithm/Data/Classes/ToList.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Algorithm/Data/Classes/ToList.lean b/Algorithm/Data/Classes/ToList.lean index a6fb77e..861b028 100644 --- a/Algorithm/Data/Classes/ToList.lean +++ b/Algorithm/Data/Classes/ToList.lean @@ -252,7 +252,7 @@ instance : Front (Array α) α where front c h := c[0]'(by simp_rw [isEmpty_iff_size_eq_zero, size] at h; omega) frontD_def := by simp front_mem _ := by - simp [size, ← ne_eq, ← Array.toList_eq_nil_iff, ← List.length_pos_iff_ne_nil] + simp [← ne_eq] instance : Back (Array α) α where back? := Array.back? From fbe3fd32847c2e231d95228a9687b21f21b6cd0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Sat, 16 Aug 2025 14:18:11 +0800 Subject: [PATCH 5/5] fix slowdown --- Algorithm/Data/Classes/GetElem.lean | 6 +++--- Algorithm/Tactic/Attr/Register.lean | 17 ++++++++++++++++- 2 files changed, 19 insertions(+), 4 deletions(-) diff --git a/Algorithm/Data/Classes/GetElem.lean b/Algorithm/Data/Classes/GetElem.lean index ef1d108..820745e 100644 --- a/Algorithm/Data/Classes/GetElem.lean +++ b/Algorithm/Data/Classes/GetElem.lean @@ -36,7 +36,7 @@ class GetSetElem (C : Type*) (ι : Type*) (α : outParam Type*) export GetSetElem (valid_setElem getElem_setElem_self getElem_setElem_of_ne) attribute [getElem_simps] valid_setElem -attribute [simp] getElem_setElem_self getElem_setElem_of_ne +attribute [getElem_simps, simp] getElem_setElem_self getElem_setElem_of_ne lemma valid_setElem_self [GetSetElem C ι α Valid] {c : C} {i : ι} {x} : Valid c[i ↦ x] i := by @@ -69,7 +69,7 @@ class GetSetEraseElem (C : Type*) (ι : Type*) (α : outParam Type*) export GetSetEraseElem (valid_erase getElem_erase_of_ne) attribute [getElem_simps] valid_erase -attribute [simp] getElem_erase_of_ne +attribute [getElem_simps, simp] getElem_erase_of_ne lemma not_valid_erase_self [GetSetEraseElem C ι α Valid] {c : C} {i : ι} : ¬Valid (erase c i) i := by @@ -151,7 +151,7 @@ export GetElemAllValid (all_valid) attribute [simp] all_valid -macro_rules | `(tactic| get_elem_tactic_trivial) => `(tactic| exact GetElemAllValid.all_valid) +macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| exact GetElemAllValid.all_valid) class GetSetElemAllValid (C : Type*) (ι : Type*) (α : outParam Type*) extends GetElemAllValid C ι α, SetElem C ι α where diff --git a/Algorithm/Tactic/Attr/Register.lean b/Algorithm/Tactic/Attr/Register.lean index 2aac1ea..21b4aef 100644 --- a/Algorithm/Tactic/Attr/Register.lean +++ b/Algorithm/Tactic/Attr/Register.lean @@ -8,4 +8,19 @@ import Lean.Meta.Tactic.Simp.RegisterCommand /-- The simpset `getElem_simps` is used by the tactic `get_elem_tactic_extensible`. -/ register_simp_attr getElem_simps -macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| simp_all [getElem_simps]; done) +macro_rules +| `(tactic| get_elem_tactic_extensible) => + `(tactic| simp +contextual only [getElem_simps, + ne_eq, ite_true, ite_false, dite_true, dite_false, + ite_cond_eq_true, ite_cond_eq_false, dite_cond_eq_true, dite_cond_eq_false, ite_self, + and_true, true_and, and_false, false_and, and_self, and_not_self, not_and_self, + and_imp, not_and, or_self, or_true, true_or, or_false, false_or, + iff_self, iff_true, true_iff, iff_false, false_iff, false_implies, forall_false, + implies_true, true_implies, not_false_eq_true, not_true_eq_false, not_iff_self, + ne_eq, *] at *; done) + +/- +was `simp_all [getElem_simps]` + +TODO: make a better tactic. `simp` lemmas about `?Valid ?c[?i ↦ ?x] ?j` is so bad. +-/