Craig Alan Feinstein (Sep 03 2024 at 02:43): Craig Alan Feinstein (Sep 03 2024 at 02:43):The following proof is fine until the last line, which uses the same lemma as the line before sum.swap, except it fails. Is this because the lemma only holds when the summation symbols are first?
lemma brc_equation:
assumes "x β rat mat π 1"
shows "(βi β {0..<π}. (L_of x $$ (i,0))^2) =
of_int Ξ * (βi β {0..<π}.(x $$ (i, 0)))^2 +
of_int (π - Ξ) * (βi β {0..<π}. (x $$ (i, 0))^2)"
proof -
have "(βi β {0..<π}. (L_of x $$ (i,0))^2) =
(βi β {0..<π}.(βh β {0..<π}. of_int (N $$ (h,i)) * x $$ (h,0))^2)"
by auto
then have "... = (βi β {0..<π}. (βj β {0..<π}. of_int (N $$ (j, i)) *
x $$ (j, 0)) * (βh β {0..<π}. of_int (N $$ (h, i)) * x $$ (h, 0)))"
by (simp add: power2_eq_square)
then have "... = (βi β {0..<π}. (βj β {0..<π}. (βh β {0..<π}.
(of_int (N $$ (j,i)) * x $$ (j,0)) * (of_int (N $$ (h,i)) * x $$ (h,0)))))"
by (metis (no_types) sum_product)
then have "... = (βj β {0..<π}. (βi β {0..<π}. (βh β {0..<π}.
(of_int (N $$ (j,i)) * x $$ (j,0)) * (of_int (N $$ (h,i)) * x $$ (h,0)))))"
using sum.swap by simp
then have "... = (βj β {0..<π}. (βh β {0..<π}. (βi β {0..<π}.
(of_int (N $$ (j,i)) * x $$ (j,0)) * (of_int (N $$ (h,i)) * x $$ (h,0)))))"
using sum.swap by simp
You want also have/also have/finally have
Mathias Fleury (Sep 03 2024 at 04:56):With this using it works:
using sum.swap[of βΉΞ»h i. (of_int (N $$ (j,i)) * x $$ (j,0)) * (of_int (N $$ (h,i)) * x $$ (h,0))βΊ for j]
You mean I should use βalso haveβ instead of βthen haveβ?
Craig Alan Feinstein (Sep 03 2024 at 05:04):I noticed in the Fisher inequality library Matrix_Vector_Extras, there is a lemma that is used sum_reorder_triple, that might also work.
Chelsea Edmonds (Sep 03 2024 at 11:16):Craig Alan Feinstein said:
I noticed in the Fisher inequality library Matrix_Vector_Extras, there is a lemma that is used sum_reorder_triple, that might also work.
Summations are definitely something which feels like it should be easy to automate, but in reality often isn't (a problem shared across proof assistants as well). I think it could be an interesting student project to investigate at some point. Instantiating directly the parameters of lemmas (like what Mathias did above) is typically the best strategy for now. The sum_reorder_triple lemma in my library could definitely help depending on what you have to do - both as examples for how to do proofs with summations and potentially in this case (with incidence matrices, such triples are not uncommon).
Craig Alan Feinstein (Sep 03 2024 at 21:33):I just got sum_reorder_triple to work.
Craig Alan Feinstein (Sep 04 2024 at 03:57):Moving around parentheses and taking out expressions to outer parentheses within multiple summations also seems to be difficult in Isabelle.
Craig Alan Feinstein (Sep 04 2024 at 03:59):Every time I solve a hard problem that I didnβt think would be hard, a new hard problem that I didnβt think would be hard comes up.
Craig Alan Feinstein (Sep 06 2024 at 01:15):Instantiation is a new trick for me that Iβll add to my toolbox.
Manuel Eberl (Sep 06 2024 at 10:20):I normally use sum.swap with very explicit proof methods like rule or subst instead.
Manuel Eberl (Sep 06 2024 at 10:22):Moving parentheses and pulling things into and out of (finite) sums is usually easy using simp add: algebra_simps sum_distrib_left sum_distrib_right
Manuel Eberl (Sep 06 2024 at 10:22):While we're at it, if you ever struggle with reindexing sums, sum.reindex_bij_witness is the secret weapon.
Craig Alan Feinstein (Sep 06 2024 at 15:43):@Manuel Eberl I just tried by (simp add: algebra_simps sum_distrib_left sum_distrib_right) and that solved the problem. Thank you.
Craig Alan Feinstein (Sep 08 2024 at 17:14):Now I have the following in which I need to use substitution of matdef into the last expression.
lemma brc_x_equation:
assumes "x β rat mat π 1" "h < π" "j < π"
shows "(βi β {0..<π}. (L_of x $$ (i,0))^2) =
of_int Ξ * (βi β {0..<π}.(x $$ (i, 0)))^2 +
of_int (π - Ξ) * (βi β {0..<π}. (x $$ (i, 0))^2)"
proof -
let ?N_rat = "map_mat (of_int) N"
have matdef: "(?N_rat * ?N_ratβ§T) $$ (j, h) = (βi β{0..<π} . ?N_rat $$ (j, i) * ?N_rat $$ (h, i))"
using assms(2) assms(3) transpose_mat_mult_entries[of "j" "?N_rat" "h"]
local.symmetric by fastforce
have "(βi β {0..<π}. (L_of x $$ (i,0))^2) =
(βi β {0..<π}.(βh β {0..<π}. (?N_rat $$ (h,i)) * x $$ (h,0))^2)"
by auto
also have "... = (βi β {0..<π}. (βj β {0..<π}. (?N_rat $$ (j, i)) *
x $$ (j, 0)) * (βh β {0..<π}. (?N_rat $$ (h, i)) * x $$ (h, 0)))"
by (simp add: power2_eq_square)
also have "... = (βi β {0..<π}. (βj β {0..<π}. (βh β {0..<π}.
(?N_rat $$ (j,i) * x $$ (j,0)) * (?N_rat $$ (h,i) * x $$ (h,0)))))"
by (metis (no_types) sum_product)
also have "... = (βi β {0..<π}. (βj β {0..<π}. (βh β {0..<π}.
?N_rat $$ (j,i) * ?N_rat $$ (h,i) * x $$ (j,0) * x $$ (h,0))))"
by (simp add: algebra_simps)
also have "... = (βj β {0..<π}. (βh β {0..<π}. (βi β {0..<π}.
?N_rat $$ (j,i) * ?N_rat $$ (h,i) * x $$ (j,0) * x $$ (h,0))))"
using sum_reorder_triple[of "Ξ» i j h . ?N_rat $$ (j,i) *
?N_rat $$ (h,i) * x $$ (j,0) * x $$ (h,0)"
"{0..<π}" "{0..<π}" "{0..<π}"] by simp
also have "... = (βj β {0..<π}. (βh β {0..<π}. (βi β {0..<π}.
?N_rat $$ (j,i) * ?N_rat $$ (h,i)) * x $$ (j,0) * x $$ (h,0)))"
by (simp add: algebra_simps sum_distrib_left sum_distrib_right)
also have "... = (βj β {0..<π}. (βh β {0..<π}.
(?N_rat * ?N_ratβ§T) $$ (j, h) * x $$ (j,0) * x $$ (h,0)))"
Shouldn't you forall quantify j and h in matdef?
Mathias Fleury (Sep 08 2024 at 17:21):(or for j h after the have)
Mathias Fleury (Sep 08 2024 at 17:22):otherwise the proof is for a fixed j and a fixed h that have nothing to do with the j/h from the sum in the last step
Craig Alan Feinstein (Sep 08 2024 at 17:55):when I do the following it cannot find a proof with try0:
have matdef: "β h j. (?N_rat * ?N_ratβ§T) $$ (j, h) = (βi β{0..<π} . ?N_rat $$ (j, i) * ?N_rat $$ (h, i))"
using assms(2) assms(3) transpose_mat_mult_entries[of "j" "?N_rat" "h"]
local.symmetric by try0
You probably want to add assms(2,3) to talk about the new h and jβ¦
Craig Alan Feinstein (Sep 08 2024 at 18:06):Do you mean this? assms(2) and assms(3) are already used.
have matdef: "β h j. (?N_rat * ?N_ratβ§T) $$ (j, h) = (βi β{0..<π} . ?N_rat $$ (j, i) * ?N_rat $$ (h, i))"
using transpose_mat_mult_entries[of "j" "?N_rat" "h"]
local.symmetric by (simp add: assms(2,3))
assms(2,3) are "h < π" "j < π"
Mathias Fleury (Sep 08 2024 at 18:41):they talk about a different h j than the one from β h j. ...
Mathias Fleury (Sep 08 2024 at 18:42):So if you compare the expression before (which was working) to the one now, you have removed assumptions
Mathias Fleury (Sep 08 2024 at 18:43):so my intuition as someone who has no clue what you are doing: you need to pass the assumptions too here
Mathias Fleury (Sep 08 2024 at 18:43):or maybe it is the fact that transpose_mat_mult_entries[of "j" "?N_rat" "h"] does refer to the wrong j and h too
Mathias Fleury (Sep 08 2024 at 18:45):My intuition is that this:
have matdef: "(?N_rat * ?N_ratβ§T) $$ (j, h) = (βi β{0..<π} . ?N_rat $$ (j, i) * ?N_rat $$ (h, i))" if "h < π" "j < π" for h j
using transpose_mat_mult_entries[of "j" "?N_rat" "h"]
local.symmetric that by fastforce
should work
Mathias Fleury (Sep 08 2024 at 18:46):and be what you want (modulo the fact that unfolding will still not work as you are going to need some congruence stuff)
Craig Alan Feinstein (Sep 08 2024 at 20:11):Yes, that worked, thank you. Just need to get the last substitution part to work now. After that, if I use the fact that N*N^t is a matrix with r on the diagonal and Lambda on the off diagonal, the proof of the lemma will be finished.
Craig Alan Feinstein (Sep 08 2024 at 20:26):The rest of the proof of the BRC is even harder than this part. I haven't been really working on this part so much in the last week.
Craig Alan Feinstein (Sep 09 2024 at 01:18):I have learned from two months plus of working with Isabelle that sometimes it's not a good idea to work to hard to prove a certain point. There might be a way to avoid trying to prove that point and do things a different way. Perhaps I don't even have to even work with (?N_rat * ?N_ratβ§T) $$ (j, h). It all depends on what's in the Fisher's Inequality library, which I will go through again.
Mathias Fleury (Sep 09 2024 at 04:17):The issue here is that you need information about the sum to the replacement
Mathias Fleury (Sep 09 2024 at 04:19):So you need to use the congruence lemma sum.cong to change the sum internally. Or you directly follow @Manuel Eberl advice:
Manuel Eberl said:
While we're at it, if you ever struggle with reindexing sums, sum.reindex_bij_witness is the secret weapon.
Because sum.reindex_bij_witness does congruence + reindexing but you do not have to reindex
Mathias Fleury (Sep 09 2024 at 04:21):Craig Alan Feinstein said:
I have learned from two months plus of working with Isabelle that sometimes it's not a good idea to work to hard to prove a certain point. There might be a way to avoid trying to prove that point and do things a different way. Perhaps I don't even have to even work with
(?N_rat * ?N_ratβ§T) $$ (j, h). It all depends on what's in the Fisher's Inequality library, which I will go through again.
it is always hard to say, but after less than 2 months, I would really try to get the proof through to understand how reindexing work, even if you end up deleting the proofs. Reindexing/applying congruence is one of the most critical tools for working with sums
Craig Alan Feinstein (Sep 09 2024 at 16:06):Thank you, I looked up sum.cong and found the Kummer congruence library uses it. It also has more examples of dealing with summations so Iβll study it.
Craig Alan Feinstein (Sep 10 2024 at 12:01):Also found some good stuff with summation in the Gauss sums library
Last updated: Dec 21 2024 at 12:33 UTC