Ssreflect Users Discussion List

[Jónathan Heras <>]

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