299 lines
11 KiB
Python
299 lines
11 KiB
Python
|
from sys import argv
|
||
|
|
from pathlib import Path
|
||
|
|
|
||
|
|
from common import printc, printerr, replaceContent
|
||
|
|
import Graph
|
||
|
|
|
||
|
|
# Increase if hasse diagram becomes too clobbered
|
||
|
|
|
||
|
|
def pairToString(pair):
|
||
|
|
if str(pair[0]).isdigit() or str(pair[1]).isdigit():
|
||
|
|
return f'({pair[0]},{pair[1]})'
|
||
|
|
else:
|
||
|
|
return pair[0] + pair[1]
|
||
|
|
|
||
|
|
def stringToPair(string):
|
||
|
|
if string[0] == '(':
|
||
|
|
return tuple([string.split(',')[0][1:], string.split(',')[0][:-1]])
|
||
|
|
else:
|
||
|
|
return tuple(list(string))
|
||
|
|
|
||
|
|
def textLatex(string):
|
||
|
|
return '\\text{' + string + '}'
|
||
|
|
|
||
|
|
def mathModeListLatex(elements):
|
||
|
|
if len(elements) > 7 or len(elements) and max(len(str(e)) for e in elements) > 10:
|
||
|
|
return '\\begin{gather*}\n' \
|
||
|
|
+ ' \\\\\n'.join(elements) + '\n' \
|
||
|
|
+ '\\end{gather*}'
|
||
|
|
else:
|
||
|
|
return f'\\[ {", ".join(elements)} \\]'
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
class Relation:
|
||
|
|
def __init__(self, pairs): # pair = (str,str)
|
||
|
|
self.pairs = set(pairs)
|
||
|
|
|
||
|
|
def __str__(self):
|
||
|
|
return f'\\{{ {", ".join(x + y for x,y in self.pairs)} \}}'
|
||
|
|
|
||
|
|
@classmethod
|
||
|
|
def fromString(cls, string):
|
||
|
|
relations = (stringToPair(x) for x in string.split(' '))
|
||
|
|
return cls(relations)
|
||
|
|
|
||
|
|
@classmethod
|
||
|
|
def fromDivisibilityPosetTo(cls, n):
|
||
|
|
pairs = set()
|
||
|
|
for dst in range(n):
|
||
|
|
pairs.add((dst, dst))
|
||
|
|
for src in range(1, dst):
|
||
|
|
if dst % src == 0:
|
||
|
|
pairs.add((src, dst))
|
||
|
|
return cls(pairs)
|
||
|
|
|
||
|
|
|
||
|
|
def isReflexive(self, verbose=False):
|
||
|
|
elements = set(list(sum(self.pairs, ())))
|
||
|
|
result = all((x,x) in self.pairs for x in elements)
|
||
|
|
|
||
|
|
if not result:
|
||
|
|
printc('Not reflexive, missing following pairs:', color='green')
|
||
|
|
missingPairs = [(x,x) for x in elements if (x,x) not in self.pairs]
|
||
|
|
print(f'\\[ {", ".join(pairToString(p) for p in missingPairs)} \\]')
|
||
|
|
if verbose:
|
||
|
|
return (False, missingPairs)
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
return (True, [(x,x) for x in elements if (x,x) in self.pairs])
|
||
|
|
|
||
|
|
return result
|
||
|
|
|
||
|
|
def isSymmetric(self, verbose=False):
|
||
|
|
result = all((y,x) in self.pairs for x,y in self.pairs)
|
||
|
|
|
||
|
|
if not result:
|
||
|
|
printc('Not symmetric, missing following pairs:', color='green')
|
||
|
|
missingPairs = [(x,y) for x,y in self.pairs if (y,x) not in self.pairs]
|
||
|
|
print(f'\\[ {", ".join(pairToString(p) for p in missingPairs)} \\]')
|
||
|
|
if verbose:
|
||
|
|
return (False, missingPairs)
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
return (True, [((x,y), (y,x)) for x,y in self.pairs if (y,x) in self.pairs and x < y])
|
||
|
|
|
||
|
|
return result
|
||
|
|
|
||
|
|
def isAntiSymmetric(self, verbose=False):
|
||
|
|
result = not any((y,x) in self.pairs and y != x for x,y in self.pairs)
|
||
|
|
|
||
|
|
if not result:
|
||
|
|
printc('Not antisymmetric, following pairs are symmetric:', color='green')
|
||
|
|
symmetricPairs = [((x,y), (y,x)) for x,y in self.pairs if (y,x) in self.pairs and y > x]
|
||
|
|
print(f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}""" for p,q in symmetricPairs)} \\]')
|
||
|
|
if verbose:
|
||
|
|
return (False, symmetricPairs)
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
return (True, [])
|
||
|
|
|
||
|
|
return result
|
||
|
|
|
||
|
|
def isTransitive(self, verbose=False):
|
||
|
|
result = True
|
||
|
|
transitivePairs = []
|
||
|
|
nonTransitivePairs = []
|
||
|
|
|
||
|
|
for x,y in self.pairs:
|
||
|
|
for z,w in self.pairs:
|
||
|
|
if not (y != z or ((x,w) in self.pairs)):
|
||
|
|
nonTransitivePairs.append(((x,y), (z,w)))
|
||
|
|
result = False
|
||
|
|
elif (y == z and x != y != w and ((x,w) in self.pairs)):
|
||
|
|
transitivePairs.append(((x,y), (z,w)))
|
||
|
|
|
||
|
|
if not result:
|
||
|
|
printc('Not transitive, following pairs are missing its transitive counterpart:', color='green')
|
||
|
|
print(f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}{textLatex(" without ")}{pairToString((p[0], q[1]))}""" for p,q in nonTransitivePairs)} \\]')
|
||
|
|
if verbose:
|
||
|
|
return (False, nonTransitivePairs)
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
return (True, transitivePairs)
|
||
|
|
|
||
|
|
return result
|
||
|
|
|
||
|
|
def isEquivalenceRelation(self, verbose=False):
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
isReflexive, reflexivePairs = self.isReflexive(verbose=True)
|
||
|
|
isSymmetric, symmetricPairs = self.isSymmetric(verbose=True)
|
||
|
|
isTransitive, transitivePairs = self.isTransitive(verbose=True)
|
||
|
|
|
||
|
|
if not isReflexive:
|
||
|
|
return 'The relation is not an equivalence relation, because it is not reflexive.'
|
||
|
|
+ ' The following elements should be related:\n\n'
|
||
|
|
+ f'\\[ {", ".join(pairToString(p) for p in reflexivePairs)} \\]'
|
||
|
|
if not isSymmetric:
|
||
|
|
return 'The relation is not an equivalence relation, because it is not symmetric.'
|
||
|
|
+ ' It is missing the following symmetric pairs of relations\n\n'
|
||
|
|
+ f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}""" for p,q in symmetricPairs)} \\]'
|
||
|
|
if not isTransitive:
|
||
|
|
return 'The relation is not an equivalence relation, because it is not transitive.'
|
||
|
|
+ ' The following pairs of relations are missing its transitive counterpart\n\n'
|
||
|
|
+ f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}{textLatex(" without ")}{pairToString((p[0], q[1]))}""" for p,q in transitivePairs)} \\]'
|
||
|
|
|
||
|
|
|
||
|
|
rxStr = mathModeListLatex([pairToString(p) for p in reflexivePairs])
|
||
|
|
smStr = mathModeListLatex([f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}""" for p,q in symmetricPairs])
|
||
|
|
trStr = mathModeListLatex([f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}{textLatex(" with ")}{pairToString((p[0], q[1]))}""" for p,q in transitivePairs])
|
||
|
|
|
||
|
|
return replaceContent(
|
||
|
|
(rxStr, smStr, trStr),
|
||
|
|
'Relations/EquivalenceProof',
|
||
|
|
lambda temp, cont: temp.replace('%REFLEXIVE', cont[0]).replace('%SYMMETRIC', cont[1]).replace('%TRANSITIVE', cont[2])
|
||
|
|
)
|
||
|
|
|
||
|
|
return self.isReflexive() and self.isSymmetric() and self.isTransitive()
|
||
|
|
|
||
|
|
def isPartialOrder(self, verbose=False):
|
||
|
|
|
||
|
|
result = self.isReflexive() and self.isAntiSymmetric() and self.isTransitive()
|
||
|
|
|
||
|
|
if result:
|
||
|
|
hasse= self.getHassePairs(checkIfPartialOrder=False)
|
||
|
|
min_el = set(a for a,b in hasse if a not in list(zip(*hasse))[1])
|
||
|
|
printc(f"Minimal elements: $\{{ {', '.join(str(e) for e in min_el)} \}}$ \\\\")
|
||
|
|
|
||
|
|
max_el = set(v for k,v in hasse if v not in (x for x,_ in hasse))
|
||
|
|
printc(f"Maximal elements: $\{{ {', '.join(str(e) for e in max_el)} \}}$" )
|
||
|
|
|
||
|
|
if verbose:
|
||
|
|
isReflexive, reflexivePairs = self.isReflexive(verbose=True)
|
||
|
|
isAntiSymmetric, antiSymmetricPairs = self.isAntiSymmetric(verbose=True)
|
||
|
|
isTransitive, transitivePairs = self.isTransitive(verbose=True)
|
||
|
|
|
||
|
|
if not isReflexive:
|
||
|
|
return 'The relation is not a partial order, because it is not reflexive.'
|
||
|
|
+ ' The following elements should be related:\n\n'
|
||
|
|
+ f'\\[ {", ".join(pairToString(p) for p in reflexivePairs)} \\]'
|
||
|
|
if not isAntiSymmetric:
|
||
|
|
return 'The relation is not a partial order, because it is not antisymmetric.'
|
||
|
|
+ ' The following relations are symmetric\n\n'
|
||
|
|
+ f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}""" for p,q in antiSymmetricPairs)} \\]'
|
||
|
|
if not isTransitive:
|
||
|
|
return 'The relation is not a partial order, because it is not transitive.'
|
||
|
|
+ ' The following pairs of relations are missing its transitive counterpart\n\n'
|
||
|
|
+ f'\\[ {", ".join(f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}{textLatex(" without ")}{pairToString((p[0], q[1]))}""" for p,q in transitivePairs)} \\]'
|
||
|
|
|
||
|
|
rxStr = mathModeListLatex([pairToString(p) for p in reflexivePairs])
|
||
|
|
trStr = mathModeListLatex([f"""{pairToString(p)}{textLatex(" and ")}{pairToString(q)}{textLatex(" with ")}{pairToString((p[0], q[1]))}""" for p,q in transitivePairs])
|
||
|
|
|
||
|
|
return replaceContent(
|
||
|
|
(rxStr, trStr),
|
||
|
|
'Relations/PosetProof',
|
||
|
|
lambda temp, cont: temp.replace('%REFLEXIVE', cont[0]).replace('%TRANSITIVE', cont[1])
|
||
|
|
)
|
||
|
|
|
||
|
|
return result
|
||
|
|
|
||
|
|
def getHassePairs(self, checkIfPartialOrder=True):
|
||
|
|
if checkIfPartialOrder and not self.isPartialOrder():
|
||
|
|
printerr('This is not a partial order')
|
||
|
|
return
|
||
|
|
|
||
|
|
nonReflexivePairs = set((x,y) for x,y in self.pairs if x != y)
|
||
|
|
|
||
|
|
hassePairs = set()
|
||
|
|
for x1, y1 in nonReflexivePairs:
|
||
|
|
for x2, y2 in nonReflexivePairs:
|
||
|
|
if y1 == x2:
|
||
|
|
hassePairs.add((x1, y2))
|
||
|
|
return nonReflexivePairs - hassePairs
|
||
|
|
|
||
|
|
def latexifyHasseDiagram(self):
|
||
|
|
hasse = self.getHassePairs()
|
||
|
|
keys = set(item for tup in hasse for item in tup)
|
||
|
|
y_pos = dict.fromkeys(keys, 0)
|
||
|
|
|
||
|
|
i = 0
|
||
|
|
while len(next_row := [val for key,val in hasse if key in [x for x,y in y_pos.items() if y == i] ]) != 0:
|
||
|
|
for item in next_row:
|
||
|
|
y_pos[item] = i + 1
|
||
|
|
i += 1
|
||
|
|
|
||
|
|
inv_ypos = dict()
|
||
|
|
for key in set(y_pos.values()):
|
||
|
|
inv_ypos[key] = [x for x,y in y_pos.items() if y == key]
|
||
|
|
|
||
|
|
output = []
|
||
|
|
|
||
|
|
for y in inv_ypos.keys():
|
||
|
|
for i, n in enumerate(inv_ypos[y]):
|
||
|
|
output.append(f'\\node ({n}) at ({i - len(inv_ypos[y])/2}, {y * 0.5 * (len(hasse) ** 0.4)}) {{${n}$}};')
|
||
|
|
|
||
|
|
output.append('')
|
||
|
|
|
||
|
|
for x,y in hasse:
|
||
|
|
output.append(f'\\draw ({x}) -- ({y});')
|
||
|
|
|
||
|
|
return '\n'.join(output)
|
||
|
|
|
||
|
|
def latexifyGraph(self):
|
||
|
|
if self.isEquivalenceRelation():
|
||
|
|
graphType = 'undirected'
|
||
|
|
pairs = [(x,y) for x,y in self.pairs if x != y]
|
||
|
|
else:
|
||
|
|
graphType = 'directed'
|
||
|
|
pairs = self.pairs
|
||
|
|
|
||
|
|
nodes = set()
|
||
|
|
for x,y in pairs:
|
||
|
|
nodes.add(x)
|
||
|
|
nodes.add(y)
|
||
|
|
|
||
|
|
edges = "\n".join(pairToString(p) for p in pairs)
|
||
|
|
|
||
|
|
processingString = f'toGraph\n\n{graphType}\n\n{ " ".join(nodes) }\n\n{edges}'
|
||
|
|
return Graph.processFileContent(processingString)
|
||
|
|
|
||
|
|
|
||
|
|
def processFileContent(raw):
|
||
|
|
outputType, inp = raw.split('\n\n')
|
||
|
|
|
||
|
|
if inp.startswith('divisibilityPosetTo'):
|
||
|
|
n = int(inp.split(' ')[1])
|
||
|
|
relation = Relation.fromDivisibilityPosetTo(n)
|
||
|
|
else:
|
||
|
|
relation = Relation.fromString(inp)
|
||
|
|
|
||
|
|
if outputType == 'proveEquivalence':
|
||
|
|
content = relation.isEquivalenceRelation(verbose=True)
|
||
|
|
return content
|
||
|
|
|
||
|
|
elif outputType == 'provePoset':
|
||
|
|
content = relation.isPartialOrder(verbose=True)
|
||
|
|
return content
|
||
|
|
|
||
|
|
elif outputType == 'hasseDiagram':
|
||
|
|
content = relation.latexifyHasseDiagram()
|
||
|
|
return replaceContent(content, 'Relations/Hasse')
|
||
|
|
|
||
|
|
elif outputType == 'graph':
|
||
|
|
content = relation.latexifyGraph()
|
||
|
|
return content
|
||
|
|
|
||
|
|
if __name__ == '__main__':
|
||
|
|
pass
|
||
|
|
relations = [(x,y) for x in range(-5, 5) for y in range(-5, 5)]
|
||
|
|
relations = [(chr(70+x), chr(70+y)) for x,y in relations if x*y >= 0]
|
||
|
|
for x in range(-5 ,5):
|
||
|
|
print(str(x) + ' - '+ chr(70 + x))
|
||
|
|
print(Relation(relations).isTransitive())
|
||
|
|
# inp = 'AA BB CC DD AB ACj
|
||
|
|
# relations = [stringToPair(p) for p in inp.split(' ')]
|
||
|
|
# # print(Relation(relations).isEquivalenceRelation())
|
||
|
|
# print(Relation(relations).isPartialOrder())
|
||
|
|
# print(Relation.fromDivisibilityPosetTo(30).isPartialOrder())
|