Stream: General

Topic: Peculiar feature of the proof of the Bruck Ryser Chowla thm

Craig Alan Feinstein (Dec 04 2024 at 05:05):

I have made lots of progress in proving the Bruck Ryser Chowla theorem in Isabelle. I learned about it in college in 1991 and was fascinated with one part of the proof that was peculiar. Back then I couldn’t put my finger on why it was peculiar but now I think I can explain it - consider proposition P(x). If variable y is independent of x, then the truth of P(x) is independent of the value of y. This is obvious.

The proof as I understand it of the BRC theorem in Stinson’s book uses this principle: it proves that S(x,y) implies P(x) as follows - it assumes S(x,y) and y=c and then proves P(x). But what about if y is not c? Since P(x) is independent of y, the fact that P(x) is true when y=c and S(x,y) is true implies that P(x) is always true, regardless of the value of y as long as S(x,y) is true for some y.

So I ask you can Isabelle handle this peculiar principle?

Fabian Huch (Dec 04 2024 at 09:23):

This is just how contexts work, if I understand your question correctly -- what you want to do is:

lemma "S (x,y) ⟹ P x"
proof -
  fix c assume "S (x,c)"
  then show "P x" sorry
qed

Craig Alan Feinstein (Dec 04 2024 at 13:28):

Correct, that is the basic structure of the Bruck Ryser Chowla theorem proof in Stinson’s book. I want to do that in Isabelle. (The details are a lot more complicated though.)

Fabian Huch (Dec 04 2024 at 13:47):

Great -- what I wrote is already working Isabelle source ;)

Craig Alan Feinstein (Dec 04 2024 at 17:02):

So you mean Isabelle is already programmed to recognize these types of proofs?

Fabian Huch (Dec 04 2024 at 17:08):

Yes (at least if I understood the question correctly). The primitive logic of Isabelle is described in detail in Chapter 2 of the Implementation manual.

Craig Alan Feinstein (Dec 04 2024 at 17:15):

Good to hear. Isabelle’s creators have my respect.

Craig Alan Feinstein (Dec 05 2024 at 22:12):

Is there a name for this type of proof or this phenomenon?

Craig Alan Feinstein (Dec 13 2024 at 21:00):

As I have tried to prove this part of the BRC theorem in Isabelle I have come to the conclusion that my interpretation outlined above is not correct - Isabelle’s not accepting it convinced me of this.

Craig Alan Feinstein (Dec 22 2024 at 01:01):

Now I think my interpretation of the BRC proof is correct, but if you look at part 2 of this thread you will see that Isabelle had problems with it.

Last updated: Dec 30 2024 at 16:22 UTC