W=WeylGroup('F4',prefix="s");
print('Cardinal de W= ',W.cardinality());

N=len(W.domain().positive_roots());

print('Classement of elements of W by', N, 'lenths and computations of inversion sets...');

Rplus=W.domain().positive_roots();

def inversionroot(w):# j =0 ou 1 pour G ou Ghat
    liste=[];
    for a in Rplus:
        if (w.action(a).is_positive_root()==False) : liste.append(a);
    return(liste);

Wl=[];
for i in range(N+1) :
    Wl.append([]);
for w in W : Wl[w.length()].append([w,inversionroot(w)]);



def exist(inv1,l) :
    for w in Wl[l] :
        #if (w.length()==l) :
        if (inv1==set(w[1])) : return([True,w]);
    return([False,1])
                
def pr(w) :
    p=1;
    for a in inversionroot(w) :
        p=p*(W.domain().rho().scalar(a));
    return(p);


print('On entre dans la boucle...');

total=0
fichier = open("sortieF4_Manuel.txt", "w")
for lu in range(3,N//3+1):# we sort in such a way 3<=l(u)<=l(v)<=l(w^\vee)<N   	  		   
    print('On teste u de longeur ',lu, 'sur ',N//3+1);
    for u in Wl[lu]:
    	#invu=inversionroot(u)
	invu=u[1]
	#print(invu)
	sinvu=set(invu)
	u=u[0]
	pu=pr(u.inverse());
	#print(pu)
    	for lv in range(lu,(N-lu)//2+1):
	    for v in Wl[lv]:
	        invv=v[1]
	    	if (sinvu.isdisjoint(invv)) :
		   v=v[0]
		   w=exist(set(invu+invv),lu+lv)
		   #print(w)
		   if w[0] :
                      w=w[1][0]
		      #w=winv.inverse()
                      pv=pr(v.inverse());pw=pr(w.inverse());
                      if (pu*pv!=pw) : print('CONTRE EXEMPLE',u,v,w,pu,pv,pw);fichier.write('CONTRE EXEMPLE :\n');
		      print('u= '+str(u)+' ; v= '+str(v)+' ; w= '+str(w))
                      print('pu=',pu,'pv=',pv,'pw=',pw)
		      fichier.write('u= '+str(u)+' ; v= '+str(v)+' ; w= '+str(w)+'\n')
		      fichier.write('pu= '+str(pu)+' ; pv= '+str(pv)+' ; pw= '+str(pw)+'\n\n')
		      total+=1
    		   
fichier.close()
print('Total',total)