Craig Alan Feinstein (Dec 22 2024 at 00:49): Craig Alan Feinstein (Dec 22 2024 at 00:49):I tried the following lemma in Isabelle:
lemma induction_step:
assumes "a ∈ ℕ" "b ∈ ℕ" "c ∈ ℕ" "d ∈ ℕ"
"x0 ∈ ℚ" "x1 ∈ ℚ" "x2 ∈ ℚ" "x3 ∈ ℚ"
"a^2 + b^2 + c^2 + d^2 = 𝗄 - Λ"
"x ∈ rat mat 𝗏 1" "𝗏 > 3" "m > 3" "x0 = x $$ (0,0)"
"x1 = x $$ (1,0)" "x2 = x $$ (2,0)" "x3 = x $$ (3,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 ∈ ℚ"
"(a ∈ ℕ ∧ b ∈ ℕ ∧ c ∈ ℕ ∧ d ∈ ℕ ∧
x0 ∈ ℚ ∧ x1 ∈ ℚ ∧ x2 ∈ ℚ ∧ x3 ∈ ℚ ∧
(a^2 + b^2 + c^2 + d^2 = 𝗄 - Λ) ∧
x ∈ rat mat 𝗏 1 ∧ 𝗏 > 3 ∧ m > 3 ∧ x0 = x $$ (0,0) ∧
x1 = x $$ (1,0) ∧ x2 = x $$ (2,0) ∧ x3 = x $$ (3,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 ∈ ℚ) ⟶
(∑i ∈ {0..<m}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2) +
y0^2 + y1^2 + y2^2 + y3^2"
shows "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,1)) * x $$ (h,0))^2 +
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,2)) * x $$ (h,0))^2 +
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,3)) * x $$ (h,0))^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
proof -
let ?L0 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
let ?L1 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,1)) * x $$ (h,0))"
let ?L2 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,2)) * x $$ (h,0))"
let ?L3 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,3)) * x $$ (h,0))"
have sumdef: "(∑i ∈ {0..<4}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
?L0^2 + ?L1^2 + ?L2^2 + ?L3^2"
by (simp add: numeral.simps(2,3))
have split: "{0..<m} = {0..<4} ∪ {4..<m}" using assms(12) by auto
have inter: "{} = {0..<4} ∩ {4..<m}" by auto
have "(∑i ∈ {0..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
(∑i ∈ {0..<4}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2)"
using split inter sum.union_disjoint[of "{0..<4}" "{4..<m}" "λ i .
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2"]
by (metis (no_types, lifting) finite_atLeastLessThan)
then have lhs: "(∑i ∈ {0..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
?L0^2 + ?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2)"
using sumdef by simp
have "∃e00 e01 e02 e03 :: rat. ?L0 =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
using linear_comb_of_y0_part_2 assms(1-24) by auto
then obtain e00 e01 e02 e03 where lin_comb_key_0:
"?L0 = e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
by fast
assume zero_assump: "y0 = (if e00 = 1 then -(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)))/2 else
(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)))/(1-e00))"
have first_fact: "y0^2 = ?L0^2"
proof (cases "e00 = 1")
case True
then have "y0 = -(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))) / 2"
using zero_assump by auto
then have "-y0 = y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
by auto
then have "(-y0)^2 = (y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
by argo
then have eq: "y0^2 = (e00* y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
using True by auto
have "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)) =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
using lin_comb_key_0 by simp
then have "y0^2 = (∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))^2"
using eq by simp
then show ?thesis
using eq by simp
next
case False
then have "y0 = (e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))) / (1 - e00)"
using zero_assump by auto
then have "(1 - e00) * y0 = e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
using False by auto
then have "y0 = e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
by (simp add: algebra_simps)
then have eq: "(y0)^2 = (e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
by argo
have "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)) =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
using lin_comb_key_0 by simp
then have "y0^2 = (∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))^2"
using eq by simp
then show ?thesis
by (simp add: algebra_simps)
qed
have "(∑i ∈ {0..<m}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2) +
y0^2 + y1^2 + y2^2 + y3^2"
using assms(1-25) zero_assump by simp
then have split_eq: "?L0^2 + ?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y0^2 + y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
using lhs by simp
then have "?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
using split_eq first_fact by simp
thus ?thesis by simp
qed
Isabelle accepted every step of the proof except for the last line "thus ?thesis by simp", even though the line before that is identical to the thesis. The error message was, "Illegal application of proof command in "state" mode" and "Result contains obtained parameters: e03 e02 e01 e00" and "Local statement fails to refine any pending goal". I assume this has to do with the fact that I used "assume" in the proof. I had anticipated that Isabelle would have problems with this in my first post "Peculiar feature of the proof of the Bruck Ryser Chowla thm". And I was right unfortunately. I'm not sure how to get Isabelle to recognize that it is a valid proof even though it is peculiar - the thesis doesn't say anything about y0, even though the proof assumes that y0 is a specific linear combination of the other y variables. Therefore, the assumption is irrelevant to whether the lemma is correct.
Any explanations or ideas?
Craig Alan Feinstein (Dec 22 2024 at 05:07):I’m starting to think perhaps I should rewrite the thesis instead as “there exists y1 y2 y3 and vector x such that ….” Since the thesis is correct only with the assumption in my proof.
Craig Alan Feinstein (Dec 22 2024 at 05:15):But there is a problem with this - I can’t repeat the induction step to get rid of y1, y2, y3, etc. with this strategy. So I am at a loss as to what to do next.
Craig Alan Feinstein (Dec 22 2024 at 17:53):Thinking about this more perhaps the answer is putting the assume part in the initial assumption.
Mathias Fleury (Dec 22 2024 at 18:22):Craig Alan Feinstein said:
And I was right unfortunately. I'm not sure how to get Isabelle to recognize that it is a valid proof even though it is peculiar - the thesis doesn't say anything about y0, even though the proof assumes that y0 is a specific linear combination of the other y variables. Therefore, the assumption is irrelevant to whether the lemma is correct.
Any explanations or ideas?
y0. So why not use the keyword define? Mathias Fleury (Dec 22 2024 at 18:25):Also your theorem is a mess currently. At least you could:
Mathias Fleury (Dec 22 2024 at 18:32):Remark that you did not follow the suggested proof pattern from Fabian. Why?
Mathias Fleury (Dec 22 2024 at 18:41):At least from what I can see here, there are assumption on y0
Mathias Fleury (Dec 22 2024 at 18:42):So it is not a free variable as you suggested in the other thread
Craig Alan Feinstein (Dec 22 2024 at 23:55):My idea to put the assume part in the assumptions worked. Isabelle recognizes the lemma proof as valid.
lemma induction_step:
assumes "a ∈ ℕ" "b ∈ ℕ" "c ∈ ℕ" "d ∈ ℕ"
"x0 ∈ ℚ" "x1 ∈ ℚ" "x2 ∈ ℚ" "x3 ∈ ℚ"
"a^2 + b^2 + c^2 + d^2 = 𝗄 - Λ"
"x ∈ rat mat 𝗏 1" "𝗏 > 3" "m > 3" "x0 = x $$ (0,0)"
"x1 = x $$ (1,0)" "x2 = x $$ (2,0)" "x3 = x $$ (3,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 ∈ ℚ"
"(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)) =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
"y0 = (if e00 = 1 then -(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)))/2 else
(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)))/(1-e00))"
"(a ∈ ℕ ∧ b ∈ ℕ ∧ c ∈ ℕ ∧ d ∈ ℕ ∧
x0 ∈ ℚ ∧ x1 ∈ ℚ ∧ x2 ∈ ℚ ∧ x3 ∈ ℚ ∧
(a^2 + b^2 + c^2 + d^2 = 𝗄 - Λ) ∧
x ∈ rat mat 𝗏 1 ∧ 𝗏 > 3 ∧ m > 3 ∧ x0 = x $$ (0,0) ∧
x1 = x $$ (1,0) ∧ x2 = x $$ (2,0) ∧ x3 = x $$ (3,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 ∈ ℚ) ⟶
(∑i ∈ {0..<m}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2) +
y0^2 + y1^2 + y2^2 + y3^2"
shows "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,1)) * x $$ (h,0))^2 +
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,2)) * x $$ (h,0))^2 +
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,3)) * x $$ (h,0))^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
proof -
let ?L0 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
let ?L1 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,1)) * x $$ (h,0))"
let ?L2 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,2)) * x $$ (h,0))"
let ?L3 = "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,3)) * x $$ (h,0))"
have sumdef: "(∑i ∈ {0..<4}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
?L0^2 + ?L1^2 + ?L2^2 + ?L3^2"
by (simp add: numeral.simps(2,3))
have split: "{0..<m} = {0..<4} ∪ {4..<m}" using assms(12) by auto
have inter: "{} = {0..<4} ∩ {4..<m}" by auto
have "(∑i ∈ {0..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
(∑i ∈ {0..<4}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2)"
using split inter sum.union_disjoint[of "{0..<4}" "{4..<m}" "λ i .
(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2"]
by (metis (no_types, lifting) finite_atLeastLessThan)
then have lhs: "(∑i ∈ {0..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
?L0^2 + ?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2)"
using sumdef by simp
have first_fact: "y0^2 = ?L0^2"
proof (cases "e00 = 1")
case True
then have "y0 = -(e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))) / 2"
using assms(26) by auto
then have "-y0 = y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
by auto
then have "(-y0)^2 = (y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
by argo
then have eq: "y0^2 = (e00* y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
using True by auto
have "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)) =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
using assms(25) by simp
then have "y0^2 = (∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))^2"
using eq by simp
then show ?thesis
using eq by simp
next
case False
then have "y0 = (e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))) / (1 - e00)"
using assms(26) by auto
then have "(1 - e00) * y0 = e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
using False by auto
then have "y0 = e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0))"
by (simp add: algebra_simps)
then have eq: "(y0)^2 = (e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int (N $$ (h, 0)) * x $$ (h, 0)))^2"
by argo
have "(∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0)) =
e00 * y0 + e01 * y1 + e02 * y2 + e03 * y3 +
(∑h ∈ {4..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))"
using assms(25) by simp
then have "y0^2 = (∑h ∈ {0..<𝗏}. of_int(N $$ (h,0)) * x $$ (h,0))^2"
using eq by simp
then show ?thesis
by (simp add: algebra_simps)
qed
have "(∑i ∈ {0..<m}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2) +
y0^2 + y1^2 + y2^2 + y3^2"
using assms(1-27) by simp
then have split_eq: "?L0^2 + ?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y0^2 + y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
using lhs by simp
then have "?L1^2 + ?L2^2 + ?L3^2 +
(∑i ∈ {4..<m}. (∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
y1^2 + y2^2 + y3^2 + of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2)"
using split_eq first_fact by simp
thus ?thesis by simp
qed
Thank you Mathias Fleury for your remarks. I now agree with you that the proof does not have the peculiar property that I suggested in the thread, as y0 is not a free variable as I thought in the other thread. Also I agree that the theorem is a mess for readers to read. My goal now is to get my proofs accepted by Isabelle and later I'll worry about making my proofs readable.
Yong Kiam (Dec 23 2024 at 01:21):"My goal now is to get my proofs accepted by Isabelle and later I'll worry about making my proofs readable."
this is surely the wrong way to go for formalized math; even if your proofs are messy, the theorem statements should really not be a mess, both for your own context management and also for others to inspect your results. It is also very difficult (I assume) for @Mathias Fleury and others to figure out what's wrong with your proofs.
Craig Alan Feinstein (Dec 23 2024 at 03:25):Yong Kiam, this particular lemma (along with three other similar lemmas) is central to the proof of the BRC theorem. Everything else in the proof is high school algebra with some linear algebra and elementary number theory. The only way I know of to make it more readable would be to stick this lemma in another lemma, which I just might do. But every assumption is necessary for the lemma to work, even though there are twenty something assumptions. Also anyone who reads the proof in Stinson’s book of the BRC should be able to understand the lemma since it uses the same variable names.
Craig Alan Feinstein (Dec 23 2024 at 03:27):Also the lemma needs to be modified since it only looks at four columns of matrix N instead of all columns. But that shouldn’t be too hard to do.
Craig Alan Feinstein (Dec 23 2024 at 03:34):Also Yong Kiam thank you for your comments.
Yong Kiam (Dec 23 2024 at 04:32):sure, but there are many more things that you can do even in its current state, such as the points @Mathias Fleury has mentioned about defining variables with the defines keyword
just looking quickly, the role of x0 etc. are all just acting as (local) definitions
you only need to define, e.g., x0 = x $$ (0,0) once instead of writing it in every assumption
Craig Alan Feinstein (Dec 23 2024 at 04:51):You mean I can just put “define x0 = x$$(0,0)” in the middle of the proof? That would definitely help to make it more readable.
Yong Kiam (Dec 23 2024 at 04:52):you can write defines as a keyword in the theorem statement, not in the middle of the proof
Yong Kiam (Dec 23 2024 at 04:53):Mathias Fleury said:
Also your theorem is a mess currently. At least you could:
- use defines for abbreviations in your theorem
- think about deduplicating assumptions
^ what I mean following what Mathias has written here would be a good step to clean up your theorem for subsequent use
Craig Alan Feinstein (Dec 23 2024 at 04:53):You mean the assumptions part?
Craig Alan Feinstein (Dec 23 2024 at 04:55):Can you please give an example?
Yong Kiam (Dec 23 2024 at 04:58):lemma foo:
defines "x0 \equiv x $$ (0,0)"
assumes ".... just use x0 in here ..."
Ok thank you.
Mathias Fleury (Dec 23 2024 at 14:43):Yong Kiam said:
"My goal now is to get my proofs accepted by Isabelle and later I'll worry about making my proofs readable."
this is surely the wrong way to go for formalized math; even if your proofs are messy, the theorem statements should really not be a mess, both for your own context management and also for others to inspect your results. It is also very difficult (I assume) for Mathias Fleury and others to figure out what's wrong with your proofs.
I actually tried to run the proof in Isabelle but failed to guess what imports it needed, so I stopped
Mathias Fleury (Dec 23 2024 at 14:48):Craig Alan Feinstein said:
Yong Kiam, this particular lemma (along with three other similar lemmas) is central to the proof of the BRC theorem. Everything else in the proof is high school algebra with some linear algebra and elementary number theory. The only way I know of to make it more readable would be to stick this lemma in another lemma, which I just might do. But every assumption is necessary for the lemma to work, even though there are twenty something assumptions. Also anyone who reads the proof in Stinson’s book of the BRC should be able to understand the lemma since it uses the same variable names.
I have not read the book, but does I doubt that Stinson put everything as an assumption. This for example just looks fishy:
(a ∈ ℕ ∧ b ∈ ℕ ∧ c ∈ ℕ ∧ d ∈ ℕ ∧
x0 ∈ ℚ ∧ x1 ∈ ℚ ∧ x2 ∈ ℚ ∧ x3 ∈ ℚ ∧
(a^2 + b^2 + c^2 + d^2 = 𝗄 - Λ) ∧
x ∈ rat mat 𝗏 1 ∧ 𝗏 > 3 ∧ m > 3 ∧ x0 = x $$ (0,0) ∧
x1 = x $$ (1,0) ∧ x2 = x $$ (2,0) ∧ x3 = x $$ (3,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 ∈ ℚ) ⟶
(∑i ∈ {0..<m}.(∑h ∈ {0..<𝗏}. of_int(N $$ (h,i)) * x $$ (h,0))^2) =
of_int Λ * (∑j ∈ {0..<𝗏}.(x $$ (j, 0)))^2 +
of_int (𝗄 - Λ) * (∑j ∈ {4..<m}. (x $$ (j, 0))^2) +
y0^2 + y1^2 + y2^2 + y3^2
It looks like you are having an induction around and this is the induction hypothesis
Craig Alan Feinstein (Dec 23 2024 at 22:20):I have imports:
theory Bruck_Ryser_Chowla imports
Fishers_Inequality.Fishers_Inequality SumSquares.FourSquares Pell.Pell
begin
The assumptions in my lemma use functions that I defined elsewhere though. I will use the lemma in my induction argument, which I haven't created yet.
Yong Kiam (Dec 24 2024 at 00:38):that is not the problem with your assumptions, rather, you have assumptions like this:
assumes P
assumes "P ⟶ Q"
you can just write that as
assumes P
assumes Q
Yong Kiam, excellent point. That gets rid of almost half of the assumptions without affecting the validity of the proof. Thank you.
Last updated: Feb 28 2025 at 08:24 UTC