From 9a0f8782df31b9dd9cb7bef5352e8cdfa9d0a32b Mon Sep 17 00:00:00 2001 From: tsuki8 <3118181069@qq.com> Date: Fri, 2 Oct 2026 11:55:18 +0800 Subject: [PATCH 1/2] Upgrade Lean and dependencies to 4.34.1 --- GroebnerTac/Lemma.lean | 2 -- GroebnerTac/Tactic.lean | 35 +++++++++++----------- GroebnerTac/Template.lean | 6 ++-- lake-manifest.json | 61 ++++++++++++++++++++------------------- lakefile.toml | 19 ++++++------ lean-toolchain | 2 +- 6 files changed, 64 insertions(+), 61 deletions(-) diff --git a/GroebnerTac/Lemma.lean b/GroebnerTac/Lemma.lean index 51afa8e..b54f682 100644 --- a/GroebnerTac/Lemma.lean +++ b/GroebnerTac/Lemma.lean @@ -79,7 +79,6 @@ theorem Rabinovich_method (I : Ideal (MvPolynomial σ K)) (f : MvPolynomial σ K rw [val_t, val_f] rw [IsLocalization.mk'_spec] simp - exact sub_self 1 have h_image : (1 : R_f) ∈ I.map (algebraMap R R_f) := by rw [← map_one φ] have step := Ideal.mem_map_of_mem φ h @@ -202,7 +201,6 @@ theorem Rabinovich_method' rw [val_t, val_f] rw [IsLocalization.mk'_spec] simp - exact sub_self 1 have h_image : (1 : R_f) ∈ I.map (algebraMap R R_f) := by rw [← map_one φ] have step := Ideal.mem_map_of_mem φ h diff --git a/GroebnerTac/Tactic.lean b/GroebnerTac/Tactic.lean index 8ff2fb2..89056b4 100644 --- a/GroebnerTac/Tactic.lean +++ b/GroebnerTac/Tactic.lean @@ -5,7 +5,6 @@ import Groebner.Groebner import Groebner.ToMathlib.List import GroebnerTac.GbOption -import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly import Lean.Meta.Tactic.TryThis import Mathlib.Tactic @@ -600,7 +599,8 @@ def mkSetSyntaxFromTerms (terms : Array Term) : MetaM Term := do /- In this section, we define the tactics to call Sage to prove some algebraic facts -/ -def verifyRemainderLogic (witness : Term) (isZeroTarget : Bool) : TacticM Unit := do +def verifyRemainderLogic (witness : Term) (isZeroTarget : Bool) : TacticM Unit := + withOptions (fun opts => opts.setBool `backward.isDefEq.respectTransparency false) do let runUse := fun x => do Mathlib.Tactic.runUse false (← Mathlib.Tactic.mkUseDischarger .none) [x] evalTactic (← `(tactic| @@ -646,7 +646,7 @@ def verifyRemainderLogic (witness : Term) (isZeroTarget : Bool) : TacticM Unit : all_goals simp only [List.get] rw [← tsub_eq_zero_iff_le, MvPolynomial.SortedRepr.lex_degree_eq] - convert_to _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 + change _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 rw [← SortedFinsupp.toFinsupp_tsub, SortedFinsupp.toFinsupp_eq_zero_iff] decide +kernel +revert )) @@ -795,7 +795,8 @@ def evalRemainderTactic : Tactic := fun stx => do -elab "remainder_zero" : tactic => do +elab "remainder_zero" : tactic => + withOptions (fun opts => opts.setBool `backward.isDefEq.respectTransparency false) do let goal ← Lean.Elab.Tactic.getMainGoal let t ← goal.getType let t ← checkTypeQ t q(Prop) @@ -860,7 +861,8 @@ elab "remainder_zero" : tactic => do dbg_trace "not a lex.IsRemainder" -elab "remainder_neq_zero" : tactic => do +elab "remainder_neq_zero" : tactic => + withOptions (fun opts => opts.setBool `backward.isDefEq.respectTransparency false) do let goal ← Lean.Elab.Tactic.getMainGoal let t ← goal.getType let t ← checkTypeQ t q(Prop) @@ -934,14 +936,15 @@ elab "remainder_neq_zero" : tactic => do all_goals simp only [List.get] rw [← tsub_eq_zero_iff_le, MvPolynomial.SortedRepr.lex_degree_eq] - convert_to _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 + change _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 rw [← SortedFinsupp.toFinsupp_tsub, SortedFinsupp.toFinsupp_eq_zero_iff] decide +kernel +revert )) | _ => dbg_trace "not a lex.IsRemainder" -elab "basis" : tactic => do +elab "basis" : tactic => + withOptions (fun opts => opts.setBool `backward.isDefEq.respectTransparency false) do let goal ← Lean.Elab.Tactic.getMainGoal -- logInfo m!"[DEBUG `basis` Goal] : {goal}" let t ← goal.getType @@ -964,7 +967,7 @@ elab "basis" : tactic => do let parsedTermsArray ← arr.mapM mkPolyListTerm evalTactic (← `(tactic| - rw [MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero] + rw [MonomialOrder.IsGroebnerBasis.iff_isRemainder_sPolynomial_zero] )) evalTactic (← `(tactic| simp only [Fin.isValue, Subtype.forall, Set.mem_insert_iff, Set.mem_singleton_iff, @@ -1006,7 +1009,7 @@ elab "basis" : tactic => do )) evalTactic (← `(tactic| · simp)) - evalTactic (← `(tactic| simp)) + evalTactic (← `(tactic| try simp)) let gs ← getUnsolvedGoals unless gs.isEmpty do evalTactic (← `(tactic| decide +kernel)) @@ -1087,7 +1090,7 @@ elab "submodule_span" "[" coeffs:term,* "]" : tactic => do (smul coeffs.back! bases.back!) else q(0) - let sumMemSpan : Q($sum ∈ Submodule.span $R $s) ← + let sumMemSpan : Q($sum ∈ Submodule.span $R $basesSet) ← match coeffs.size with | 0 => pure <| show Q($sum ∈ Submodule.span $R $basesSet) from show Q(0 ∈ Submodule.span $R $basesSet) from @@ -1197,8 +1200,7 @@ elab "basis'" : tactic => do have h_ideal : Ideal.span ($basis_term : Set $polyType) = $ideal_term := by simp -- ideal - simp only [h_ideal] at h_gb - exact h_gb + simpa only [h_ideal] using h_gb })) @@ -1226,8 +1228,7 @@ elab "base" : tactic => do have h_ideal : Ideal.span ($basis_term : Set $polyType) = $ideal_term := by -- simp idealeq - simp only [h_ideal] at h_gb - exact h_gb + simpa only [h_ideal] using h_gb })) elab "add_gb_hyp" name:(ident)? G:term : tactic => @@ -1725,7 +1726,8 @@ def evalradicalMembership : Tactic := fun _stx => do syntax (name := GBSolve) "gb_solve" : tactic @[tactic GBSolve] -def evalGBSolve : Tactic := fun stx => do +def evalGBSolve : Tactic := fun stx => + withOptions (fun opts => opts.setBool `backward.isDefEq.respectTransparency false) do let goal ← Lean.Elab.Tactic.getMainGoal let t ← goal.getType let t ← checkTypeQ t q(Prop) @@ -1795,8 +1797,7 @@ def evalGBSolve : Tactic := fun stx => do basis have h_ideal : Ideal.span ($basis_term : Set $polyType) = $ideal_term := by idealeq - simp only [h_ideal] at h_gb - exact h_gb + simpa only [h_ideal] using h_gb })) | ~q($f ∈ Ideal.radical (R := @MvPolynomial $σ $R $i) (Ideal.span $I_gens)) => diff --git a/GroebnerTac/Template.lean b/GroebnerTac/Template.lean index 95a7d9e..0a177db 100644 --- a/GroebnerTac/Template.lean +++ b/GroebnerTac/Template.lean @@ -8,6 +8,8 @@ import GroebnerTac.Tactic In this file we show some templates of using those problem. -/ +set_option backward.isDefEq.respectTransparency false + section open MvPolynomial MonomialOrder @@ -73,7 +75,7 @@ example : all_goals simp only [List.get] rw [← tsub_eq_zero_iff_le, MvPolynomial.SortedRepr.lex_degree_eq] - convert_to _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 + change _ → ¬ SortedFinsupp.toFinsupp _ - SortedFinsupp.toFinsupp x = 0 rw [← SortedFinsupp.toFinsupp_tsub, SortedFinsupp.toFinsupp_eq_zero_iff] decide +kernel +revert @@ -81,7 +83,7 @@ example : example : letI basis := ({X 0 + X 1 ^ 2, X 1 ^ 2} : Set <| MvPolynomial (Fin 3) ℚ) lex.IsGroebnerBasis basis (Ideal.span basis) := by - rw [MonomialOrder.IsGroebnerBasis.isGroebnerBasis_iff_isRemainder_sPolynomial_zero] + rw [MonomialOrder.IsGroebnerBasis.iff_isRemainder_sPolynomial_zero] simp only [Fin.isValue, Subtype.forall, Set.mem_insert_iff, Set.mem_singleton_iff, forall_eq_or_imp, forall_eq, sPolynomial_self] simp only [← Set.range_get_singleton, ← Set.range_get_cons_list] diff --git a/lake-manifest.json b/lake-manifest.json index edd58f9..c8a1894 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,24 +1,24 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/WuProver/MonomialOrderedPolynomial.git", "type": "git", "subDir": null, "scope": "WuProver", - "rev": "821e036784b8e3081fe8aa5797f269625eeed44b", + "rev": "94262b086a817bb6eacefd92c3b87dfc85402a2d", "name": "MonomialOrderedPolynomial", "manifestFile": "lake-manifest.json", - "inputRev": null, + "inputRev": "94262b086a817bb6eacefd92c3b87dfc85402a2d", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/WuProver/groebner_proj", "type": "git", "subDir": null, "scope": "WuProver", - "rev": "c92d123e526cea653f20b66e6d226038fbd7118f", + "rev": "a34921b6a211a8242c3aaf39759a6d48c6b67e67", "name": "groebner", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "a34921b6a211a8242c3aaf39759a6d48c6b67e67", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4export", @@ -31,24 +31,24 @@ "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, - "scope": "", - "rev": "698d2b68b870f1712040ab0c233d34372d4b56df", + "scope": "leanprover-community", + "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc8", - "inherited": true, + "inputRev": "v4.34.1", + "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/doc-gen4", "type": "git", "subDir": null, "scope": "", - "rev": "fbfa185b60c17f8efb9c78863ccf3cf873b6721b", + "rev": "953c8992d174b4e56955e01e101d46668c68f2bb", "name": "«doc-gen4»", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "v4.34.1", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "22a0afa903bcf65285152eea298a3d319badc78d", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead", + "rev": "e928b72544873815af278d38681b31c0293588e3", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,17 +95,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.94", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -115,7 +115,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -125,7 +125,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -135,27 +135,27 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc8", + "inputRev": "v4.34.0", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/kim-em/leansqlite", + {"url": "https://github.com/leanprover/leansqlite", "type": "git", "subDir": null, "scope": "", - "rev": "d14544c72b593af6a66131bc34cdab16bf7c0940", + "rev": "f9cdb9eacb5c8b8ecc02ee9fd9e568d7d28c1416", "name": "leansqlite", "manifestFile": "lake-manifest.json", - "inputRev": "suppress-reducibility-warning", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, "scope": "", - "rev": "629254926fb54ef83d582bd41a0b9eb72b934015", + "rev": "0e569d08b6443ce0908d356884c765397253e2f0", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -165,21 +165,22 @@ "type": "git", "subDir": null, "scope": "", - "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "rev": "4d8616fd4870d0a3453d845770833eac7951fe1c", "name": "BibtexQuery", "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", + "inputRev": "master", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/acmepjz/md4lean", "type": "git", "subDir": null, "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "rev": "31907cc18f48a95384f99cee5582c00fb39e0f67", "name": "MD4Lean", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}], "name": "GroebnerTac", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index 8acb342..4ce3d9f 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -10,21 +10,22 @@ relaxedAutoImplicit = false weak.linter.mathlibStandardSet = true maxSynthPendingDepth = 3 -# [[require]] -# name = "mathlib" -# scope = "leanprover-community" -# rev = "v4.24.0-rc1" +[[require]] +name = "MonomialOrderedPolynomial" +git = "https://github.com/WuProver/MonomialOrderedPolynomial.git" +scope = "WuProver" +rev = "94262b086a817bb6eacefd92c3b87dfc85402a2d" [[require]] name = "groebner" -# git = "https://github.com/WuProver/groebner_proj.git" +git = "https://github.com/WuProver/groebner_proj" scope = "WuProver" -# rev = "main" +rev = "a34921b6a211a8242c3aaf39759a6d48c6b67e67" [[require]] -name = "MonomialOrderedPolynomial" -git = "https://github.com/WuProver/MonomialOrderedPolynomial.git" -scope = "WuProver" +name = "mathlib" +scope = "leanprover-community" +rev = "v4.34.1" [[lean_lib]] name = "GroebnerTac" diff --git a/lean-toolchain b/lean-toolchain index b58ff4f..ba8ebf2 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc8 \ No newline at end of file +leanprover/lean4:v4.34.1 From 5e0e98e7b60aaf5ca79ba852b10825f435d15118 Mon Sep 17 00:00:00 2001 From: tsuki8 <3118181069@qq.com> Date: Fri, 2 Oct 2026 12:05:37 +0800 Subject: [PATCH 2/2] Adapt proof templates and budget the rational remainder example --- GroebnerTac/Example.lean | 1 + GroebnerTac/Template.lean | 19 ++----------------- 2 files changed, 3 insertions(+), 17 deletions(-) diff --git a/GroebnerTac/Example.lean b/GroebnerTac/Example.lean index 8cde068..7b4b9d8 100644 --- a/GroebnerTac/Example.lean +++ b/GroebnerTac/Example.lean @@ -69,6 +69,7 @@ example : (- C (2/9 : ℚ) * X 1) := by gb_solve +set_option maxHeartbeats 800000 in example : lex.IsRemainder (X 0 ^ 2 + X 1 ^ 2 : MvPolynomial (Fin 3) ℚ) {X 0 + C (1/2 : ℚ) * X 1} diff --git a/GroebnerTac/Template.lean b/GroebnerTac/Template.lean index 0a177db..01ce4a8 100644 --- a/GroebnerTac/Template.lean +++ b/GroebnerTac/Template.lean @@ -165,7 +165,7 @@ example: lex.IsGroebnerBasis basis (Ideal.span basis) := by basis have h_ideal : Ideal.span ({X 1^3 - X 2^2, X 0^2 - X 1, X 0*X 1 - X 2, X 0*X 2 - X 1^2} : Set <| MvPolynomial (Fin 3) ℚ) = Ideal.span ({X 0^2 - X 1, X 0^3 - X 2} : Set <| MvPolynomial (Fin 3) ℚ) := by - ideal + idealeq simp [h_ideal] at h_gb exact h_gb @@ -299,22 +299,7 @@ example : have t₂: (1 - X 2) ∈ Ideal.span ({1-X 2} : Set (MvPolynomial (Fin 3) ℚ)) := by exact Ideal.mem_span_singleton_self (1 - X 2) exact t₁ t₂ - rw [h₁] - apply Ideal.add_mem _ l₁ l₂ - rw [← h₁] - refine ⟨Ideal.span {1 - X 2, X 0, X 1}, ?_⟩ - ext x - constructor - · intro h - simp at h - have l: ({1 - X 2, X 0, X 1} : Set (MvPolynomial (Fin 3) ℚ)) ⊆ (Ideal.span ({1 - X 2, X 0, X 1} : Set (MvPolynomial (Fin 3) ℚ))) := by - exact Ideal.subset_span - exact h l - · intro h - simp - intro a - simp at h - exact h + simpa only [← h₁] using (Ideal.add_mem _ l₁ l₂) have h₄ : lex.IsRemainder (1: MvPolynomial (Fin 3) ℚ) {1 - X 2, X 0, X 1} 1 := by remainder