Craig Alan Feinstein (Aug 06 2024 at 03:00): Craig Alan Feinstein (Aug 06 2024 at 03:00):In the last two months, I've learned to do lots of stuff in Isabelle, but I haven't had the opportunity to verify results of relatively complex calculations, until now. For instance, I tried the following, but got stuck with the last part. The matrix C which is a function of a,b,c,d is such that C*C^t is supposed to be (a^2 + b^2 + c^2 + d^2)*I_4. Any ideas?
"four_squares n = (SOME (a, b, c, d). a^2 + b^2 + c^2 + d^2 = n)"
fun lagrange_mat_of_4 :: "(nat × nat × nat × nat) ⇒ int mat" where
"lagrange_mat_of_4 (a, b, c, d) =
mat 4 4 (λ(i, j). if (i, j) = (1, 1) then a
else if (i, j) = (1, 2) then b
else if (i, j) = (1, 3) then c
else if (i, j) = (1, 4) then d
else if (i, j) = (2, 1) then -b
else if (i, j) = (2, 2) then a
else if (i, j) = (2, 3) then -d
else if (i, j) = (2, 4) then c
else if (i, j) = (3, 1) then -c
else if (i, j) = (3, 2) then d
else if (i, j) = (3, 3) then a
else if (i, j) = (3, 4) then -b
else if (i, j) = (4, 1) then -d
else if (i, j) = (4, 2) then -c
else if (i, j) = (4, 3) then b
else if (i, j) = (4, 4) then a
else 0)"
fun lagrange_mat :: "nat ⇒ int mat" where
"lagrange_mat n = lagrange_mat_of_4(four_squares(n))"
lemma lagrange_identity:
assumes "n ∈ ℕ"
shows "(lagrange_mat n)*(lagrange_mat n)⇧T = int n ⋅⇩m (1⇩m (4::nat))"
proof -
let ?M = "lagrange_mat n"
let ?MT = "transpose_mat(?M)"
let ?prodM = "?M*?MT"
let ?nI = "int n ⋅⇩m (1⇩m (4::nat))"
obtain a b c d where squares: "four_squares n = (a, b, c, d)"
using sum_of_four_squares by (metis surj_pair)
have M_def: "?M = lagrange_mat_of_4 (a, b, c, d)"
using squares by simp
have MT_def: "?MT = transpose_mat(?M)"
by simp
have prodM_def: "?prodM = ?M*?MT"
by simp
then have lagrange_matrix_structure: "?prodM = mat 4 4
(λ(i, j). if (i, j) = (1, 1) then a*a + b*b + c*c + d*d
else if (i, j) = (1, 2) then a*(-b) + b*a + c*(-d) + d*c
else if (i, j) = (1, 3) then a*(-c) + b*d + c*a + d*(-b)
else if (i, j) = (1, 4) then a*(-d) + b*(-c) + c*b + d*a
else if (i, j) = (2, 1) then (-b)*a + a*b + (-d)*c + c*d
else if (i, j) = (2, 2) then (-b)*(-b) + a*a + (-d)*(-d) + c*c
else if (i, j) = (2, 3) then (-b)*(-c) + a*d + (-d)*a + c*(-b)
else if (i, j) = (2, 4) then (-b)*(-d) + a*(-c) + (-d)*b + c*a
else if (i, j) = (3, 1) then (-c)*a + d*b + a*c + (-b)*d
else if (i, j) = (3, 2) then (-c)*(-b) + d*a + a*(-d) + (-b)*c
else if (i, j) = (3, 3) then (-c)*(-c) + d*d + a*a + (-b)*(-b)
else if (i, j) = (3, 4) then (-c)*(-d) + d*(-c) + a*b + (-b)*a
else if (i, j) = (4, 1) then (-d)*a + (-c)*b + b*c + a*d
else if (i, j) = (4, 2) then (-d)*(-b) + (-c)*a + b*(-d) + a*c
else if (i, j) = (4, 3) then (-d)*(-c) + (-c)*d + b*a + a*(-b)
else if (i, j) = (4, 4) then (-d)*(-d) + (-c)*(-c) + b*b + a*a
else 0)"
by sorry
I forgot to say I am importing stuff from the Jordan Normal Form directory
Yong Kiam (Aug 06 2024 at 06:41):have you tried using mat_eq_iff?
Craig Alan Feinstein (Aug 06 2024 at 16:03):I tried using mat_eq_iff and sledgehammer with no success
Craig Alan Feinstein (Aug 06 2024 at 19:07):I just had a thought that maybe I didn’t import the section containing mat_eq_iff. I’ll check that when I get back on Isabelle.
Craig Alan Feinstein (Aug 07 2024 at 00:44):I tried importing that section but it didn’t work
Yong Kiam (Aug 07 2024 at 06:58):you probably need to do mat_eq_iff and auto and inspect the goal more closely....
Yong Kiam (Aug 07 2024 at 06:59):maybe simplify using algebra_simps
Mathias Fleury (Aug 07 2024 at 11:51):And for sure give more details than "it didn't work". What did you try? What goal remained?
Craig Alan Feinstein (Aug 07 2024 at 23:56):I changed it to make it look a little nicer to this, but it didn't find anything from sledgehammer:
fun four_squares :: "nat ⇒ (nat × nat × nat × nat)" where
"four_squares n = (SOME (a, b, c, d). a^2 + b^2 + c^2 + d^2 = n)"
fun lagrange_mat_of_4 :: "(nat × nat × nat × nat) ⇒ int mat" where
"lagrange_mat_of_4 (a, b, c, d) =
mat 4 4 (λ(i, j). if (i, j) = (1, 1) then a
else if (i, j) = (1, 2) then b
else if (i, j) = (1, 3) then c
else if (i, j) = (1, 4) then d
else if (i, j) = (2, 1) then -b
else if (i, j) = (2, 2) then a
else if (i, j) = (2, 3) then -d
else if (i, j) = (2, 4) then c
else if (i, j) = (3, 1) then -c
else if (i, j) = (3, 2) then d
else if (i, j) = (3, 3) then a
else if (i, j) = (3, 4) then -b
else if (i, j) = (4, 1) then -d
else if (i, j) = (4, 2) then -c
else if (i, j) = (4, 3) then b
else if (i, j) = (4, 4) then a
else 0)"
fun lagrange_mat :: "nat ⇒ int mat" where
"lagrange_mat n = lagrange_mat_of_4(four_squares(n))"
lemma lagrange_identity:
assumes n_natural: "n ∈ ℕ"
shows "(lagrange_mat n)*(lagrange_mat n)⇧T = int n ⋅⇩m (1⇩m (4::nat))"
proof -
obtain a b c d where squares: "four_squares n = (a, b, c, d)"
using sum_of_four_squares by (metis surj_pair)
then have "lagrange_mat n = lagrange_mat_of_4(a, b, c, d)" using squares
by simp
then have "(lagrange_mat n)*(lagrange_mat n)⇧T =
lagrange_mat_of_4(a, b, c, d)*(lagrange_mat_of_4(a, b, c, d))⇧T"
by simp
then have
"lagrange_mat_of_4(a, b, c, d)*(lagrange_mat_of_4(a, b, c, d))⇧T =
int n ⋅⇩m (1⇩m (4::nat))"
using algebra_simps mat_eq_iff by sledgehammer
The "by auto" suggestion was helpful, as it allowed me to see some steps in what Isabelle is thinking. But I still don't know how to convince Isabelle.
Craig Alan Feinstein (Aug 08 2024 at 04:24):It seems that working with matrices and vectors is harder than working with simple algebra in Isabelle. Any suggestions would be appreciated.
Mathias Fleury (Aug 08 2024 at 14:13):If I understand the problem correctly, the issue now is that you have to work with the choice (to derive that a^2 + b^2 + c^2 + d^2 = n) which sledgehammer is not good at
Mathias Fleury (Aug 08 2024 at 14:20):See this thread https://isabelle.zulipchat.com/#narrow/stream/238552-Beginner-Questions/topic/Proving.20lemma.20with.20definite.20description/near/291315915
Craig Alan Feinstein (Aug 09 2024 at 00:43):@MathiasFleury I think that is a good suggestion, so I got rid of the n and just kept the a,b,c,d. I'll worry about the n later. I came up with this (worrying only about the first entry of the matrix), but sledgehammer didn't find a proof. Any ideas?
fun lagrange_mat_of_4 :: "(nat × nat × nat × nat) ⇒ int mat" where
"lagrange_mat_of_4 (a, b, c, d) =
mat 4 4 (λ(i, j). if (i, j) = (1, 1) then a
else if (i, j) = (1, 2) then b
else if (i, j) = (1, 3) then c
else if (i, j) = (1, 4) then d
else if (i, j) = (2, 1) then -b
else if (i, j) = (2, 2) then a
else if (i, j) = (2, 3) then -d
else if (i, j) = (2, 4) then c
else if (i, j) = (3, 1) then -c
else if (i, j) = (3, 2) then d
else if (i, j) = (3, 3) then a
else if (i, j) = (3, 4) then -b
else if (i, j) = (4, 1) then -d
else if (i, j) = (4, 2) then -c
else if (i, j) = (4, 3) then b
else if (i, j) = (4, 4) then a
else 0)"
lemma lagrange_mat_of_4_identity:
assumes "a ∈ ℕ" "b ∈ ℕ" "c ∈ ℕ" "d ∈ ℕ"
shows "(lagrange_mat_of_4 (a, b, c, d))*(lagrange_mat_of_4 (a, b, c, d))⇧T =
int (a^2 + b^2 + c^2 + d^2) ⋅⇩m (1⇩m (4::nat))"
proof -
let ?M = "lagrange_mat_of_4 (a, b, c, d)"
let ?MT = "transpose_mat(?M)"
let ?prodM = "?M*?MT"
let ?nI = "int (a^2 + b^2 + c^2 + d^2) ⋅⇩m (1⇩m (4::nat))"
have "?prodM $$ (1,1) =
a * a + b * b + c * c + d * d" using algebra_simps mat_eq_iff by sledgehammer
Wait a second - I just had a thought that maybe the indices are 0,1,2,3 instead of 1,2,3,4 for matrices in Isabelle? I'll try this now.
Craig Alan Feinstein (Aug 09 2024 at 00:55):Unfortunately changing the indices had no effect. Sledgehammer still failed.
Craig Alan Feinstein (Aug 09 2024 at 01:46):Are there any actual examples of matrix multiplication in Isabelle?
Mathias Fleury (Aug 09 2024 at 12:38):As I have never used the matrix multiplication, I cannot help you. Some general information:
transferor variants like thatfind_theorem or the panel if you know that the theorem exists Mathias Fleury (Aug 09 2024 at 12:38):You are at the point where searching for lemmas and deciding how to prove things by hand and looking how other theorems are proved is the right way to go
Craig Alan Feinstein (Aug 09 2024 at 13:17):I agree that I am at a point where I need to learn how to find stuff on my own. What is find_theorem and the panel?
Mathias Fleury (Aug 09 2024 at 13:18):https://stackoverflow.com/questions/21255473/using-find-theorems-in-isabelle the query panel is just a front-end to the same tool
Craig Alan Feinstein (Aug 09 2024 at 13:22):Ok thank you
Chelsea Edmonds (Aug 12 2024 at 10:07):Agree 100% with Mathias advice above. To add a bit of Matrix context specifically, I found that sledgehammer wasn't great for matrix reasoning - I suspect due to the fact that you constantly need to prove the index bounds hold (i.e. that you're not reasoning on an index outside the row/column dimensions... which do go from 0). There are many lemmas that enable reasoning at the index level (e.g. index_mult_mat) which may be useful to look for in the library. You should be able to find many examples of how to use these types of lemmas and managing dimension assumptions throughout AFP entries using the JNF library - both for multiplication and other common operators.
Craig Alan Feinstein (Aug 12 2024 at 16:18):I found that Chelsea’s library about Incidence matrices in Fisher’s inequality was very helpful for working with matrices. I was able to model part of my proof on it so far.
Craig Alan Feinstein (Aug 13 2024 at 02:50):Here is a simple question - suppose I have two 2x2 matrices, one with rows (1 2) (3 4) and the other with rows (1 3) (2 4) (which happens to be the transpose of the first). How do I efficiently prove in Isabelle that the product is (5 11) (11 25)?
Jonathan Julian Huerta y Munive (Aug 13 2024 at 08:12):@Craig Alan Feinstein I have not worked with the Jordan Normal Form AFP entry, but to answer your question, it is generally good practice to develop general lemmas that will allow Isabelle's simplifier to "reduce" the expression from left to right. For instance, in this AFP entry, in the proof of times_mtx2, Isabelle only needed the simplifier because of the lemmas provided before: sq_mtx_times_eq and sq_mtx_eq_iff. Take a look at what they are saying and you could replicate the approach. Then, the lemma times_mtx2 itself is later used for "computation proofs" in the lemma inv_mtx_chB_hOsc.
Jonathan Julian Huerta y Munive (Aug 13 2024 at 09:57):Since you mention that you do not know the command find_theorems yet, perhaps this ~1-hour exercise file can help you.
Craig Alan Feinstein (Aug 14 2024 at 01:29):Thank you both, I’ll give them a shot.
Craig Alan Feinstein (Aug 14 2024 at 16:20):There is still a lot of elementary things to be done with matrices in the libraries, for instance I couldn’t find a definition of a positive definite matrix.
Jonathan Julian Huerta y Munive (Aug 14 2024 at 23:08):@Craig Alan Feinstein right, Serapis does not throw me anything useful and grepping the AFP only threw me this AFP entry. It would be a good exercise for whoever tries it :wink:
Craig Alan Feinstein (Aug 16 2024 at 02:27):The matrix part is going well, except I cannot find a way to prove that
\Sigma_{i=1}^4 M(k) = M(1) + M(2) + M(3) + M(4)
Is there a library that has definition of summations?
Mathias Fleury (Aug 16 2024 at 04:43):I know it sounds mean, but did you try to search for Sum in Isabelle or on your favorite search engine? Because on my search engine, the 4th solution points to a Sum in Isar_Examples… Using a search engine is much faster than posting a question here…
Craig Alan Feinstein (Aug 16 2024 at 13:27):Of course I searched. I searched the Archive of Formal Proofs with no luck and also the Isabelle search engine with no luck, probably because I searched for “summation” and “Sigma summation”. I don’t post here if I haven’t tried myself.
Craig Alan Feinstein (Aug 16 2024 at 15:42):I just typed “sum” in FindFacts. It didn’t give isar examples on the first page. However I’m now looking at Serapis and it looks like there is stuff that could be helpful. I’ll have to use that search engine more.
Craig Alan Feinstein (Aug 16 2024 at 23:00):To be specific, I'm been trying get Isabelle to recognize the following with no luck. The stuff I found through searching hasn't been of any help:
have "(∑k ∈{0..<4} . (?M $$ (3, k))^2) =
(?M $$ (3, 0))^2 + (?M $$ (3, 1))^2 +
(?M $$ (3, 2))^2 + (?M $$ (3, 3))^2"
Typing the following into my session works
have "(∑k ∈{0..<4} . f k) =
f 0 + f 1 + f 2 + f 3" for f :: "nat ⇒ ('a :: comm_monoid_add)"
by (simp add: numeral.simps(2,3))
If you're having syntax issues I imagine it's a matrix thing rather than a sum thing
Craig Alan Feinstein (Aug 18 2024 at 02:15):@Christian Pardillo Laursen that worked. May I ask how you found that? I wouldn't have found that on my own.
Mathias Fleury (Aug 19 2024 at 16:31):Rule of thumb when a term is not recognized: test peaces of it in term to see what Isabelle does not recognize exactly. So maybe term "(∑k ∈{0..<4} . (?M $$ (3, k))^2)" and term "(?M $$ (3, 0))^2 + (?M $$ (3, 1))^2 +
(?M $$ (3, 2))^2 + (?M $$ (3, 3))^2"
Usually one of two things happen:
note [[show_sorts]] look at the different sorts that are required which ones are not compatible. Craig Alan Feinstein (Oct 16 2024 at 00:02):Is there an easy way to do the same thing in which proves (∑k ∈{m-3..<m+1} . (?M (3,m-3))^2 + (?M (3,m-1))^2 + (?M $$ (3,m))^2 ? That way only works when k ∈{0..<4}. I could redefine the function so it works, but I was hoping there is an easier way.
Mathias Fleury (Oct 16 2024 at 05:04):find_theorem is your friend!
Craig Alan Feinstein (Oct 16 2024 at 12:08):I shall try it.
Last updated: Dec 21 2024 at 12:33 UTC