Craig Alan Feinstein (Jul 14 2024 at 07:30): Craig Alan Feinstein (Jul 14 2024 at 07:30):I just started learning Isabelle by immersion and have been successful in proving some lemmas that I will need to prove the Bruck Ryser Chowla theorem, which is my current goal. I have been using the Design Theory folder in the Archive of Formal Proofs. And I have been using symmetric_bibd in bibs as my context. In this context, N is the incidence matrix. To prove the BRC theorem, I need to show the the determinant of N times N transpose equals the square of the determinant of N. I have been having trouble doing this even though I found a lemma somewhere else in the AFP called det_mult which is supposed to do this. I am wondering if I have to prove that N is a square matrix to do this. In any case, does anybody have any ideas to prove this?
Christian Pardillo Laursen (Jul 14 2024 at 10:57):Looking at the det_mul theorem, you do indeed need matrices of type ‘a^’n^’n. Do you have these? Unfortunately this is not something one can prove, as it’s a type issue. You’ll have to supply matrices of the correct type in the first place or the rule won’t apply.
Craig Alan Feinstein (Jul 14 2024 at 11:57):N is defined as a matrix of type v x b. But in the symmetric_bibd locale, v=b so N is a square matrix in this context.
Craig Alan Feinstein (Jul 14 2024 at 19:49):This is what I have so far with respect to this lemma, but it's not working. It is highlighting "by" in pink and has a red exclamation point:
theory Bruck_Ryser_Chowla imports Fishers_Inequality.Incidence_Matrices
Fishers_Inequality.Fishers_Inequality Jordan_Normal_Form.Determinant
SumSquares.FourSquares
begin
section ‹Bruck Ryser Chowla Theorem›
context ordered_sym_bibd
begin
lemma det_incidence: "det (N * N⇧T) = (det N)^2"
proof -
have "det (N * N⇧T) = det N * det N⇧T" using rep_value_sym by (simp add: det_mult)
also have "det (N * N⇧T) = det N * det N" by simp
qed
Mathias Fleury (Jul 14 2024 at 20:27):Try to use
apply (subst det_mult)
To see why auto / simp is failing
Craig Alan Feinstein (Jul 14 2024 at 21:30):I changed the lemma proof to:
lemma det_incidence: "det (N * N⇧T) = (det N)^2"
proof -
have "det (N * N⇧T) = det N * det N⇧T" using rep_value_sym by (simp add: det_mult)
also have "det (N * N⇧T) = det N * det N" using det_transpose by simp
then have "det (N * N⇧T) = (det N)^2" using power2_eq_square by simp
apply (subst det_mult)
qed
When I clicked on the apply line, I got in the window:
proof (state)
this:
det (N * N⇧T) = (det N)⇧2
goal (1 subgoal):
det (N * N⇧T) = (det N)⇧2
Failed to finish proof:
goal (1 subgoal):
det (N * N⇧T) = (det N)⇧2
Craig Alan Feinstein (Jul 14 2024 at 21:54):Did I use the apply line correctly? I’ve never used it before.
Craig Alan Feinstein (Jul 15 2024 at 02:41):I found using sledgehammer that the following works. I'm not sure I could figure all this out without sledgehammer at this point. Hopefully I'll learn to do it without sledgehammer. But I'm certainly thankful for sledgehammer:
lemma det_incidence: "det (N * N⇧T) = (det N)^2"
proof -
have "det (N * N⇧T) = det N * det N⇧T"
by (metis (full_types) N_carrier_mat det_mult local.symmetric transpose_carrier_mat)
also have "det N * det N⇧T = det N * det N"
using N_carrier_mat det_transpose local.symmetric by auto
then have "det (N * N⇧T) = (det N)^2" by (simp add: calculation power2_eq_square)
thus ?thesis by simp
qed
Mathias Fleury (Jul 15 2024 at 05:21):I meant to add the line at the first place it is failing:
lemma det_incidence:
shows "det (N * N⇧T) = (det N)^2"
proof -
have "det (N * N⇧T) = det N * det N⇧T"
apply (subst det_mult)
and to look at the generated goals. In this case
proof (prove)
goal (3 subgoals):
1. N ∈ carrier_mat ?n ?n
2. N⇧T ∈ carrier_mat ?n ?n
3. det N * det N⇧T = det N * det N⇧T
And if you look at the proof, sledgehammer found the theorem det_incidence and the proofs boils down to:
have ‹N ∈ carrier_mat 𝗏 𝗏›
by (metis (full_types) N_carrier_mat local.symmetric)
then have "det (N * N⇧T) = det N * det N⇧T"
by (simp add: det_mult)
Craig Alan Feinstein said:
I found using sledgehammer that the following works. I'm not sure I could figure all this out without sledgehammer at this point. Hopefully I'll learn to do it without sledgehammer. But I'm certainly thankful for sledgehammer:
As a learning exercise, there is value to do it without sledgehammer. Otherwise, just use it…
Mathias Fleury (Jul 15 2024 at 05:23):And: the structured proof is
have ...
[also ...]+
finally
Not have /also/have
Mathias Fleury (Jul 15 2024 at 05:25):And the show ?thesis should be in the last line of the calculation. And the also is not useful:
lemma det_incidence: "det (N * N⇧T) = (det N)^2"
proof -
have ‹N ∈ carrier_mat 𝗏 𝗏›
by (metis (full_types) N_carrier_mat local.symmetric)
then have "det (N * N⇧T) = det N * det N"
by (simp add: det_mult det_transpose)
then show ?thesis by (simp add: power2_eq_square)
qed
just quickly looking at what @Christian Pardillo Laursen and @Craig Alan Feinstein have said, it looks like you are referring to two different matrix libraries. The one from JNF is a different type from the type-based ones.
Craig Alan Feinstein (Jul 15 2024 at 22:10):So I should not use the one from JNF and use the one from HOL.analysis? This one JNF appears to be giving me problems in other lemmas that I am trying to prove as it thinks the matrix is an integer.
Craig Alan Feinstein (Jul 15 2024 at 22:10):matrix of integers I mean
Craig Alan Feinstein (Jul 16 2024 at 00:11):I got it to work. No more problems. Just one last step I need to complete to prove the easy part of the brc theorem.
Wenda Li (Jul 16 2024 at 13:27):Craig Alan Feinstein said:
So I should not use the one from JNF and use the one from HOL.analysis? This one JNF appears to be giving me problems in other lemmas that I am trying to prove as it thinks the matrix is an integer.
If possible, I would recommend the one from JNF. Leaving matrix dimensions out of types provides the most flexibility, albeit at the cost of slightly more verbose statements. If you do prefer the one from HOL.analysis, it is not a big deal either, as there is a theory in AFP that converts between these two representations.
Craig Alan Feinstein (Jul 16 2024 at 18:09):Thank you, I used the one from JNF.
Last updated: Dec 21 2024 at 12:33 UTC