Ssreflect Users Discussion List

[Georges Gonthier <>]

    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
>
>