Skip to content

Commit 3befeaf

Browse files
tsuki8tsuki8
committed
change this to 4.28
1 parent 2a4ebbc commit 3befeaf

15 files changed

Lines changed: 719 additions & 256 deletions

‎GroebnerTac.lean‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1 @@
11
import Mathlib
2-
import GroebnerTac.Example
3-
import GroebnerTac.Application
4-
import GroebnerTac.Lemma
5-
import GroebnerTac.Problem
6-
import GroebnerTac.Template
7-
import GroebnerTac.Tactic
8-

‎GroebnerTac/Application.lean‎

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,8 @@
11
import Mathlib
22

3-
import Groebner.Basic
4-
import Groebner.List
5-
-- import Groebner.Lemma
6-
7-
import MonomialOrderedPolynomial.TreeRepr
8-
import MonomialOrderedPolynomial.SortedAddMonoidAlgebra
9-
import MonomialOrderedPolynomial.Ordering
10-
import MonomialOrderedPolynomial.MvPolynomial
11-
import MonomialOrderedPolynomial.Polynomial
3+
import MonomialOrderedPolynomial
4+
import Groebner.Groebner
5+
import Groebner.ToMathlib.List
126

137
import GroebnerTac.Tactic
148

‎GroebnerTac/Example.lean‎

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,6 @@
1-
import Groebner.Basic
2-
import Groebner.List
3-
4-
import MonomialOrderedPolynomial.TreeRepr
5-
import MonomialOrderedPolynomial.SortedAddMonoidAlgebra
6-
import MonomialOrderedPolynomial.Ordering
71
import MonomialOrderedPolynomial.MvPolynomial
8-
import MonomialOrderedPolynomial.Polynomial
9-
2+
import Groebner.Groebner
3+
import Groebner.ToMathlib.List
104
import GroebnerTac.Tactic
115

126
/-!

‎GroebnerTac/HighdimSystem.lean‎

Lines changed: 0 additions & 39 deletions
This file was deleted.

‎GroebnerTac/Lemma.lean‎

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,10 @@
11
import Mathlib
22

3-
import Groebner.Basic
4-
import Groebner.List
5-
import GroebnerTac.Tactic
6-
7-
import MonomialOrderedPolynomial.TreeRepr
8-
import MonomialOrderedPolynomial.SortedAddMonoidAlgebra
9-
import MonomialOrderedPolynomial.Ordering
103
import MonomialOrderedPolynomial.MvPolynomial
11-
import MonomialOrderedPolynomial.Polynomial
4+
import Groebner.Groebner
5+
import Groebner.ToMathlib.List
6+
7+
import GroebnerTac.Tactic
128

139
open MvPolynomial
1410

‎GroebnerTac/NewExample.lean‎

Lines changed: 295 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,295 @@
1+
import MonomialOrderedPolynomial
2+
import Groebner.Groebner
3+
import Groebner.ToMathlib.List
4+
5+
import GroebnerTac.Tactic
6+
7+
/-!
8+
In this file we show some examples of using our tactic.
9+
-/
10+
11+
section
12+
open MvPolynomial MonomialOrder
13+
14+
set_option linter.unusedSimpArgs false in
15+
set_option linter.unreachableTactic false in
16+
set_option linter.unusedTactic false in
17+
18+
set_option synthInstance.maxSize 100000000
19+
20+
open MvPolynomial
21+
variable {σ : Type*} (m : MonomialOrder σ)
22+
23+
/- The test example of basis -/
24+
example :
25+
letI basis := ({X 0 + X 1 ^ 2, X 1 ^ 2} : Set <| MvPolynomial (Fin 3) ℚ)
26+
lex.IsGroebnerBasis basis (Ideal.span basis) := by
27+
gb_solve
28+
29+
example :
30+
letI basis := ({X 0 ^ 4 - X 1} : Set <| MvPolynomial (Fin 3) ℚ)
31+
lex.IsGroebnerBasis basis (Ideal.span basis) := by
32+
gb_solve
33+
34+
example :
35+
letI basis := ({X 0} : Set <| MvPolynomial (Fin 3) ℚ)
36+
lex.IsGroebnerBasis basis (Ideal.span basis) := by
37+
gb_solve
38+
39+
40+
/- The test example of basis'-/
41+
set_option maxHeartbeats 20000000 in
42+
example :
43+
lex.IsGroebnerBasis
44+
({X 1^3 - X 2^2, X 0^2 - X 1, X 0*X 1 - X 2, X 0*X 2 - X 1^2} :
45+
Set <| MvPolynomial (Fin 3) ℚ)
46+
(Ideal.span ({X 0^2 - X 1, X 0^3 - X 2} :
47+
Set <| MvPolynomial (Fin 3) ℚ)):= by
48+
basis'
49+
50+
51+
example :
52+
lex.IsGroebnerBasis
53+
({X 0 - 1, X 1^2} : Set <| MvPolynomial (Fin 2) ℚ)
54+
(Ideal.span ({X 0^2 + X 1^2 - 1, X 0 - 1} : Set <| MvPolynomial (Fin 2) ℚ)) := by
55+
basis'
56+
57+
example :
58+
lex.IsGroebnerBasis
59+
({1} : Set <| MvPolynomial (Fin 3) ℚ)
60+
(Ideal.span ({X 0, 1 - X 0} : Set <| MvPolynomial (Fin 3) ℚ)) := by
61+
basis'
62+
63+
example :
64+
lex.IsGroebnerBasis
65+
({X 0 ^ 2 - 1} : Set <| MvPolynomial (Fin 2) ℚ)
66+
(Ideal.span ({X 0 ^ 2 - 1, (X 0 ^ 2 - 1) * (X 1 + 1)} :
67+
Set <| MvPolynomial (Fin 2) ℚ)) := by
68+
basis'
69+
70+
set_option maxHeartbeats 20000000 in
71+
example :
72+
lex.IsGroebnerBasis
73+
({X 0 - X 3, X 1 - X 3, X 2 - X 3} : Set <| MvPolynomial (Fin 4) ℚ)
74+
(Ideal.span ({X 0 - X 1, X 1 - X 2, X 2 - X 3} :
75+
Set <| MvPolynomial (Fin 4) ℚ)) := by
76+
basis'
77+
78+
example :
79+
lex.IsGroebnerBasis
80+
({X 0 - C (1/2 : ℚ)} : Set <| MvPolynomial (Fin 1) ℚ)
81+
(Ideal.span ({2 * X 0 - 1} : Set <| MvPolynomial (Fin 1) ℚ)) := by
82+
basis'
83+
84+
example :
85+
lex.IsGroebnerBasis
86+
({X 1 + 6} : Set <| MvPolynomial (Fin 2) ℚ)
87+
(Ideal.span ({C (2/3 : ℚ) * X 1 + 4} : Set <| MvPolynomial (Fin 2) ℚ)) := by
88+
basis'
89+
90+
91+
example : lex.IsGroebnerBasis ({X 0, X 1} :
92+
Set (MvPolynomial (Fin 3) ℚ)) (Ideal.span {X 0, X 0 + X 1}) := by
93+
add_gb_hyp h ({X 0, X 0 + X 1} : Set (MvPolynomial (Fin 3) ℚ))
94+
simp at h
95+
exact h
96+
97+
-- cyclic-2
98+
example :
99+
lex.IsGroebnerBasis
100+
({X 0 + X 1, X 1 ^ 2 + 1} : Set <| MvPolynomial (Fin 2) ℚ)
101+
(Ideal.span ({X 0 + X 1, X 0 * X 1 - 1} : Set <| MvPolynomial (Fin 2) ℚ)) := by
102+
add_gb_hyp h ({X 0 + X 1, X 0 * X 1 - 1} : Set (MvPolynomial (Fin 2) ℚ))
103+
simp at h
104+
exact h
105+
106+
-- cyclic-3
107+
set_option maxHeartbeats 20000000 in
108+
example :
109+
letI inputs := ({X 0 + X 1 + X 2,
110+
X 0 * X 1 + X 1 * X 2 + X 2 * X 0,
111+
X 0 * X 1 * X 2 - 1} : Set <| MvPolynomial (Fin 3) ℚ)
112+
∃ (G : Set <| MvPolynomial (Fin 3) ℚ),
113+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
114+
add_gb_hyp h ({X 0 + X 1 + X 2,
115+
X 0 * X 1 + X 1 * X 2 + X 2 * X 0,
116+
X 0 * X 1 * X 2 - 1} : Set <| MvPolynomial (Fin 3) ℚ)
117+
exact
118+
Exists.intro _ h
119+
120+
-- cyclic-4
121+
set_option maxHeartbeats 200000000 in
122+
example :
123+
letI inputs := ({X 0 + X 1 + X 2 + X 3,
124+
X 0*X 1 + X 1*X 2 + X 2*X 3 + X 3*X 0,
125+
X 0*X 1*X 2 + X 1*X 2*X 3 + X 2*X 3*X 0 + X 3*X 0*X 1,
126+
X 0*X 1*X 2*X 3 - 1} : Set <| MvPolynomial (Fin 4) ℚ)
127+
∃ (G : Set <| MvPolynomial (Fin 4) ℚ),
128+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
129+
set_option synthInstance.maxSize 1024 in add_gb_hyp h ({X 0 + X 1 + X 2 + X 3,
130+
X 0*X 1 + X 1*X 2 + X 2*X 3 + X 3*X 0,
131+
X 0*X 1*X 2 + X 1*X 2*X 3 + X 2*X 3*X 0 + X 3*X 0*X 1,
132+
X 0*X 1*X 2*X 3 - 1} : Set <| MvPolynomial (Fin 4) ℚ)
133+
exact
134+
Exists.intro _ h
135+
136+
-- cyclic-5
137+
-- set_option maxHeartbeats 5000000000 in
138+
-- set_option maxRecDepth 500000000 in
139+
-- lemma cyclic5:
140+
-- letI inputs := ({
141+
-- X 0 + X 1 + X 2 + X 3 + X 4,
142+
-- X 0*X 1 + X 1*X 2 + X 2*X 3 + X 3*X 4 + X 4*X 0,
143+
-- X 0*X 1*X 2 + X 1*X 2*X 3 + X 2*X 3*X 4 + X 3*X 4*X 0 + X 4*X 0*X 1,
144+
-- X 0*X 1*X 2*X 3 + X 1*X 2*X 3*X 4 + X 2*X 3*X 4*X 0 + X 3*X 4*X 0*X 1 + X 4*X 0*X 1*X 2,
145+
-- X 0*X 1*X 2*X 3*X 4 - 1
146+
-- } : Set <| MvPolynomial (Fin 5) ℚ)
147+
-- ∃ (G : Set <| MvPolynomial (Fin 5) ℚ),
148+
-- lex.IsGroebnerBasis G (Ideal.span inputs) := by
149+
-- set_option synthInstance.maxSize 1024 in add_gb_hyp h ({
150+
-- X 0 + X 1 + X 2 + X 3 + X 4,
151+
-- X 0*X 1 + X 1*X 2 + X 2*X 3 + X 3*X 4 + X 4*X 0,
152+
-- X 0*X 1*X 2 + X 1*X 2*X 3 + X 2*X 3*X 4 + X 3*X 4*X 0 + X 4*X 0*X 1,
153+
-- X 0*X 1*X 2*X 3 + X 1*X 2*X 3*X 4 + X 2*X 3*X 4*X 0 + X 3*X 4*X 0*X 1 + X 4*X 0*X 1*X 2,
154+
-- X 0*X 1*X 2*X 3*X 4 - 1
155+
-- } : Set <| MvPolynomial (Fin 5) ℚ)
156+
-- exact
157+
-- Exists.intro _ h
158+
159+
-- #print axioms cyclic5
160+
161+
example :
162+
letI inputs := ({X 0 - C (2/3 : ℚ), X 1 + C (4/5 : ℚ)}: Set <| MvPolynomial (Fin 2) ℚ)
163+
∃ (G : Set <| MvPolynomial (Fin 2) ℚ),
164+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
165+
add_gb_hyp h ({X 0 - C (2/3 : ℚ), X 1 + C (4/5 : ℚ)} : Set <| MvPolynomial (Fin 2) ℚ)
166+
exact
167+
Exists.intro
168+
{0 + C (1 / 1) * X 0 ^ 1 + C (-2 / 3), 0 + C (1 / 1) * X 1 ^ 1 + C (4 / 5)} h
169+
170+
-- Katsura-1
171+
example :
172+
letI inputs := ({
173+
X 0 + 2 * X 1 - 1,
174+
X 0^2 - X 0 + 2 * X 1^ 2
175+
} : Set <| MvPolynomial (Fin 2) ℚ)
176+
∃ (G : Set <| MvPolynomial (Fin 2) ℚ),
177+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
178+
179+
set_option synthInstance.maxSize 1024 in add_gb_hyp h ({
180+
X 0 + 2 * X 1 - 1,
181+
X 0^2 - X 0 + 2 * X 1^ 2
182+
} : Set <| MvPolynomial (Fin 2) ℚ)
183+
exact
184+
Exists.intro _ h
185+
186+
187+
188+
-- Katsura-2
189+
set_option maxHeartbeats 2000000 in
190+
example :
191+
letI inputs := ({
192+
X 0 + 2 * X 1 + 2 * X 2 - 1,
193+
X 0^2 + 2 * X 1^2 + 2 * X 2^2 - X 0,
194+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1
195+
} : Set <| MvPolynomial (Fin 3) ℚ)
196+
∃ (G : Set <| MvPolynomial (Fin 3) ℚ),
197+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
198+
199+
set_option synthInstance.maxSize 1024 in add_gb_hyp h ({
200+
X 0 + 2 * X 1 + 2 * X 2 - 1,
201+
X 0^2 + 2 * X 1^2 + 2 * X 2^2 - X 0,
202+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1
203+
} : Set <| MvPolynomial (Fin 3) ℚ)
204+
exact
205+
Exists.intro _ h
206+
207+
-- Katsura-3
208+
set_option maxHeartbeats 2000000 in
209+
example :
210+
letI inputs := ({
211+
X 0 + 2 * X 1 + 2 * X 2 + 2 * X 3 - 1,
212+
X 0^2 - X 0 + 2 * X 1^2 + 2 * X 2^2 + 2* X 3^2,
213+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1 + 2 * X 2 * X 3,
214+
2*X 0*X 2 + X 1^2 + 2*X 1*X 3 - X 2
215+
} : Set <| MvPolynomial (Fin 3) ℚ)
216+
∃ (G : Set <| MvPolynomial (Fin 3) ℚ),
217+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
218+
219+
set_option synthInstance.maxSize 1024 in add_gb_hyp h ({
220+
X 0 + 2 * X 1 + 2 * X 2 + 2 * X 3 - 1,
221+
X 0^2 - X 0 + 2 * X 1^2 + 2 * X 2^2 + 2* X 3^2,
222+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1 + 2 * X 2 * X 3,
223+
2*X 0*X 2 + X 1^2 + 2*X 1*X 3 - X 2
224+
} : Set <| MvPolynomial (Fin 3) ℚ)
225+
exact
226+
Exists.intro _ h
227+
228+
-- Katsura-4
229+
set_option maxHeartbeats 5000000 in
230+
example :
231+
letI inputs := ({
232+
X 0 + 2 * X 1 + 2 * X 2 + 2 * X 3 + 2 * X 4 - 1,
233+
X 0^2 - X 0 + 2 * X 1^2 + 2 * X 2^2 + 2 * X 3^2 + 2 * X 4^2,
234+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1 + 2 * X 2 * X 3 + 2 * X 3 * X 4,
235+
2 * X 0 * X 2 + X 1^2 + 2 * X 1 * X 3 + 2 * X 2 * X 4 - X 2,
236+
2 * X 0 * X 3 + 2 * X 1 * X 2 + 2 * X 1 * X 4 - X 3
237+
} : Set <| MvPolynomial (Fin 5) ℚ)
238+
∃ (G : Set <| MvPolynomial (Fin 5) ℚ),
239+
lex.IsGroebnerBasis G (Ideal.span inputs) := by
240+
241+
set_option synthInstance.maxSize 1024 in add_gb_hyp h ({
242+
X 0 + 2 * X 1 + 2 * X 2 + 2 * X 3 + 2 * X 4 - 1,
243+
X 0^2 - X 0 + 2 * X 1^2 + 2 * X 2^2 + 2 * X 3^2 + 2 * X 4^2,
244+
2 * X 0 * X 1 + 2 * X 1 * X 2 - X 1 + 2 * X 2 * X 3 + 2 * X 3 * X 4,
245+
2 * X 0 * X 2 + X 1^2 + 2 * X 1 * X 3 + 2 * X 2 * X 4 - X 2,
246+
2 * X 0 * X 3 + 2 * X 1 * X 2 + 2 * X 1 * X 4 - X 3
247+
} : Set <| MvPolynomial (Fin 5) ℚ)
248+
249+
exact
250+
Exists.intro _ h
251+
252+
example :
253+
Ideal.span ({X 0 + X 1^2, X 1 }) =
254+
Ideal.span ({X 0, X 1 } : Set (MvPolynomial (Fin 3) ℚ)) := by
255+
ideal
256+
257+
example :
258+
Ideal.span ({X 0 + X 1^ 2, X 1 ^ 2}) =
259+
Ideal.span ({X 0, X 1 ^ 2} : Set (MvPolynomial (Fin 3) ℚ)) := by
260+
ideal
261+
262+
example :
263+
Ideal.span ({2 * X 0 - 1} : Set (MvPolynomial (Fin 3) ℚ)) =
264+
Ideal.span ({X 0 - C (1/2 : ℚ)}) := by
265+
ideal
266+
267+
example :
268+
Ideal.span ({C (1/3 : ℚ) * X 0 + C (2/3 : ℚ)} : Set (MvPolynomial (Fin 3) ℚ)) =
269+
Ideal.span ({X 0 + 2}) := by
270+
ideal
271+
272+
example :
273+
Ideal.span ({X 0 ^ 2 - C (1/4 : ℚ), X 0 - C (1/2 : ℚ)} : Set (MvPolynomial (Fin 3) ℚ)) =
274+
Ideal.span ({X 0 - C (1/2 : ℚ)}) := by
275+
ideal
276+
277+
example :
278+
Ideal.span ({C (1/2 : ℚ) * X 0 + C (1/2 : ℚ), C (1/2 : ℚ) * X 0 - C (1/2 : ℚ)} : Set (MvPolynomial (Fin 3) ℚ)) =
279+
Ideal.span ({1}) := by
280+
ideal
281+
282+
example :
283+
Ideal.span ({
284+
X 0 + X 1 + X 2,
285+
X 0 * X 1 + X 1 * X 2 + X 2 * X 0,
286+
X 0 * X 1 * X 2 - 1
287+
} : Set (MvPolynomial (Fin 3) ℚ)) =
288+
Ideal.span ({
289+
X 0 + X 1 + X 2,
290+
X 0 ^ 2 + X 1 ^ 2 + X 2 ^ 2,
291+
X 0 * X 1 * X 2 - 1
292+
} : Set (MvPolynomial (Fin 3) ℚ)) := by
293+
ideal
294+
295+
end

0 commit comments

Comments
 (0)