Craig Alan Feinstein (Jul 17 2024 at 03:36): Craig Alan Feinstein (Jul 17 2024 at 03:36):The following is the beginning of a short proof of the easier half of the Bruck Ryser Chowla Theorem. It is so short because it uses lots of lemmas that I'm not posting, including power_of_k_minus_lambda_d:
theorem bruck_ryser_chowla_even:
assumes "βn::nat. π = 2 * n"
shows "sqrt(π - Ξ) β β"
proof -
have "(sqrt(π - Ξ))^(π - 1) β β" using power_of_k_minus_lambda_d
by blast
from assms obtain n where "π = 2 * n" by blast
then have "π - 1 = 2 * n - 1" by auto
then have "(sqrt(π - Ξ))^(2 * n - 1) β β" using power_of_k_minus_lambda_d
by presburger
It gives no errors so far, but when I try to show the conclusion from the last line (which is just simple algebra that square root of π - Ξ squared = π - Ξ in conjunction with the fact that k-Ξ is a natural number), I always get lots of problems. Sledgehammer doesn't seem to recognize simple algebra. Any ideas?
Mathias Fleury (Jul 17 2024 at 04:55):First, it is hard to say much without context, but for Ξ = 0, k = 2, and v = 2, your lemma does not hold
Mathias Fleury (Jul 17 2024 at 04:57):Second,
which is just simple algebra that square root of π - Ξ squared = π - Ξ in conjunction with the fact that k-Ξ is a natural number
the proof states (sqrt(π - Ξ))^(2 * n - 1) β ββ¦ when n = 0, there is squared at all. So your reasoning per hand has holes
Mathias Fleury (Jul 17 2024 at 04:58):Third, please put your isabelle code with 3 backquotes to keep the indentation (the code block below the text editing box)
Mathias Fleury (Jul 17 2024 at 05:01):Fourth, the general approach for a proof is:
Craig Alan Feinstein (Jul 17 2024 at 13:32):That is a good point. I thought that since the context of the theorem is a symmetric BIBD, it would assume that lambda > 0, but it probably was not told that. So given my assumptions that I told it, the theorem might not be true. Sledgehammer is almost like magic but it doesnβt prove false statements. Also I tried intermediate steps with no success. Iβll try again with better assumptions.
Mathias Fleury (Jul 17 2024 at 14:30):maybe, I do not know the context of \Lambda
Mathias Fleury (Jul 17 2024 at 14:50):It is very hard to judge what your intermediate steps are.
Mathias Fleury (Jul 17 2024 at 14:52):This is what I got by adding some assumptions within 15min of trying and my (rusty) math knowledge:
lemma
assumes "βn::nat. n>0 β§ π = 2 * n" and
k_ge: "π β₯ Ξ" and
diff_rat: βΉπ - Ξ β ββΊ
shows "sqrt(π - Ξ) β β"
proof -
have eq: "(sqrt(π - Ξ))^(π - 1) β β" sorry
from assms obtain n where "π = 2 * n" "n > 0" by blast
then have "π - 1 = 2 * n - 1" by auto
then have "(sqrt(π - Ξ))^(2 * n - 1) β β"
using eq by auto
then have rat: βΉ(sqrt(π - Ξ))^(2 * n) / (sqrt(π - Ξ)) β ββΊ
by (metis βΉ0 < nβΊ div_by_0 div_less_iff_less_mult mult.commute mult_pos_pos
nonzero_mult_div_cancel_left one_div_two_eq_zero pos2 power_eq_0_iff
power_minus_mult zero_less_diff)
have eq2: βΉ(sqrt(π - Ξ))^(2 * n) / (sqrt(π - Ξ)) = ((π - Ξ))^ n * (1/sqrt(π - Ξ))βΊ
using k_ge
by (simp add: power_mult)
moreover have βΉ(π - Ξ) ^ n β ββΊ
using diff_rat by (simp add: power_mult Rats_mult_iff)
ultimately have βΉ1/sqrt(π - Ξ) β ββΊ
using rat k_ge apply (simp add: power_mult Rats_mult_iff)
by (metis Rats_1 Rats_divide divide_divide_eq_right nonzero_mult_div_cancel_left power_eq_0_iff real_sqrt_zero)
then show ?thesis
by (simp add: divide_inverse)
qed
Side remark: for n = 0, i am not sure if it holds or not, it depends on (sqrt(π - Ξ))^(π - 1) β β means exactly. Currently the exponent is a natural number, meaning that you get X^0 which is not helpful for proving what you want
Mathias Fleury (Jul 17 2024 at 14:57):but I am not sure if this is wanted or not
Craig Alan Feinstein (Jul 17 2024 at 22:11):I just partially put your formulas in before the batteries in my laptop ran out. So far so good. Question - what is the difference between putting statements in quotes ββ¦β and putting statements in <β¦>. I noticed that there is a difference because some of your stuff only works in <β¦>.
Another question - why is your long explanation in purple? It doesnβt like long explanations?
Thank you so much for your help. Is it correct for me to include you in the authorship if and hopefully when this all gets published in the Isabelle archive of formal proofs?
Craig Alan Feinstein (Jul 17 2024 at 22:55):I just got my laptop a charger. Your code worked so I've proven my first major theorem in Isabelle; however, I need to prove the assumptions for it to technically be a proof. One thing I did not know before this is that apparently the definition of a natural number according to Isabelle includes zero.
Craig Alan Feinstein (Jul 17 2024 at 23:19):I modified the code to get a proof without extra assumptions (v even is part of the theorem; v odd is the other part). I put three backward slashes before it, so hopefully it will look better:
\\\theorem bruck_ryser_chowla_even:
assumes "βn::nat. π = 2 * n"
shows "sqrt(π - Ξ) β β"
proof -
have "(sqrt(π - Ξ))^(π - 1) β β" using power_of_k_minus_lambda_3
by blast
from assms obtain n where "π = 2 * n" by blast
then have "π - 1 = 2 * n - 1" by auto
then have "(sqrt(π - Ξ))^(2 * n - 1) β β" using power_of_k_minus_lambda_3
by presburger
then have rat: "(sqrt(π - Ξ))^(2 * n)/sqrt(π - Ξ) β β"
by (metis div_by_0 div_less_iff_less_mult mult.commute
mult_pos_pos nonzero_mult_div_cancel_left one_div_two_eq_zero
pos2 power_eq_0_iff power_minus_mult zero_less_diff)
have eq2: βΉ(sqrt(π - Ξ))^(2 * n) / (sqrt(π - Ξ)) = ((π - Ξ))^ n * (1/sqrt(π - Ξ))βΊ
using k_minus_lambda_is_natural
by (simp add: power_mult)
moreover have βΉ(π - Ξ) ^ n β ββΊ
using k_minus_lambda_is_natural by (simp add: power_mult Rats_mult_iff)
ultimately have βΉ1/sqrt(π - Ξ) β ββΊ
using rat k_minus_lambda_is_natural apply (simp add: power_mult Rats_mult_iff)
by (metis Rats_1 Rats_divide divide_divide_eq_right
nonzero_mult_div_cancel_left power_eq_0_iff real_sqrt_zero)
then show ?thesis
by (simp add: divide_inverse)
qed\\\
Craig Alan Feinstein (Jul 17 2024 at 23:21):I'm sorry, I see you said back quotes. Not sure what that is.
Mathias Fleury (Jul 18 2024 at 05:00):Craig Alan Feinstein said:
Thank you so much for your help. Is it correct for me to include you in the authorship if and hopefully when this all gets published in the Isabelle archive of formal proofs?
just take these few lines as your own that is far from enough to credit me
Mathias Fleury (Jul 18 2024 at 05:01):Craig Alan Feinstein said:
I just partially put your formulas in before the batteries in my laptop ran out. So far so good. Question - what is the difference between putting statements in quotes ββ¦β and putting statements in <β¦>. I noticed that there is a difference because some of your stuff only works in <β¦>.
I prefer the cartouche βΉ...βΊ because I find them nicer to look at, no difference otherwise
Mathias Fleury (Jul 18 2024 at 05:02):Craig Alan Feinstein said:
Another question - why is your long explanation in purple? It doesnβt like long explanations?
That means that the proof is not terminating for you. Probably some theorem that changed meaning in your context (I only imported Complex_Main). Try sledgehammer
Mathias Fleury (Jul 18 2024 at 05:03):Backtick. Click on the ? bottom right of the area where you enter text
Mathias Fleury (Jul 18 2024 at 05:06):Mathias Fleury said:
Craig Alan Feinstein said:
Another question - why is your long explanation in purple? It doesnβt like long explanations?
That means that the proof is not terminating for you. Probably some theorem that changed meaning in your context (I only imported Complex_Main). Try sledgehammer
Ahh you removed the assumption n > 0, so the proof does not hold anymore. See my side remark above
Mathias Fleury (Jul 18 2024 at 05:10):Craig Alan Feinstein said:
I just got my laptop a charger. Your code worked so I've proven my first major theorem in Isabelle; however, I need to prove the assumptions for it to technically be a proof. One thing I did not know before this is that apparently the definition of a natural number according to Isabelle includes zero.
I am not aware of any construction of natural numbers that goes without 0
Mathias Fleury (Jul 18 2024 at 05:11):(I checked wikipedia and there seem to be a debate, but no formal definition listed goes without 0)
Craig Alan Feinstein (Jul 18 2024 at 12:54):Does the purple highlights mean that it doesnβt consider the proof to be valid? Even before I removed the assumptions that n>0, it had purple highlights. Iβm pretty sure based on experimenting yesterday that it considers the natural numbers not to include zero.
Lukas Stevens (Jul 18 2024 at 12:56):Purple highlight means that the method did not terminate yet. If it stays purple, it often means that the proof method loops, e.g. due to a loop of rewriting rules.
Mathias Fleury (Jul 18 2024 at 13:00):Craig Alan Feinstein said:
Iβm pretty sure based on experimenting yesterday that it considers the natural numbers not to include zero.
This is with 100% certainty wrong:
lemma
βΉ0 β ββΊ
by auto
You are correct that 0 is in N. I still get the purple highlights when I copy your exact text and substitute the sorry for my lemma, just as I did when I changed it yesterday. Sledgehammer didn't resolve it. For now, I'm going to leave it alone.
Mathias Fleury (Jul 19 2024 at 05:01): then have "(sqrt(π - Ξ))^(2 * n - 1) β β"
using eq by auto
moreover have βΉ(sqrt(π - Ξ))^(2 * n - 1) = (sqrt(π - Ξ))^(2 * n) / (sqrt(π - Ξ))βΊ
using βΉ0 < nβΊ k_ge by (cases βΉπ - Ξ = 0βΊ) (auto simp: divide_inverse power_diff_conv_inverse)
ultimately have rat: βΉ(sqrt(π - Ξ))^(2 * n) / (sqrt(π - Ξ)) β ββΊ
by simp
(with the rather obvious splitting intermediate step of making the transformation explicit)
Mathias Fleury (Jul 19 2024 at 05:03):(the by (cases ...) (auto ...) is the result of finding power_diff_conv_inverse (with find_theorems) and finding out why auto did not apply it
Craig Alan Feinstein (Jul 19 2024 at 16:44):I have it down to the following:
assumes "βn::nat. π = 2 * n"
shows "sqrt(π - Ξ) β β"
proof -
have "(sqrt(π - Ξ))^(π - 1) β β" using power_of_k_minus_lambda_3
by blast
from assms obtain n where "π = 2 * n" by blast
then have "π - 1 = 2 * n - 1" by auto
then have "(sqrt(π - Ξ))^(2 * n - 1) β β" using power_of_k_minus_lambda_3
by presburger
then have "(sqrt(π - Ξ))^(2 * n)/sqrt(π - Ξ) β β"
by (metis div_by_0 div_less_iff_less_mult)
moreover have βΉ(π - Ξ) ^ n β ββΊ
using k_minus_lambda_is_natural by simp
ultimately have βΉ1/sqrt(π - Ξ) β ββΊ
by (metis divide_divide_eq_right)
then show ?thesis
by (simp add: divide_inverse)
qed?
The lines where I use metis are highlighted purple on my machine. I don't think it matters whether n=0 or not. The theorem should still be true.
Actually now I see that there may by problems with dividing by zero if k= Lambda. This might be causing the problems.
Mathias Fleury (Jul 19 2024 at 19:13):n > 0 makes a ton of a difference
Mathias Fleury (Jul 19 2024 at 19:14):Mathias Fleury said:
Side remark: for n = 0, i am not sure if it holds or not, it depends on
(sqrt(π - Ξ))^(π - 1) β βmeans exactly. Currently the exponent is a natural number, meaning that you getX^0which is not helpful for proving what you want
please reread that sentence
Mathias Fleury (Jul 19 2024 at 19:14):and remember that 0 - 1 = 0
Mathias Fleury (Jul 19 2024 at 19:17):Craig Alan Feinstein said:
Actually now I see that there may by problems with dividing by zero if k= Lambda. This might be causing the problems.
no, it does not. a / 0 = 0 (yes it is surprising; yes it makes sense; please check the mailing list this pops up every year and I am not discussing this here)
Craig Alan Feinstein (Jul 19 2024 at 20:49):I'm going to add the assumption that n > 0 again.
Chelsea Edmonds (Jul 24 2024 at 12:26):Hi @Craig Alan Feinstein , just saw this thread - very happy to see someone else taking up design theory in Isabelle! I was the main author on the original design AFP entry, so feel free to reach out with any questions. Sounds like this one is basically solved, but as some general tips for doing simple algebra on the design parameters. I went back and forth between the parameters being nats vs ints for a while - but based on their definitions (cardinalities of certain sets), nats made more sense and generally reduced the amount of type casting I had to do. Obviously, a lot of proofs on paper rely on integer properties though for algebraic manipulation (as in your case) so we still have to work around it. One tactic that is often really useful is the algebra_simps tactic (this often helps where sledgehammer fails), though it'll still need the right assumptions. Sometimes working with int versions of the parameters when doing a long calculation can also significantly improve automation (see the Boses inequality proof in the Resolvable design theory for a good example).
Craig Alan Feinstein (Jul 24 2024 at 23:43):Hi @Chelsea Edmonds, I've been using a lot of your work on Isabelle Combinatorial Design Theory to try to prove the BRC theorem. I learned of this theorem in college in about 1990 and I liked its creative proof that uses the fact that every integer is the sum of four squares. Also the fact that it uses algebra is a good way for me to learn Isabelle. I'm glad you laid the groundwork for Design Theory, as it would have been difficult for me to do this from scratch. This is my first time working with a proof assistant and it is fun, but sometimes frustrating as I don't always understand the details of what makes a valid proof in Isabelle. May I email you versions of my BRC proof attempt and ask you questions when I get stuck? I ask because I am not sure they want me to post versions of my proof in Zulip.
Chelsea Edmonds (Jul 25 2024 at 09:41):Craig Alan Feinstein said:
Hi Chelsea Edmonds, I've been using a lot of your work on Isabelle Combinatorial Design Theory to try to prove the BRC theorem. I learned of this theorem in college in about 1990 and I liked its creative proof that uses the fact that every integer is the sum of four squares. Also the fact that it uses algebra is a good way for me to learn Isabelle. I'm glad you laid the groundwork for Design Theory, as it would have been difficult for me to do this from scratch. This is my first time working with a proof assistant and it is fun, but sometimes frustrating as I don't always understand the details of what makes a valid proof in Isabelle. May I email you versions of my BRC proof attempt and ask you questions when I get stuck? I ask because I am not sure they want me to post versions of my proof in Zulip.
Glad it's been useful! Your welcome to email me (c.l.edmonds@sheffield.ac.uk), or DM me with any questions about the existing libraries/how to use them effectively/problems specific to design theory. That said, this chat is still a great place to ask general questions about Isabelle proofs/generic errors as you're working and learning about Isabelle too - as you've already been doing! For those types of things more people probably means a better chance at a faster response and also different insights.
Last updated: Dec 21 2024 at 12:33 UTC