Ssreflect Users Discussion List

[Georges Gonthier <>]

  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