Ssreflect Users Discussion List

[Jónathan Heras <>]

Hi,

I guess that I was misreading the notation. Thank you for the explanation.

Cheers,
Jónathan


On 27/03/12 11:07, Georges Gonthier wrote:
>      Hi Jonathan,
>   I don't see how you could expect such  properties: the choice of a 
> complementary subspace is necessarily arbitrary. Are you misreading the 
> notation?
>         U :\: V is a complement to U :&: V in U as a subspace, i.e., it is a 
> (somewhat arbitrary) subspace of U such that
>    (U :&: V + U :\: V)%VS = U and the sum on the left-hand side is direct.
> You can write the set-theoretic complement to V in U as [predD U&  V] -- this 
> is a (collective) vector predicate, but not a subspace.
>    u \in [predD U :\: V] will be expanded to (u \notin V)&&  (u \in U) by the 
> inE lemma (indeed, the two boolean formulas are convertible).
> If you did mean u \in U :\: V, then lemmas diffvSl and capv_diff tell you 
> respectively that u \in U and u \in V ->  u = 0, with some elementary 
> reasoning, but these conditions do not imply, conversely, u \in U:\: V...
>    Best,
>    Georges
>
> -----Original Message-----
> From: Jónathan Heras []
> Sent: 27 March 2012 07:26
> To: 
> Subject: Re: Property about diff of vector spaces
>
> Hi Georges,
>
> Roughly speaking, I am trying to prove that if x \in A:\:B then x satisfies some 
> concrete properties; so, I would like to know when x belongs to A :\: B; that is, I 
> need a mem_diff theorem; therefore I was trying to prove that false lemma (V1 :\: V2  
> == V1 :&: ((V1 :&:
> V2)^C)) in order to apply it
> and subsequently use the memv_cap lemma ((v \in vs1 :&: vs2) = (v \in
> vs1)&&  (v \in vs2)).
>
> So, I need a mem_diff lemma but I am not sure about what is the statement of 
> this lemma.
>
> Cheers,
> Jónathan
>
>
> On 26/03/12 23:02, Georges Gonthier wrote:
> >     Hi Jonathan,
> > I'm afraid the reason you can't complete your proof is simply that the lemma 
> > doesn't hold.
> > (U :\: V)%VS is some complement to V in U, (U :&: (U :&: V)^C)%VS is another 
> > one, and they do not have to be equal.
> >      As picking a complement necessarily involves some arbitrary
> > choice, and (see my ITP 2011 paper) Gaussian elimination naturally provided a complement, I 
> > did not standardize the complement in the mxalgebra library -- so although (capmx_gen A B :=: 
> > A :&:B)%MS it is not the case than ((capmx_gen A B)^C :=: (A :&:B)^C)%MS. I chose to 
> > use capmx_gen A B (the precursor to A :&: B) in the definition of A :\: B because it 
> > simplified the internal theory somewhat (the precise definition of A :&: B involves a few 
> > twists that ensure the operator is strictly monoidal). I did not expect there would be proofs 
> > where a particular choice of A :\: B would matter; similarly Laurent Théry and Laurance 
> > Rideau, who created the vector library, based U :\: V on A :\: B because this simplified the 
> > task of transferring results from mxalgebra to vector. Do you have a use case where the 
> > diffvE identity would be genuinely useful ?
> >      Cheers,
> > Georges
> >
> > -----Original Message-----
> > From: Jónathan Heras []
> > Sent: 26 March 2012 19:21
> > To: 
> > Subject: Property about diff of vector spaces
> >
> > Hi,
> >
> > I was trying to prove that (V1 :\: V2)%VS   == V1 :&: ((V1 :&: V2)^C).
> > My attempt was:
> >
> > Lemma diffvE (V :vectType K) (vs1 vs2 : {vspace V}) : (vs1 :\: vs2) =
> > (vs1 :&: ((vs1 :&: vs2)^C)).
> > Proof.
> > rewrite /diffv /capv /complv capv_mx2vsr.
> > apply/eqP. rewrite -mxeq2vseq.
> > apply/eqmxP.
> > have H : (vs2mx vs1 :&: (capmx_gen (vs2mx vs1) (vs2mx vs2))^C :=:
> > vs2mx
> > vs1 :&: (vs2mx (mx2vs (vs2mx vs1 :&: vs2mx vs2)))^C)%MS;
> >      last by apply : eqmx_trans (diffmxE (vs2mx vs1) (vs2mx vs2)) H.
> > apply : cap_eqmx; first by done.
> > rewrite capv_mx2vs !vs2mxK.
> >
> >
> > At this point I am not able to continue, I would like to apply the lemma which 
> > says: A :&: B :=: capmx_gen A B but it seems that I cannot apply it.
> >
> > Any suggestions?
> >
> > Thank you in advance.
> >
> > Sincerely. Jónathan