From 5bb11cda52689f8c90bb3799cfd3f0df3a7b8d8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 18 Sep 2026 14:58:39 +0800 Subject: [PATCH 1/2] chore: bump toolchain to v4.33.1 --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- lean-toolchain | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 5c547de..08f4f93 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.33.1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", diff --git a/lakefile.lean b/lakefile.lean index a3ce923..903776e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.33.0" +require "leanprover-community" / "mathlib" @ git "v4.33.1" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index 025e595..a8afa7d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.33.1 From 19d11aaffa96ea4f95526130e7b47d3772f41e28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Yuyang=20Zhao=20=E8=B5=B5=E9=9B=A8=E6=89=AC?= Date: Fri, 18 Sep 2026 15:10:31 +0800 Subject: [PATCH 2/2] chore: bump toolchain to v4.34.0-rc1 --- Algorithm/Data/Classes/DefaultDict.lean | 6 +++--- Algorithm/Data/DFinsupp/Basic.lean | 8 ++++---- Algorithm/Data/DFinsupp/Defs.lean | 21 +++++++++++---------- Algorithm/Data/UnionFind.lean | 10 +++++----- Algorithm/Graph/DFS.lean | 8 ++++---- Algorithm/Graph/Dijkstra.lean | 3 ++- Algorithm/Tactic/Attr/Register.lean | 3 ++- lake-manifest.json | 22 +++++++++++----------- lakefile.lean | 2 +- lean-toolchain | 2 +- 10 files changed, 44 insertions(+), 41 deletions(-) diff --git a/Algorithm/Data/Classes/DefaultDict.lean b/Algorithm/Data/Classes/DefaultDict.lean index 52ac6fc..a8ac774 100644 --- a/Algorithm/Data/Classes/DefaultDict.lean +++ b/Algorithm/Data/Classes/DefaultDict.lean @@ -138,8 +138,8 @@ lemma getElem_listIndicator [DecidableEq ι] (l : List ι) (f : ∀ i ∈ l, α) split_ifs with h₁ h₂ h₂ · simp [h₁] · simp [h₁] at h₂ - · simp_rw [getElem_listIndicator, dif_pos (List.mem_of_ne_of_mem h₁ h₂)] - · simp_rw [getElem_listIndicator, dif_neg (List.not_mem_of_not_mem_cons h₂)] + · simp_rw [getElem_listIndicator, dite_eq_left (List.mem_of_ne_of_mem h₁ h₂)] + · simp_rw [getElem_listIndicator, dite_eq_right (List.not_mem_of_not_mem_cons h₂)] variable [Ext C ι α d] variable (C) @@ -165,7 +165,7 @@ lemma getElem_indicator [DecidableEq ι] (s : Finset ι) (f : ∀ i ∈ s, α) ( abbrev toOfFn [Fintype ι] (f : ι → α) : OfFn C ι α f where ofFn := indicator C Finset.univ (fun i _ ↦ f i) getElem_ofFn _ := by - convert (getElem_indicator _ _ _).trans <| dif_pos <| Finset.mem_univ _ + convert (getElem_indicator _ _ _).trans <| dite_eq_left <| Finset.mem_univ _ classical infer_instance end DefaultDict diff --git a/Algorithm/Data/DFinsupp/Basic.lean b/Algorithm/Data/DFinsupp/Basic.lean index 9d76aed..e6ca64d 100644 --- a/Algorithm/Data/DFinsupp/Basic.lean +++ b/Algorithm/Data/DFinsupp/Basic.lean @@ -59,10 +59,10 @@ theorem filter_apply (p : ι → Prop) [DecidablePred p] (i : ι) (f : Π₀' i, rfl theorem filter_apply_pos {p : ι → Prop} [DecidablePred p] (f : Π₀' i, [β i, d i]) {i : ι} - (h : p i) : f.filter p i = f i := by simp only [filter_apply, if_pos h] + (h : p i) : f.filter p i = f i := by simp only [filter_apply, ite_eq_left h] theorem filter_apply_neg {p : ι → Prop} [DecidablePred p] (f : Π₀' i, [β i, d i]) {i : ι} - (h : ¬p i) : f.filter p i = d i := by simp only [filter_apply, if_neg h] + (h : ¬p i) : f.filter p i = d i := by simp only [filter_apply, ite_eq_right h] @[simp] theorem filter_default (p : ι → Prop) [DecidablePred p] : @@ -111,11 +111,11 @@ theorem filter_single (p : ι → Prop) [DecidablePred p] (i : ι) (x : β i) : @[simp] theorem filter_single_pos {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : p i) : - (single d i x).filter p = single d i x := by rw [filter_single, if_pos h] + (single d i x).filter p = single d i x := by rw [filter_single, ite_eq_left h] @[simp] theorem filter_single_neg {p : ι → Prop} [DecidablePred p] (i : ι) (x : β i) (h : ¬p i) : - (single d i x).filter p = default := by rw [filter_single, if_neg h] + (single d i x).filter p = default := by rw [filter_single, ite_eq_right h] theorem piecewise_single_erase (x : Π₀' i, [β i, d i]) (i : ι) [∀ i' : ι, Decidable <| (i' ∈ ({i} : Set ι))] : -- Porting note: added Decidable hypothesis diff --git a/Algorithm/Data/DFinsupp/Defs.lean b/Algorithm/Data/DFinsupp/Defs.lean index c9df85d..d71293b 100644 --- a/Algorithm/Data/DFinsupp/Defs.lean +++ b/Algorithm/Data/DFinsupp/Defs.lean @@ -196,7 +196,7 @@ variable (d) in defined on this `Finset`. -/ def mk (s : Finset ι) (x : ∀ i : (↑s : Set ι), β (i : ι)) : Π₀' i, [β i, d i] := ⟨fun i => if H : i ∈ s then x ⟨i, H⟩ else d i, - Trunc.mk ⟨s.1, fun i => if H : i ∈ s then Or.inl H else Or.inr <| dif_neg H⟩⟩ + Trunc.mk ⟨s.1, fun i => if H : i ∈ s then Or.inl H else Or.inr <| dite_eq_right H⟩⟩ variable {s : Finset ι} {x : ∀ i : (↑s : Set ι), β i} {i : ι} @@ -205,10 +205,10 @@ theorem mk_apply : (mk d s x : ∀ i, β i) i = if H : i ∈ s then x ⟨i, H⟩ rfl theorem mk_of_mem (hi : i ∈ s) : (mk d s x : ∀ i, β i) i = x ⟨i, hi⟩ := - dif_pos hi + dite_eq_left hi theorem mk_of_not_mem (hi : i ∉ s) : (mk d s x : ∀ i, β i) i = d i := - dif_neg hi + dite_eq_right hi variable (d) in theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β d _ s) := by @@ -217,7 +217,7 @@ theorem mk_injective (s : Finset ι) : Function.Injective (@mk ι β d _ s) := b have h1 : (mk d s x : ∀ i, β i) i = (mk d s y : ∀ i, β i) i := by rw [H] obtain ⟨i, hi : i ∈ s⟩ := i dsimp only [mk_apply, Subtype.coe_mk] at h1 - simpa only [dif_pos hi] using h1 + simpa only [dite_eq_left hi] using h1 end mk @@ -279,7 +279,7 @@ theorem single_eq_same {i b} : single d i b i = b := by simp only [single_apply, dite_eq_ite, ite_true] theorem single_eq_of_ne {i i' b} (h : i ≠ i') : single d i b i' = d i' := by - simp only [single_apply, dif_neg h] + simp only [single_apply, dite_eq_right h] theorem single_injective {i} : Function.Injective (single d i) := fun _ _ H => Function.update_injective _ i <| DFunLike.coe_injective.eq_iff.mpr H @@ -417,12 +417,12 @@ theorem erase_single (j : ι) (i : ι) (x : β i) : @[simp] theorem erase_single_same (i : ι) (x : β i) : (single d i x).erase i = default := by - rw [erase_single, if_pos rfl] + rw [erase_single, ite_eq_left rfl] @[simp] theorem erase_single_ne {i j : ι} (x : β i) (h : i ≠ j) : (single d i x).erase j = single d i x := by - rw [erase_single, if_neg h] + rw [erase_single, ite_eq_right h] @[simp] theorem update_eq_erase (f : Π₀' i, [β i, d i]) (i : ι) : @@ -444,9 +444,10 @@ theorem single_zipWith_erase (f : ∀ i, β i → β i → β i) zipWith f (fun _ ↦ hf₁ _ _) (single d i (x i)) (x.erase i) = x := ext fun i' => if h : i = i' then by - subst h; simp only [zipWith_apply, single_apply, erase_apply, hf₂, dite_eq_ite, if_true] + subst h; simp only [zipWith_apply, single_apply, erase_apply, hf₂, dite_eq_ite, ite_true] else by - simp only [zipWith_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), hf₁] + simp only [zipWith_apply, single_apply, erase_apply, dite_eq_right h, + ite_eq_right (Ne.symm h), hf₁] protected theorem induction_on {p : (Π₀' i, [β i, d i]) → Prop} (x : Π₀' i, [β i, d i]) (f : ∀ i, β i → β i → β i) (hf₁ : ∀ i x, f i (d i) x = x) (hf₂ : ∀ i x, f i x (d i) = x) @@ -468,7 +469,7 @@ protected theorem induction_on {p : (Π₀' i, [β i, d i]) → Prop} (x : Π₀ intro j cases H j with | _ H2 · cases Multiset.mem_cons.1 H2 with | _ H3 - · right; exact if_pos H3 + · right; exact ite_eq_left H3 · left; exact H3 right split_ifs <;> [rfl; exact H2] diff --git a/Algorithm/Data/UnionFind.lean b/Algorithm/Data/UnionFind.lean index ac302a5..a08984e 100644 --- a/Algorithm/Data/UnionFind.lean +++ b/Algorithm/Data/UnionFind.lean @@ -41,14 +41,14 @@ termination_by wf.wrap i lemma rootCore_of_eq (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i : ι) (hi : parent[i] = i) : rootCore parent wf i = i := by - rw [rootCore, if_pos hi] + rw [rootCore, ite_eq_left hi] @[simp] lemma rootCore_parent (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i : ι) : rootCore parent wf parent[i] = rootCore parent wf i := by conv_rhs => rw [rootCore] split_ifs with h - · rw [rootCore, h, if_pos h] + · rw [rootCore, h, ite_eq_left h] · rfl @[simp] @@ -63,7 +63,7 @@ termination_by wf.wrap i lemma transGen_rootCore (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k]) (i : ι) (hi : parent[i] ≠ i) : Relation.TransGen (fun i j ↦ i ≠ j ∧ i = parent[j]) (rootCore parent wf i) i := by - rw [rootCore, if_neg hi, rootCore] + rw [rootCore, ite_eq_right hi, rootCore] split_ifs with h · exact .single ⟨hi, rfl⟩ · rw [rootCore_parent] @@ -260,7 +260,7 @@ lemma link_root (self : UnionFind ι P S) (i j : ι) (hi : self.parent[i] = i) self.root k := by ext k; unfold link; dsimp obtain (hij | rfl) := decEq i j - · rw [if_neg hij] + · rw [ite_eq_right hij] split_ifs with hk hs <;> aesop · aesop @@ -314,7 +314,7 @@ lemma setParent_wf (self : UnionFind ι P S) rw [rootCore] split_ifs with h · rw [root_of_parent_eq _ _ h]; tauto - · rw [root, rootCore, if_neg h]; tauto + · rw [root, rootCore, ite_eq_right h]; tauto · simp [hk] at hjk · rw [h k hk] congr! 3 diff --git a/Algorithm/Graph/DFS.lean b/Algorithm/Graph/DFS.lean index 638fb8a..5774832 100644 --- a/Algorithm/Graph/DFS.lean +++ b/Algorithm/Graph/DFS.lean @@ -165,9 +165,9 @@ lemma isDFSForest_dfsForest' (g : G) (dfsForest' g vs visited).1 := by induction vs, visited using dfsForest'.induct g (BoolArray := BoolArray) with | case1 => unfold dfsForest'; constructor - | case2 _ _ _ h ih => rwa [dfsForest', if_pos h] + | case2 _ _ _ h ih => rwa [dfsForest', ite_eq_left h] | case3 visited v vs hv _ _ _ _ hc _ _ _ _ ih₁ ih₂ => - rw [dfsForest', if_neg hv] + rw [dfsForest', ite_eq_right hv] let rc := dfsForest' g (succList g v) visited[v ↦ true] dsimp; apply IsDFSForest.node {v : V | rc.2.val[v]} · simp [hv] @@ -322,13 +322,13 @@ lemma dfsTR_spec' (g : G) induction vs, visited using dfsTR.induct g (BoolArray := BoolArray) with | case1 => simp [dfsTR] | case2 _ v _ hv ih => - simp only [dfsTR, if_pos hv, List.mem_cons] + simp only [dfsTR, ite_eq_left hv, List.mem_cons] rw [← ih] ext w simp [traversal] aesop | case3 _ _ _ hv ih => - rw [dfsTR, if_neg hv, ← ih] + rw [dfsTR, ite_eq_right hv, ← ih] rw [visited_set_true, traversal_insert] · simp [hv] · ext; simp (config := { contextual := true }) diff --git a/Algorithm/Graph/Dijkstra.lean b/Algorithm/Graph/Dijkstra.lean index 0a38e08..f992d5e 100644 --- a/Algorithm/Graph/Dijkstra.lean +++ b/Algorithm/Graph/Dijkstra.lean @@ -569,7 +569,8 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType) obtain ⟨d, h₂⟩ := h₂ use min d <| (Finset.univ (α := ToQuiver.mk g (minIdx heap) ⟶ ToQuiver.mk g w)).inf fun e ↦ heap[minIdx heap] + c (e : E g).info - constructor; · rw [dijkstraStep_fst_getElem (spec₁ := h₁), if_neg (by tauto), h₂.1, min_assoc] + constructor + · rw [dijkstraStep_fst_getElem (spec₁ := h₁), ite_eq_right (by tauto), h₂.1, min_assoc] replace h₂ := h₂.2 rw [isLeastOfEdges_congr (dijkstraStep_snd_support _ _ _ _ _)] rw [isLeastOfEdges_congr Set.union_singleton.symm] diff --git a/Algorithm/Tactic/Attr/Register.lean b/Algorithm/Tactic/Attr/Register.lean index 5252ef0..df3e6ea 100644 --- a/Algorithm/Tactic/Attr/Register.lean +++ b/Algorithm/Tactic/Attr/Register.lean @@ -18,7 +18,8 @@ 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, + ite_eq_left_of_eq_true, ite_eq_right_of_eq_false, dite_eq_left_of_eq_true, + dite_eq_right_of_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, diff --git a/lake-manifest.json b/lake-manifest.json index 08f4f93..834ffd4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "rev": "de5ce8a9a66a4aa68a9bdbb35b63a06d34d9ca11", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.1", + "inputRev": "v4.34.0-rc1", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "38e9c3ce15cbb63c92e90bb9a92e4eb82131f669", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "2bc7cf064315b26bc38dac2e9612fb581be9b75f", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "978b7ec9fbbf9a535114f1de8fe5b3778b358870", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "99e8adeea3c3cd86b6b79ba01a1383bf2d31d055", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "c1c4362a130f12e632d252180a6c2a31d8fd4726", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "3b55e9d00c6b0018e5d984eb011b6f93c09bd163", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "01bc479e7432594821ba3fb0ca465211941de86d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "af8bc067a4cc6c6df472a68909a3f40b1c76c43e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0-rc1", "inherited": true, "configFile": "lakefile.toml"}], "name": "algorithm", diff --git a/lakefile.lean b/lakefile.lean index 903776e..29e7ecf 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,7 +2,7 @@ import Lake open Lake DSL -require "leanprover-community" / "mathlib" @ git "v4.33.1" +require "leanprover-community" / "mathlib" @ git "v4.34.0-rc1" abbrev algorithmOnlyLinters : Array LeanOption := #[ ⟨`linter.mathlibStandardSet, true⟩, diff --git a/lean-toolchain b/lean-toolchain index a8afa7d..75def60 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.1 +leanprover/lean4:v4.34.0-rc1