I'm not sure I necessarily understand all of your question, but it seems as if you are hoping to prove the
(x * y = 0) <=> (x = 0) \/ (y = 0) property for multiplication in your linear space. Your vectors are lists of coefficients, so that x = 0 really means that the list x consists only of zeroes. You say you want to prove (perhaps by induction) (LENGTH x = LENGTH y) /\ (x * y = 0) /\ EVERY (\e. e <> 0) x ==> EVERY (\e. e = 0) y This is not right though. You should have EXISTS (\e. e <> 0) x as an assumption. In other words, to be a non-zero vector, it is enough to have one element be non-zero. It is not necessary to have *all* elements be non-zero. Note how you don't need to define P and Q separately as constants, just write out the lambda-expression. Michael On 22/03/13 7:46 PM, Yuntao Peng wrote: > I want to prove a property of linear space. Property description as follows: > If exist unique β, and β = p_1 α_1 +p_2 α_2 +…+p_n α_n , then α_1, α_2 , > … , α_n linearly independent. > Where β, α_1, α_2 , … , α_n are the elements of linearly space, and > p_1, p_2, … , p_n are complex. > Derivation： > β = p_1 α_1 +p_2 α_2 +…+p_n α_n (1) > 0 = k_1 α_1 +k_2 α_2 +…+k_n α_n (2)_ > (1)+ (2) ==> β = p_1 α_1 +p_2 α_2 +…+p_n α_n = (k_1 +p_1 )α_1 +(k_2 > +p_2 )α_2 +…+(k_n +p_n )α_n > ==> k1=0, k2=0,…, kn=0 ==> α_1, α_2 , … , α_n linearly independent > Now, I have proved a goal, and save it as a theorem. > g `!k:complex x:'a. (k LM x = ls0) /\ (x <> ls0) ==> (k = 0)` > Where “LM” is multiplication sign of linear space, “ls0” is zero of > linear space. > My question is how to prove the goal as follows? > g `!l1:complex list l2:'a list. (LENGTH l1 = LENGTH l2) /\ (LMP(l1,l2) = > ls0) /\ (EVERY P l2) ==> (EVERY Q l1)`; > Where“LN” is plus of linear space. > val ls_mult_add = > Define > `(LMP ([],l2:'a list) = ls0) /\ > (LMP ((h1::t1):complex list,l2:'a list) = if (l2 = []) then ls0 > else (h1 LM HD l2) > LP (LMP (t1,TL l2)))`; > if l1=(p1,p2,…,pn), l2=(α_1 ,α_2 ,…,α_n ) , then LMP(l1,l2) = p_1 α_1 > +p_2 α_2 +…+p_n α_n > val Q_def = Define `!x:complex. Q x = (x = 0c)`; > val P_def = Define `!x:'a. P x = (x <> ls0)`; > I am looking forward your advice. > Thanks. > Peng. > ------------------------------------------------------------------------------ > Everyone hates slow websites. So do we. > Make your web apps faster with AppDynamics > Download AppDynamics Lite for free today: > http://p.sf.net/sfu/appdyn_d2d_mar > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Everyone hates slow websites. So do we. Make your web apps faster with AppDynamics Download AppDynamics Lite for free today: http://p.sf.net/sfu/appdyn_d2d_mar
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
