Stream: General

Topic: Asking for help

Craig Alan Feinstein (Apr 23 2025 at 02:10):

I've been working on Isabelle since July 2024, trying to prove the Bruck Ryser Chowla theorem as a challenge and a learning exercise. I'm on the last lemma (or maybe second to last), which happens to be the most challenging. I'm wondering if anybody would be willing to take a look at it and give me some suggestions. Thank you in advance.

Yutaka Nagashima (May 07 2025 at 18:18):

@Craig Alan Feinstein
If you haven’t heard from others, it might be a good idea to add a link to your repository so they can see if they’re able to help. :thinking:

Craig Alan Feinstein (May 28 2025 at 13:52):

Where do people usually put their repositories? I don’t have my stuff online.

Yutaka Nagashima (May 29 2025 at 15:44):

I guess:

• https://github.com or/and
• https://gitee.com (especially for people in China)

Mathias Fleury (May 29 2025 at 16:02):

heptapod where the AFP lives deserves to be mentioned too.

Mathias Fleury (May 29 2025 at 16:02):

There are many others (bitbucket, gitlab, ...), but github (and partially gitlab because it can be hosted) are winning

Yutaka Nagashima (Jun 01 2025 at 14:01):

@Craig Alan Feinstein
Unsolicited advice: you should think carefully about which license to use before open-sourcing. :thinking:

Craig Alan Feinstein (Jun 01 2025 at 19:24):

I just created a Github account.

Craig Alan Feinstein (Jun 09 2025 at 00:54):

Yutaka, finally I'm starting to build a repository in Github. What license would you recommend? I ultimately want to get my Bruck Ryser Chowla Theorem proof into the Archive of Formal Proofs. I really don't care if I get help and would be happy to include their names for credit if they want it.

Christian Pardillo Laursen (Jun 10 2025 at 10:07):

From the AFP: "All entries in the Archive of Formal Proofs are licensed under a BSD-style License or the GNU LGPL. This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions."

They're quite similar, I'd say just go with BSD but you should read up a bit on the various software licenses if you're going to make open source contributions.

Craig Alan Feinstein (Jun 10 2025 at 23:12):

Christian, unfortunately I did the MIT license before I read your comment. I can't seem to find a way to change it. In any case, for everyone out there, my name on GitHub is cafeinst and the entry is Bruck_Ryser_Chowla.

Christian Pardillo Laursen (Jun 18 2025 at 15:10):

The MIT license is very permissive so it should be fine, but if you do want to change it you can simply replace the contents of your LICENSE file with the text at this link https://www.isa-afp.org/LICENSE

Christian Pardillo Laursen (Jun 18 2025 at 17:57):

Looking at your theory, I have the following pieces of advice to offer:

• Function "rightside" is simply snd, replacing it might give you some automation benefits.
• In lemmas combine_r_lambda_terms, brc_x_identity, brc_x_equation, you assume x ∈ rat mat, but since this needs to be a type assertion rather than an assumption these lemmas end up with an uninterpreted symbol "rat" which makes the lemmas useless. Replace the assumption with fixes x :: "rat mat"
• In Isar proofs, if you're proving things using ".", often it's better to skip the proof step, since the lemma is readily available anyway.
• It's generally helpful to prove the most general theorem you can, both in terms of types and constants. For example, you prove lambda_all_ones only for your Lambda constant, but it's both simpler and usually better to prove a more general theorem, like:

lemma lambda_all_ones:
  fixes l :: "'b :: {monoid_mult, zero}"
  assumes "h < 𝗏" "j < 𝗏"
  shows "(l ⋅⇩m (J⇩m 𝗏)) $$ (j, h) = l"
  using assms by simp

Craig Alan Feinstein (Jun 20 2025 at 02:41):

Christian, I tried replacing rightside with snd and it worked fine. For the lemmas combine_r_lambda_terms... when I replaced the assumption with fixes x :: "rat mat", I got problems in the proofs. The lambda_all_ones that you suggested worked. My lemma brc_v_1_mod_4 is the one that is giving me the real problems. It is supposed to use brc_x_equation but it has problems.

Christian Pardillo Laursen (Jun 20 2025 at 08:26):

It's understandable that the proofs might break when you fix x :: "rat mat", since it looks like previously the type inference was setting the type of x to "int mat" instead, and the proofs might not be compatible. If you ctrl-hover over the rat term in your brc_x_equation lemma, you'll see that the type inference gave it a very strange type - removing the assumption will improve your odds of making it applicable.

Craig Alan Feinstein (Jun 20 2025 at 14:25):

Christian, I’ll try it. I have absolutely nothing to lose since making the brc_x_equation applicable seems to be the source of my problem.

Mathias Fleury (Jun 20 2025 at 15:50):

  (* We can pick arbitrary h < 𝗏 and j < 𝗏 since they're not used in the conclusion *)
  obtain h j where hj: "h < 𝗏" "j < 𝗏"
    using positive_v by (metis gr0I not_less0)

does not hold for v = 0

Mathias Fleury (Jun 20 2025 at 15:51):

You have many issues with normalization/casting of expression

Mathias Fleury (Jun 20 2025 at 15:51):

variants of the already existing:

lemma complex_of_rat_sum: ‹complex_of_rat (∑h ∈A. f h) = (∑h ∈A. complex_of_rat(f h))›
  using of_rat_hom.hom_sum by blast

lemma rat_of_int_mult: ‹rat_of_int (x * y) = rat_of_int x * rat_of_int y›
  by simp
lemma rat_of_int_sum: ‹rat_of_int (∑h ∈A. f h) = (∑h ∈A. rat_of_int (f h))›
 ‹rat_of_int (∑h=a..b. f h) = (∑h=a..b. rat_of_int (f h))›
 ‹rat_of_int (∑h=a..<b. f h) = (∑h=a..<b. rat_of_int (f h))›
  using of_int_sum by blast+

Mathias Fleury (Jun 20 2025 at 18:45):

linear_comb_of_y_part_2_i3 contains a reference to i in the assumption that is not used in the rest of the statement

Mathias Fleury (Jun 20 2025 at 18:51):

in brc_v_1_mod_4 the first steps can be used like this:

    have x123:"x0 = x $$ (m-4,0)" "x1 = x $$ (m-3,0)" "x2 = x $$ (m-2,0)" "x3 = x $$ (m-1,0)"
      using ineq unfolding x_def by (auto simp: index_mat)
    have "∃e00 e10 e20 e30 :: rat.(∑h ∈ {0..<m}. of_int(N $$ (m-h-1,m-4)) * x $$ (m-h-1,0)) =
          e00 * y0 + e10 * y1 + e20 * y2 + e30 * 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[OF lag_eq ineq x123 x0_def x1_def x2_def x3_def] by auto

Craig Alan Feinstein (Jun 22 2025 at 17:13):

Mathias, it looks like you were looking at lemma brc_x_equation_new. I got rid of that, as that had lots of problems.

Craig Alan Feinstein (Jun 22 2025 at 18:19):

The linear_comb_of_y_part_2_i3 was actually not what I had originally intended. I actually wanted to use linear_comb_of_y_part_2 where i can be set to 0, 1, 2, or 3 but I couldn't figure out how to do it. For instance, the line using linear_comb_of_y_part_2[where i=2] ineq lag_eq by auto doesn't work. That is one of many things I had problems with. I'll put my new version up there.

Craig Alan Feinstein (Jun 22 2025 at 18:32):

I just put the new version up.

Craig Alan Feinstein (Jun 24 2025 at 03:41):

I am having trouble instantiating lemma linear_comb_of_y_part_2 with variable i. Maybe I should do your suggestion before and do a fix i in the lemma statement?

Last updated: Jun 29 2025 at 20:22 UTC