[isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Lawrence Paulson]

Is there a case for moving some material from this file into the Analysis 
directory?

https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
 


Many of the results proved at the end of this file are quite straightforward 
anyway. As somebody with a lifting-and-transfer phobia, I don't feel qualified 
to make this decision. Possibly these techniques are overkill. I have already 
proved some of these results quite straightforwardly using linearity, and 
installed them not long ago.

Larry

> Begin forwarded message:
> 
> From: Fabian Immler 
> Subject: Re: [isabelle] Matrix-Vector operation
> Date: 26 February 2018 at 08:02:40 GMT
> To: isabelle-users 
> Cc: Omar Jasim 
> 
> Dear Omar,
> 
> Unfortunately, there are no lemmas on distributivity of *v in the 
> distribution.
> Some are currently in the AFP-entry Perron_Frobenius:
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> You can prove them (in HOL-Analysis) as follows:
> 
> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: 
> ring_1 ^ 'n)"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf left_diff_distrib)
> 
> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_right)
> 
> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_left)
> 
> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v 
> (v - w) = M *v v - M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf right_diff_distrib)
> 
> Those should probably be included in the next Isabelle release.
> 
> Hope this helps,
> Fabian
> 
> 
>> Am 25.02.2018 um 19:27 schrieb Omar Jasim :
>> 
>> Hi,
>> 
>> This may be trivial but I have a difficulty proving the following lemma:
>> 
>> lemma
>> fixes  A :: "real^3^3"
>>   and x::"real^3"
>> assumes "A>0"
>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>> 
>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>> related to this?
>> 
>> Cheers
>> Omar
> 



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Fabian Immler]

> Am 26.02.2018 um 12:54 schrieb Lawrence Paulson :
> 
> Is there a case for moving some material from this file into the Analysis 
> directory?
> 
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> Many of the results proved at the end of this file are quite straightforward 
> anyway. As somebody with a lifting-and-transfer phobia, I don't feel 
> qualified to make this decision. Possibly these techniques are overkill. I 
> have already proved some of these results quite straightforwardly using 
> linearity, and installed them not long ago.
For the record, "not long ago" is c8caefb20564. I generalized this to the same 
class constraints as in HMA_Connect in d97a28a006f9.

Yes, I guess these techniques are overkill for the (straightforward) proofs of
matrix_add_vect_distrib,
matrix_vector_right_distrib,
matrix_vector_right_distrib_diff,
matrix_diff_vect_distrib
(they are exactly the lemmas touched by d97a28a006f9). I left them in 
HMA_Connect.thy as examples for the transfer_hma method.

The remaining lemmas at the end of HMA_Connect are probably not so easy to move 
to the distribution: they involve concepts that are missing in HOL-Analysis, 
e.g., eigen_value, charpoly, or similar_matrix.

We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
Analysis/Finite_Cartesian_Product both formalize vectors and matrices and that 
there are formalizations of (aspects of) linear algebra for both of them. Last 
year in Logrono, there was the proposal to put all linear algebra on the common 
foundation of a locale for modules, but apparently nobody has found the time 
and motivation to push this much further.

Perhaps a more humble first step towards unifying the existing theories would 
be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do the 
construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.

Any opinions on that?

Fabian



> Larry
> 
>> Begin forwarded message:
>> 
>> From: Fabian Immler 
>> Subject: Re: [isabelle] Matrix-Vector operation
>> Date: 26 February 2018 at 08:02:40 GMT
>> To: isabelle-users 
>> Cc: Omar Jasim 
>> 
>> Dear Omar,
>> 
>> Unfortunately, there are no lemmas on distributivity of *v in the 
>> distribution.
>> Some are currently in the AFP-entry Perron_Frobenius:
>> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
>> 
>> You can prove them (in HOL-Analysis) as follows:
>> 
>> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: 
>> ring_1 ^ 'n)"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf left_diff_distrib)
>> 
>> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_right)
>> 
>> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_left)
>> 
>> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v 
>> (v - w) = M *v v - M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf right_diff_distrib)
>> 
>> Those should probably be included in the next Isabelle release.
>> 
>> Hope this helps,
>> Fabian
>> 
>> 
>>> Am 25.02.2018 um 19:27 schrieb Omar Jasim :
>>> 
>>> Hi,
>>> 
>>> This may be trivial but I have a difficulty proving the following lemma:
>>> 
>>> lemma
>>> fixes  A :: "real^3^3"
>>>   and x::"real^3"
>>> assumes "A>0"
>>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>>> 
>>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>>> related to this?
>>> 
>>> Cheers
>>> Omar
>> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Lawrence Paulson]

I was at the meeting in Logroño and my impression was that we had to live with 
these different formalisations. There was no way to unify them and the best one 
could hope to transfer certain results from one formalisation to another using 
local types in some incredibly complicated way.

If there really is a common basis for formalising linear algebra than I would 
be thrilled to see it, and I'm sure we could figure out a way to implement this.

Larry

> On 26 Feb 2018, at 14:57, Fabian Immler  wrote:
> 
> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
> that there are formalizations of (aspects of) linear algebra for both of 
> them. Last year in Logrono, there was the proposal to put all linear algebra 
> on the common foundation of a locale for modules, but apparently nobody has 
> found the time and motivation to push this much further.
> 
> Perhaps a more humble first step towards unifying the existing theories would 
> be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do the 
> construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.
> 
> Any opinions on that?



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Fabian Immler]

> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson :
> 
> I was at the meeting in Logroño and my impression was that we had to live 
> with these different formalisations. There was no way to unify them and the 
> best one could hope to transfer certain results from one formalisation to 
> another using local types in some incredibly complicated way.
HMA_Connect shows a way to unify (at least parts of) them: it makes explicit 
that 'a^'n^'m can be seen as a subtype of 'a mat.

This makes it possible to avoid duplications: for example, results about 
eigenvalues are only proved once for 'a mat and are transferred to the 
"subtype" 'a^'n^'m.
In contrast to that, we do have duplicate developments for determinants, 
multiplication etc. in isabelle and the AFP. We should be able to get rid of 
those.

Ideally, one would do the developments for 'a^'n^'m, but I am not sure how well 
theorems can be transferred in that direction...

Fabian


> If there really is a common basis for formalising linear algebra than I would 
> be thrilled to see it, and I'm sure we could figure out a way to implement 
> this.
> 
> Larry
> 
>> On 26 Feb 2018, at 14:57, Fabian Immler > > wrote:
>> 
>> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
>> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
>> that there are formalizations of (aspects of) linear algebra for both of 
>> them. Last year in Logrono, there was the proposal to put all linear algebra 
>> on the common foundation of a locale for modules, but apparently nobody has 
>> found the time and motivation to push this much further.
>> 
>> Perhaps a more humble first step towards unifying the existing theories 
>> would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do 
>> the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.
>> 
>> Any opinions on that?
> 



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Thiemann, Rene]

Dear all,

with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a 
mat”.
However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get 
the additional
constraint that the dimensions of the matrix must be non-zero.

To be more precise, assume the following two lemmas (where I omit 
sort-constraints):

lemma one: 
  fixes A B :: “‘a^’n^’m”
  shows “A + B = B + A” 

lemma two: 
  fixes A B :: “‘a mat”
  shows “A : carrier_mat n m ==> B : carrier_mat n m ==> A + B = B + A” 

From “two” and HMA_Connect you can easily get “one”.
But from “one” and HMA_Connect you only get “three” via transfer:  

lemma three: 
  fixes A B :: “‘a mat”
  shows “n ~= 0 ==> m ~= 0 ==> A : carrier_mat n m ==> B : carrier_mat n m ==> 
A + B = B + A” 

To obtain “two” from “three", one would have to manually proof the result for 
the corner cases “n = 0 \/ m = 0”.


But indeed, Fabian is completely right that lemmas for determinants, etc. are 
duplicates. Actually, the JNF-matrices “‘a mat” 
have been developed from scratch (without HMA_Connect), by manually copying and 
adapting several proofs from the distribution.

Cheers,
René

> Am 26.02.2018 um 18:28 schrieb Fabian Immler :
> 
> 
>> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson :
>> 
>> I was at the meeting in Logroño and my impression was that we had to live 
>> with these different formalisations. There was no way to unify them and the 
>> best one could hope to transfer certain results from one formalisation to 
>> another using local types in some incredibly complicated way.
> HMA_Connect shows a way to unify (at least parts of) them: it makes explicit 
> that 'a^'n^'m can be seen as a subtype of 'a mat.
> 
> This makes it possible to avoid duplications: for example, results about 
> eigenvalues are only proved once for 'a mat and are transferred to the 
> "subtype" 'a^'n^'m.
> In contrast to that, we do have duplicate developments for determinants, 
> multiplication etc. in isabelle and the AFP. We should be able to get rid of 
> those.
> 
> Ideally, one would do the developments for 'a^'n^'m, but I am not sure how 
> well theorems can be transferred in that direction...
> 
> Fabian
> 
> 
>> If there really is a common basis for formalising linear algebra than I 
>> would be thrilled to see it, and I'm sure we could figure out a way to 
>> implement this.
>> 
>> Larry
>> 
>>> On 26 Feb 2018, at 14:57, Fabian Immler >> > wrote:
>>> 
>>> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
>>> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
>>> that there are formalizations of (aspects of) linear algebra for both of 
>>> them. Last year in Logrono, there was the proposal to put all linear 
>>> algebra on the common foundation of a locale for modules, but apparently 
>>> nobody has found the time and motivation to push this much further.
>>> 
>>> Perhaps a more humble first step towards unifying the existing theories 
>>> would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do 
>>> the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.
>>> 
>>> Any opinions on that?
>> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev