Email Gateway (Nov 18 2024 at 13:16): Email Gateway (Nov 18 2024 at 13:16):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,
this is a repeated attempt to attract attention to a mistake in
HOL-Analysis.
To be specific, I am convinced that line 997 of
HOL/Analysis/Finite_Cartesian_Product.thy should be
where "v v* m == (χ j. sum (λi. (v$i) * ((m$i)$j)) (UNIV :: 'm
set)) :: 'a^'n"
instead of the current
where "v v* m == (χ j. sum (λi. ((m$i)$j) * (v$i)) (UNIV :: 'm set))
:: 'a^'n"
Please, let me know if there a different way/place to report this properly.
Stepan
On 17-Sep-24 9:22 AM, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:
Hello,
in HOL/Analysis/Finite_Cartesian_Product.thy
the multiplication by a vector from the left (constant
vector_matrix_mult) is not associative unless the underlying semiring
is commutative.
Namely,
lemma "(x v* A) v* B = x v* (A ** B)"
is not true, unlike its proven counterpart
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"This is due to the inverted order of multiplicands in the definition
of vector_matrix_mult.I expect this is unintended. If there is no motivation I miss, I
suggest it should be changed.Best regards
Stepan
Email Gateway (Nov 19 2024 at 13:13):From: 伊藤洋介 <glacier345@gmail.com>
Dear Stepan Holub,
I agree with you.
The definition of vector_matrix_mult seems wrong.
I think this is the right place to point it out.
I hope the Isabelle developers also agree with us...
Best regards,
2024年11月18日(月) 22:16 Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>:
Hello,
this is a repeated attempt to attract attention to a mistake in
HOL-Analysis.To be specific, I am convinced that line 997 of
HOL/Analysis/Finite_Cartesian_Product.thy should bewhere "v v* m == (χ j. sum (λi. (v$i) * ((m$i)$j)) (UNIV :: 'm
set)) :: 'a^'n"instead of the current
where "v v* m == (χ j. sum (λi. ((m$i)$j) * (v$i)) (UNIV :: 'm set))
:: 'a^'n"Please, let me know if there a different way/place to report this properly.
Stepan
On 17-Sep-24 9:22 AM, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:Hello,
in HOL/Analysis/Finite_Cartesian_Product.thy
the multiplication by a vector from the left (constant
vector_matrix_mult) is not associative unless the underlying semiring
is commutative.
Namely,
lemma "(x v* A) v* B = x v* (A ** B)"
is not true, unlike its proven counterpart
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"This is due to the inverted order of multiplicands in the definition
of vector_matrix_mult.I expect this is unintended. If there is no motivation I miss, I
suggest it should be changed.Best regards
Stepan
--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com
Email Gateway (Nov 19 2024 at 15:38):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
it might well be that I am the only HOL-Analysis person remaining among
the core Isabelle developers. I've never used the matrices in
HOL-Analysis, so I am completely unfamiliar with that library. But if I
am indeed the only person who is in a position to do anything about it,
I will look into it.
Perhaps some more people using that library can chime in?
Manuel
On 19/11/2024 14:13, 伊藤洋介 wrote:
Dear Stepan Holub,
I agree with you.
The definition ofvector_matrix_multseems wrong.
I think this is the right place to point it out.
I hope the Isabelle developers also agree with us...Best regards,
2024年11月18日(月) 22:16 Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>:
Hello,
this is a repeated attempt to attract attention to a mistake in
HOL-Analysis.To be specific, I am convinced that line 997 of
HOL/Analysis/Finite_Cartesian_Product.thy should be> where "v v* m == (χ j. sum (λi. (v$i) * ((m$i)$j)) (UNIV :: 'm
> set)) :: 'a^'n"instead of the current
> where "v v* m == (χ j. sum (λi. ((m$i)$j) * (v$i)) (UNIV :: 'm
set))
> :: 'a^'n"Please, let me know if there a different way/place to report this
properly.Stepan
On 17-Sep-24 9:22 AM, Stepan Holub (via cl-isabelle-users Mailing
List)
wrote:
> Hello,
>
> in HOL/Analysis/Finite_Cartesian_Product.thy
> the multiplication by a vector from the left (constant
> vector_matrix_mult) is not associative unless the underlying
semiring
> is commutative.
> Namely,
> lemma "(x v* A) v* B = x v* (A ** B)"
> is not true, unlike its proven counterpart
> lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
>
> This is due to the inverted order of multiplicands in the
definition
> of vector_matrix_mult.
>
> I expect this is unintended. If there is no motivation I miss, I
> suggest it should be changed.
>
> Best regards
>
> Stepan
>
>--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com
Email Gateway (Nov 19 2024 at 15:50):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Thanks for the reactions. I appreciate them.
Just in case the topic seems esoteric: I believe there should be no
discussion about the fact that matrix multiplication is supposed to be
associative. Which is not the case now.
Stepan
On 11/19/2024 4:38 PM, Manuel Eberl wrote:
Hello,
it might well be that I am the only HOL-Analysis person remaining
among the core Isabelle developers. I've never used the matrices in
HOL-Analysis, so I am completely unfamiliar with that library. But if
I am indeed the only person who is in a position to do anything about
it, I will look into it.Perhaps some more people using that library can chime in?
Manuel
On 19/11/2024 14:13, 伊藤洋介 wrote:
Dear Stepan Holub,
I agree with you.
The definition ofvector_matrix_multseems wrong.
I think this is the right place to point it out.
I hope the Isabelle developers also agree with us...Best regards,
2024年11月18日(月) 22:16 Stepan Holub
<cl-isabelle-users@lists.cam.ac.uk>:Hello,
this is a repeated attempt to attract attention to a mistake in
HOL-Analysis.To be specific, I am convinced that line 997 of
HOL/Analysis/Finite_Cartesian_Product.thy should be> where "v v* m == (χ j. sum (λi. (v$i) * ((m$i)$j)) (UNIV :: 'm
> set)) :: 'a^'n"instead of the current
> where "v v* m == (χ j. sum (λi. ((m$i)$j) * (v$i)) (UNIV :: 'm
set))
> :: 'a^'n"Please, let me know if there a different way/place to report this
properly.Stepan
On 17-Sep-24 9:22 AM, Stepan Holub (via cl-isabelle-users Mailing
List)
wrote:
> Hello,
>
> in HOL/Analysis/Finite_Cartesian_Product.thy
> the multiplication by a vector from the left (constant
> vector_matrix_mult) is not associative unless the underlying
semiring
> is commutative.
> Namely,
> lemma "(x v* A) v* B = x v* (A ** B)"
> is not true, unlike its proven counterpart
> lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x"
>
> This is due to the inverted order of multiplicands in the
definition
> of vector_matrix_mult.
>
> I expect this is unintended. If there is no motivation I miss, I
> suggest it should be changed.
>
> Best regards
>
> Stepan
>
>--
伊藤 洋介
Yosuke ITO
+81 80-5057-6931
glacier345@gmail.com
Email Gateway (Nov 20 2024 at 10:50):From: Lawrence Paulson <lp15@cam.ac.uk>
I ported vast chunks of this library (from HOL Light). But the operative word is “ported”; I didn't change any definitions. This particular file however, lists the author as Amine Chaieb (Who gave us formal power series). Anyway the question is simple: what do textbooks say?
Of course it is not esoteric. This sort of basic definition needs to be correct.
Larry
On 19 Nov 2024, at 15:38, Manuel Eberl <manuel@pruvisto.org> wrote:
it might well be that I am the only HOL-Analysis person remaining among the core Isabelle developers. I've never used the matrices in HOL-Analysis, so I am completely unfamiliar with that library. But if I am indeed the only person who is in a position to do anything about it, I will look into it.
Perhaps some more people using that library can chime in?
Email Gateway (Nov 20 2024 at 11:12):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Anyway the question is simple: what do textbooks say?
Do you mean what textbooks say about how matrices should be multiplied?
Stepan
Email Gateway (Nov 21 2024 at 18:53):From: Alexander Pach <alexander.pach@tum.de>
Dear all,
as vector_matrix_mult is surprisingly rarely used, only minor adaptions
are needed. See attached file 81471.patch for Isabelle and 15047.patch
for the AFP, which also adapts Vector-Matrix-Multiplications for
AFP-defined arrays, where necessary. Feel free to use them in any way
you see fit.
I have successfully built all sessions using vector_matrix_mult in their
theory files, but not all possibly impacted sessions due to performance
constraints, so I'd appreciate someone doing a complete build.
Kind regards
Alexander Pach
P.S. Groebner_Bases has a definition with correct term order in
Macaulay_Matrix at line 31:
mult_vec_mat :: "'a vec \<Rightarrow> 'a :: semiring_0 mat \<Rightarrow> 'a vec" (infixl "\<^sub>v*" 70)
where "v \<^sub>v* A \<equiv> vec (dim_col A) (\<lambda>j. v \<bullet> col A j)"
Am 2024-11-20 um 11:50 schrieb Lawrence Paulson:
I ported vast chunks of this library (from HOL Light). But the operative word is “ported”; I didn't change any definitions. This particular file however, lists the author as Amine Chaieb (Who gave us formal power series). Anyway the question is simple: what do textbooks say?
Of course it is not esoteric. This sort of basic definition needs to be correct.
Larry
On 19 Nov 2024, at 15:38, Manuel Eberl<manuel@pruvisto.org> wrote:
it might well be that I am the only HOL-Analysis person remaining among the core Isabelle developers. I've never used the matrices in HOL-Analysis, so I am completely unfamiliar with that library. But if I am indeed the only person who is in a position to do anything about it, I will look into it.
Perhaps some more people using that library can chime in?
81471.patch
15047.patch
smime.p7s
Email Gateway (Nov 21 2024 at 19:48):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Dear Alexander,
thank you very much. Accidentally I have just written almost the same
patch (for HOL-Analysis only), attached.
It contains two additional minor suggestions:
- vector_scalar_commute and scalar_vector_matrix_assoc can be
generalized from field to comm_semiring_1
- vector_matrix_mul_assoc in Cartesian_Space is now a (weaker)
duplicate and can be deleted.
Best regards
Stepan
On 21-Nov-24 7:46 PM, Alexander Pach wrote:
Dear all,
as vector_matrix_mult is surprisingly rarely used, only minor
adaptions are needed. See attached file 81471.patch for Isabelle and
15047.patch for the AFP, which also adapts
Vector-Matrix-Multiplications for AFP-defined arrays, where necessary.
Feel free to use them in any way you see fit.I have successfully built all sessions using vector_matrix_mult in
their theory files, but not all possibly impacted sessions due to
performance constraints, so I'd appreciate someone doing a complete build.Kind regards
Alexander PachP.S. Groebner_Bases has a definition with correct term order in
Macaulay_Matrix at line 31:mult_vec_mat :: "'a vec \<Rightarrow> 'a :: semiring_0 mat \<Rightarrow> 'a vec" (infixl "\<^sub>v*" 70)
where "v \<^sub>v* A \<equiv> vec (dim_col A) (\<lambda>j. v \<bullet> col A j)"
Am 2024-11-20 um 11:50 schrieb Lawrence Paulson:I ported vast chunks of this library (from HOL Light). But the operative word is “ported”; I didn't change any definitions. This particular file however, lists the author as Amine Chaieb (Who gave us formal power series). Anyway the question is simple: what do textbooks say?
Of course it is not esoteric. This sort of basic definition needs to be correct.
Larry
On 19 Nov 2024, at 15:38, Manuel Eberl<manuel@pruvisto.org> wrote:
it might well be that I am the only HOL-Analysis person remaining among the core Isabelle developers. I've never used the matrices in HOL-Analysis, so I am completely unfamiliar with that library. But if I am indeed the only person who is in a position to do anything about it, I will look into it.
Perhaps some more people using that library can chime in?
Email Gateway (Nov 21 2024 at 19:53):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
P.S.: BTW, a plausible explanation of how that strange definition came
about in the first place is that, for some reasons, Amine sacrificed
associativity of the vector-matrix multiplication in non-commutative
case in favor of vector_transpose_matrix identity in the non-commutative
case (for two matrices the transpose identity is restricted to the
commutative case in the original version anyway).
On 21-Nov-24 8:47 PM, Stepan Holub (via cl-isabelle-users Mailing List)
wrote:
Dear Alexander,
thank you very much. Accidentally I have just written almost the same
patch (for HOL-Analysis only), attached.It contains two additional minor suggestions:
- vector_scalar_commute and scalar_vector_matrix_assoc can be
generalized from field to comm_semiring_1
- vector_matrix_mul_assoc in Cartesian_Space is now a (weaker)
duplicate and can be deleted.Best regards
Stepan
On 21-Nov-24 7:46 PM, Alexander Pach wrote:
Dear all,
as vector_matrix_mult is surprisingly rarely used, only minor
adaptions are needed. See attached file 81471.patch for Isabelle and
15047.patch for the AFP, which also adapts
Vector-Matrix-Multiplications for AFP-defined arrays, where
necessary. Feel free to use them in any way you see fit.I have successfully built all sessions using vector_matrix_mult in
their theory files, but not all possibly impacted sessions due to
performance constraints, so I'd appreciate someone doing a complete
build.Kind regards
Alexander PachP.S. Groebner_Bases has a definition with correct term order in
Macaulay_Matrix at line 31:mult_vec_mat :: "'a vec \<Rightarrow> 'a :: semiring_0 mat \<Rightarrow> 'a vec" (infixl "\<^sub>v*" 70)
where "v \<^sub>v* A \<equiv> vec (dim_col A) (\<lambda>j. v \<bullet> col A j)"
Am 2024-11-20 um 11:50 schrieb Lawrence Paulson:I ported vast chunks of this library (from HOL Light). But the operative word is “ported”; I didn't change any definitions. This particular file however, lists the author as Amine Chaieb (Who gave us formal power series). Anyway the question is simple: what do textbooks say?
Of course it is not esoteric. This sort of basic definition needs to be correct.
Larry
On 19 Nov 2024, at 15:38, Manuel Eberl<manuel@pruvisto.org> wrote:
it might well be that I am the only HOL-Analysis person remaining among the core Isabelle developers. I've never used the matrices in HOL-Analysis, so I am completely unfamiliar with that library. But if I am indeed the only person who is in a position to do anything about it, I will look into it.
Perhaps some more people using that library can chime in?
Email Gateway (Nov 22 2024 at 14:57):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks both, now installed.
Larry
On 21 Nov 2024, at 19:47, Stepan Holub <holub@karlin.mff.cuni.cz> wrote:
Dear Alexander,
thank you very much. Accidentally I have just written almost the same patch (for HOL-Analysis only), attached.
It contains two additional minor suggestions:
- vector_scalar_commute and scalar_vector_matrix_assoc can be generalized from field to comm_semiring_1
- vector_matrix_mul_assoc in Cartesian_Space is now a (weaker) duplicate and can be deleted.Best regards
Stepan
On 21-Nov-24 7:46 PM, Alexander Pach wrote:
Dear all,
as vector_matrix_mult is surprisingly rarely used, only minor adaptions are needed. See attached file 81471.patch for Isabelle and 15047.patch for the AFP, which also adapts Vector-Matrix-Multiplications for AFP-defined arrays, where necessary. Feel free to use them in any way you see fit.
I have successfully built all sessions using vector_matrix_mult in their theory files, but not all possibly impacted sessions due to performance constraints, so I'd appreciate someone doing a complete build.
Kind regards
Alexander PachP.S. Groebner_Bases has a definition with correct term order in Macaulay_Matrix at line 31:
mult_vec_mat :: "'a vec \<Rightarrow> 'a :: semiring_0 mat \<Rightarrow> 'a vec" (infixl "\<^sub>v*" 70)
where "v \<^sub>v* A \<equiv> vec (dim_col A) (\<lambda>j. v \<bullet> col A j)"
Am 2024-11-20 um 11:50 schrieb Lawrence Paulson:I ported vast chunks of this library (from HOL Light). But the operative word is “ported”; I didn't change any definitions. This particular file however, lists the author as Amine Chaieb (Who gave us formal power series). Anyway the question is simple: what do textbooks say?
Of course it is not esoteric. This sort of basic definition needs to be correct.
Larry
On 19 Nov 2024, at 15:38, Manuel Eberl <manuel@pruvisto.org> wrote:
it might well be that I am the only HOL-Analysis person remaining among the core Isabelle developers. I've never used the matrices in HOL-Analysis, so I am completely unfamiliar with that library. But if I am indeed the only person who is in a position to do anything about it, I will look into it.
Perhaps some more people using that library can chime in?<vector_matrix_mult.patch>
Last updated: Jan 04 2025 at 20:18 UTC