Craig Alan Feinstein (Mar 23 2025 at 22:14): Craig Alan Feinstein (Mar 23 2025 at 22:14):I haven't really used Isabelle heavily since last year and I'm just getting back into it now. The good news is I've learned so much since the summer of last year. Last year, someone in Zulip recommended the "fix" operator. I tried using it here but I got a "linarith_split_limited exceeded" error after the last line "by auto":
lemma brc_v_1_mod_4:
assumes "π mod 4 = 1"
shows "βx :: rat mat.(βj β {4..<5}.
((βh β {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
(βh β {5..<π}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
of_nat Ξ * (βj β {0..<π}.(x $$ (j, 0)))^2 +
of_nat (π - Ξ) * (βj β {4..<5}. (x $$ (4-j, 0))^2)"
proof -
obtain a b c d where lag_eq:
"a^2 + b^2 + c^2 + d^2 = π - Ξ"
using blocksize_gt_index sum_of_four_squares by metis
fix m :: "nat"
fix n :: "nat"
fix h :: "nat"
fix i :: "nat"
fix j :: "nat"
fix x :: "rat mat"
fix x0 :: "rat"
fix x1 :: "rat"
fix x2 :: "rat"
fix x3 :: "rat"
fix y0 :: "rat"
fix y1 :: "rat"
fix y2 :: "rat"
fix y3 :: "rat"
assume assm1: "π β₯ m" "m > 3" "x0 = x $$ (m-4,0)"
"x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
"x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
assume assm2: "m + 4*n = π"
have "βe0 e1 e2 e3 :: rat.(βh β {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
(βh β {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"
using linear_comb_of_y_part_2_i3 assm1 lag_eq by auto
Any ideas what could be causing this?
The lemma being used in brc_v_1_mod_4 is the following, which was successfully proven:
lemma linear_comb_of_y_part_2_i3:
assumes "a β β" "b β β" "c β β" "d β β"
"x0 β β" "x1 β β" "x2 β β" "x3 β β"
"a^2 + b^2 + c^2 + d^2 = (π - Ξ)"
"x β rat mat" "π β₯ m" "m > 3" "i β {0..<4}" "x0 = x $$ (m-4,0)"
"x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
"x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"y0 β β" "y1 β β" "y2 β β" "y3 β β"
shows "βe0 e1 e2 e3 :: rat.(βh β {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
(βh β {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"
Another question is what are the advantages of using fix instead of assume? As I recall, one of the experts in Zulip said I should be using fix instead of assume. Could the problem be I should have used fix in linear_comb_of_y_part_2_i3 instead of assume?
Mathias Fleury (Mar 24 2025 at 05:46):fix is just a way to fix a variable. So this:
fix m :: "nat"
assume assm1: "π β₯ m"
just means "let
such that
So the question is not "should I use fix". The question is "how does my proof look like on paper?"
Mathias Fleury (Mar 24 2025 at 05:48):In a proof by hand you would never write an assume in a middle of a proof. So you should not do it in Isabelle either.
Mathias Fleury (Mar 24 2025 at 05:48):Remark that
"x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
look like definitions and not assumptions
Craig Alan Feinstein (Mar 24 2025 at 16:09):Mathias, so all this is just cosmetic? I was hoping this would lead me to figure out why my proof isnβt working. In any case how would you rewrite the assume part in the middle of my proof so it looks cosmetically better?
irvin (Mar 24 2025 at 17:24):I believe that unless you provide a method for others to run your proofs. It would be extremely hard for others to figure out modify/fix your proofs.
Mathias Fleury (Mar 24 2025 at 18:59):it is not a question about cosmetic. It is a question about how the proofs.
Mathias Fleury (Mar 24 2025 at 19:00):On paper, you would never write in the middle a proof "oh and here let's assume that v >= 4".
Mathias Fleury (Mar 24 2025 at 19:00):You need to justify why you can do that
Mathias Fleury (Mar 24 2025 at 19:01):and one why to do that is to say: oh let's just give a name to this thing
Mathias Fleury (Mar 24 2025 at 19:01):this is not an assumption
Mathias Fleury (Mar 24 2025 at 19:02):But, Isabelle is not here to tell you how to do a proof, it is here to check the proof. You have to do the creative part of deciding how to do the proof.
Craig Alan Feinstein (Mar 24 2025 at 22:37):Irvin, even though it looks complicated, the proof of brcv1mod4 follows from the other lemma by modes ponens. But I am having trouble getting Isabelle to recognize this.
Craig Alan Feinstein (Mar 24 2025 at 23:14):Mathias I am putting inside the proof assumptions about variables that are not defined in the actual statement of the lemma. But they are necessary for proving existence in the lemma statement. How would you do this? By the way, this is all part of the last part of the standard proof of the Bruck Ryser Chowla theorem. This isnβt my proof. Iβm just trying to translate it into Isabelle.
Mathias Fleury (Mar 25 2025 at 02:50):A lot of the literature looks like a proof but needs improvement to have a proper proof
Mathias Fleury (Mar 25 2025 at 02:53):So in your case:
But they are necessary for proving existence in the lemma statement.
Why can you assume them? Obviously you cannot assume False in the middle of a proof. So there must be some argument why you can do that
Mathias Fleury (Mar 25 2025 at 02:58):My guess is that:
1. x0 to x4 are actually definitions "x0 = x $$ (m-4,0)" "x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)" (keyword in Isabelle: defines⦠and you do not need a proof to define things!)
2. m and n are actually value you can obtain from π mod 4 = 1 but you pick values such that m>3 intead of the smallest values (keyword in Isabelle: obtainβ¦ and you need a proof!)
3. From 1 you can prove that the alternative definition with one_of ... four_of hold (keyword in Isabelle: have⦠and you need a proof und will use x0_def ... x4_def)
Mathias Fleury (Mar 25 2025 at 03:00):And if I am correct, something just happened: none of the things are assume in the middle of a proof. They have a proper justification. And none of the things are new fresh variables in the middle of a proof that need a fix.
Craig Alan Feinstein (Mar 25 2025 at 16:02):The lemma claims there exist rational numbers which satisfy the equation- v and k and Lambda are properties of the symmetric design. The variables that are assumed and fixed are used to construct the solution.
Craig Alan Feinstein (Mar 25 2025 at 16:21):Are there any other similar existence theorems in Isabelle?
irvin (Mar 25 2025 at 17:12):Here are some examples of using define and obtain.
lemma DEFINE:
assumes n_def:"(n :: nat) = 2"
shows "βy. y * 2 = n"
proof -
define y where y_def: "(y ::nat) = 1"
then have "y * 2 = n"
using y_def n_def by simp
then show "βy. y * 2 = n"
by auto
qed
lemma OBTAIN:
assumes "βy. P y"
shows "βx. P x"
proof -
obtain y where " P y "
using assms by auto
then show "βx. P x"
by auto
qed
Define requires no proof, obtain requires a proof
irvin (Mar 25 2025 at 17:14):Craig Alan Feinstein said:
The lemma claims there exist rational numbers which satisfy the equation- v and k and Lambda are properties of the symmetric design. The variables that are assumed and fixed are used to construct the solution.
in isabelle it would roughly be.
obtain rat1 rat2 rat3 where "property1" "property2"
by proof_method
I would suggest starting with an Isabelle tutorial like the prog-prove (the beginning of the concrete semantics)
Craig Alan Feinstein (Mar 25 2025 at 23:06):Irvin and Mathias, thank you that gives me something to work with.
Craig Alan Feinstein (Mar 26 2025 at 00:18):I just tried the following:
lemma brc_v_1_mod_4:
assumes "π mod 4 = 1"
shows "βx :: rat mat.(βj β {4..<5}.
((βh β {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
(βh β {5..<π}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
of_nat Ξ * (βj β {0..<π}.(x $$ (j, 0)))^2 +
of_nat (π - Ξ) * (βj β {4..<5}. (x $$ (4-j, 0))^2)"
proof -
obtain a b c d where lag_eq:
"a^2 + b^2 + c^2 + d^2 = π - Ξ"
using blocksize_gt_index sum_of_four_squares by metis
fix m :: "nat"
fix n :: "nat"
fix i :: "nat"
fix x :: "rat mat"
define x0 where "(x0 :: rat) = x $$ (m-4,0)"
define x1 where "(x1 :: rat) = x $$ (m-3,0)"
define x2 where "(x2 :: rat) = x $$ (m-2,0)"
define x3 where "(x3 :: rat) = x $$ (m-1,0)"
define n where "(n :: nat) = (π - m) div 4"
fix y0 :: "rat"
fix y1 :: "rat"
fix y2 :: "rat"
fix y3 :: "rat"
assume assm1: "π β₯ m" "m > 3" "i β {0..<4}"
"x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
have "βe0 e1 e2 e3 :: rat.(βh β {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
e0 * y0 + e1 * y1 + e2 * y2 + e3 * y3 +
(βh β {4..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0))"
using linear_comb_of_y_part_2_i3 assm1 lag_eq by auto
Unfortunately, I got a "linarith_split_limit exceeded (current value is 9)" error repeated. The last have statement should follow from "linear_comb_of_y_part_2_i3" in the first post of this thread. It is just modes ponens.
irvin (Mar 26 2025 at 02:42):You're still assuming stuff that I assume you should be proving.
This bit should be have
"x0 = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x1 = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x2 = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x3 = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
In fact brc_v_1_mod_4 should not be using any assume keyword in the whole proof block
Mathias Fleury (Mar 26 2025 at 05:40):BTW isn't linarith_split_limit exceeded just a warning?
Craig Alan Feinstein (Mar 26 2025 at 15:58):Mathias, linarith split limit exceeded was something that kept repeating itself to the point where I couldnβt tell what was happening. When I had my Isabelle in front of me last night I got a purple highlight over auto meaning it was still running without stopping.
Craig Alan Feinstein (Mar 26 2025 at 16:09):Irvin the four equations that you posted are definitely assumptions. Or perhaps better to say definitions, but I donβt know how to make them definitions.
Mathias Fleury (Mar 26 2025 at 19:30):Craig Alan Feinstein said:
Mathias, linarith split limit exceeded was something that kept repeating itself to the point where I couldnβt tell what was happening. When I had my Isabelle in front of me last night I got a purple highlight over auto meaning it was still running without stopping.
could be that the arith simplifier is spamming the interface with messages
Mathias Fleury (Mar 26 2025 at 19:36):Craig Alan Feinstein said:
Irvin the four equations that you posted are definitely assumptions. Or perhaps better to say definitions, but I donβt know how to make them definitions.
One last try: in the world of math I know where proofs are sequences of applications of theorems and axioms, there are no assumptions in the middle of a proof. Never. It just does not make sense.
Apparently we cannot agree on that. Therefore, we cannot help you.
Craig Alan Feinstein (Mar 26 2025 at 22:45):Mathias I am not here to argue with you, but learn from you. But I am coming from the perspective that you can say βassumeβ in a math proof. I learned this as a college freshman from a course in logic - if you want to prove that A implies B, then you can do this by assuming A and then proving B. In the case of the proof of the Bruck Ryser Chowla theorem, the idea is to prove a certain equation 1 has an rational solution. This is done by assuming that the variables in equation 2 satisfy certain conditions and then showing by induction that these conditions lead to a solution in equation 1. This is why I was using assume in the proof. But I really donβt care if you call what I am doing assume or something else. I just want my Isabelle proof to work.
Mathias Fleury (Mar 27 2025 at 05:38):if you want to prove that A implies B, then you can do this by assuming A and then proving B
When you prove that theorem yes. When you use that theorem no. When you use it, you show that A holds. And from this you derive B.
And here you are clearly trying to use it. You even using the keyword using linear_comb_of_y_part_2_i3.
irvin (Mar 27 2025 at 15:01):Also note that its safe to assume .../ without loss of generality assume ... needs to be justified in isabelle.
Craig Alan Feinstein (Mar 27 2025 at 16:17):Ok, now I understand where you are coming from. I have to think about this.
Craig Alan Feinstein (Mar 28 2025 at 00:03):Before today, I thought your arguments were irrelevant semantic arguments. Now I see that yes they are semantic arguments but not irrelevant because in Isabelle, everything is semantics. I reread what you wrote and they make sense now. Thank you.
Craig Alan Feinstein (Apr 03 2025 at 02:45):I've gotten to this point:
lemma brc_v_1_mod_4:
assumes "π mod 4 = 1"
shows "βx :: rat mat.(βj β {4..<5}.
((βh β {0..<5}. of_int(N $$ (4-h,4-j)) * x $$ (4-h,0)) +
(βh β {5..<π}. of_int(N $$ (h,4-j)) * x $$ (h,0)))^2) =
of_nat Ξ * (βj β {0..<π}.(x $$ (j, 0)))^2 +
of_nat (π - Ξ) * (βj β {4..<5}. (x $$ (4-j, 0))^2)"
proof -
obtain a b c d where lag_eq:
"a^2 + b^2 + c^2 + d^2 = π - Ξ"
using blocksize_gt_index sum_of_four_squares by metis
fix h :: "nat"
fix i :: "nat"
fix j :: "nat"
obtain m where "π β₯ m" "m > 3"
using assms t_design_min_v by force
define n where "n = (π-m) div 4"
fix y0 :: "rat"
fix y1 :: "rat"
fix y2 :: "rat"
fix y3 :: "rat"
fix x0 :: "rat"
fix x1 :: "rat"
fix x2 :: "rat"
fix x3 :: "rat"
obtain x where "x $$ (m-4,0) = one_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x $$ (m-3,0) = two_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x $$ (m-2,0) = three_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
"x $$ (m-1,0) = four_of(y_inv_of((a, b, c, d),(y0, y1, y2, y3)))"
by simp
define x0 where "x0 = x $$ (m-4,0)"
define x1 where "x1 = x $$ (m-3,0)"
define x2 where "x2 = x $$ (m-2,0)"
define x3 where "x3 = x $$ (m-1,0)"
The problem with it is I want x to be a rat mat but I'm not sure how to use the obtain statement to do this.
Mathias Fleury (Apr 03 2025 at 04:37):obtain x :: "rat mat" where β¦
Thanks!
Last updated: Apr 03 2025 at 20:22 UTC