Yves Bertot (Aug 23 2021 at 11:03): Yves Bertot (Aug 23 2021 at 11:03):Hello, I would like to apply matrix knowledge to the resolution of a system of two linear equations with two unknowns. So I have :
A * x + B * y + C = 0 and D * x + E * y + F = 0, and I know (x1, y1) such that the first left member is positive and the second one is 0, and (x2,y2) such that the first left member is negative and the second one is 0. I would like to prove that the system has a solution that is unique. I was thinking of using the matrix M that has A B D E as coefficient, show that because of the two witnesses this matrix is invertible, and just say the solution has to be A ^-1 *m V where V is the colon vector with C and F as coefficient.
I am already stuck at the objective of showing that my system of equations is the same as A *m X + F = 0. How can I expand the definition of matrix multiplication?
Yves Bertot (Aug 23 2021 at 11:03):How does one use mulmx_key?
Yves Bertot (Aug 23 2021 at 11:30):I think I found a solution: use matrixP and reason on each coefficient separately relying on mxE.
Yves Bertot (Aug 23 2021 at 11:51):Here is a snippet (the function mkmx2 constructs a 2 by 2 matrix with the 4 coefficients, and the function mkcv2 is the same for a vector of dimension 2).
set M := mkmx2 A B D E.
set V1 := mkcv2 (b_x - a_x) (b_y - a_y).
set V2 := mkcv2 (d_x - c_x) (d_y - c_y).
have sys_to_mx_eqn :
forall x y, (A * x + B * y + C = 0 /\ D * x + E * y + F = 0) <->
(M *m (\col_(i < 2) if i == ord0 then x else y) +
(\col_(i < 2) if i == ord0 then C else F) = 0).
move=> x y; split.
move=> [eq1 eq2]; apply/matrixP=> i [ [ | j] jp] //; rewrite !mxE.
rewrite big_ord_recr /= big_ord1 /= !mxE /= {jp}.
by move: i=> [[ | [ | [ | i]]]].
move/matrixP=> mxeqn; split.
suff : A * x + B * y + C = 0 by [].
have := mxeqn (Ordinal (isT : (0 < 2)%N)) (Ordinal (isT : (0 < 1)%N)).
by rewrite !mxE /= big_ord_recr /= big_ord1 /= !mxE /=.
suff : D * x + E * y + F = 0 by [].
have := mxeqn (Ordinal (isT : (1 < 2)%N)) (Ordinal (isT : (0 < 1)%N)).
by rewrite !mxE /= big_ord_recr /= big_ord1 /= !mxE /=.
It may look long, but in fact there is a lot of repetition.
Pierre Roux (Aug 23 2021 at 12:51):Would using block_mx and col_mx instead of custom mkmx2 and mkcv2 help?
Yves Bertot (Aug 23 2021 at 14:43):I needed to have function that make it short to construct a matrix from the coefficients. The function block_mx and col_mx make it easier to build matrices from inputs that are already matrices.
Yves Bertot (Aug 23 2021 at 14:48):By the way, I have solved my use case with two linear equations and two unknowns. It turns out that the determinant of the matrix M is a multiple of the difference of A * x + B * y + C at points (x1, y1) and (x2, y2). Unicity works well, but it is cumbersome that there is no existing theorem stating that multiplication by a unitmx is injective.
Pierre Roux (Aug 26 2021 at 16:00):@Yves Bertot maybe using mulrI ( https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L2983 ) since matrix are equipped with a unitRingType.
Yves Bertot (Aug 30 2021 at 06:31):@Pierre Roux , thanks for the suggestion, it does not work because I am multiplying by a matrix in unitmx but left hand side and the right hand side are not in the same type (one type is 'M_2, the other is `'cV_2'), so I am not working in a unitRingType.
YAMAMOTO Mitsuharu (Aug 30 2021 at 07:04):Does can_inj/can_eq together with mulKmx/mulmxK work? I can find several uses of these combinations in mathcomp.
Yves Bertot (Aug 30 2021 at 07:27):Thanks @YAMAMOTO Mitsuharu , you are giving the right pointers: I should use mulKmx. Here is an example, with the following goal:
M \in unitmx -> M *m V = V' -> V = M^-1 *m V'
I can solve the goal with the following line:
by move=> Munit solmv; rewrite -solmv mulKmx.
If I don't already have the hypothesis M *m V = V', I can start with the following goal :
M \in unitmx -> V = M^-1 *m V'
and use the following tactic:
move=>Munit; apply: (can_inj (mulKmx Munit)); rewrite mulKVmx.
and end up with the following goal conclusion:
M *m V = V'
YAMAMOTO Mitsuharu (Aug 30 2021 at 07:52):Alternatively,
move=> Munit; apply: canRL (mulKmx Munit).
and
move=> Munit; apply: canRL (mulKmx Munit) _.,
respectively.
Last updated: Oct 13 2024 at 01:02 UTC