Symmetric_Difference_Assoc.pl

:-set_prolog_flag(encoding,utf8).
:-encoding(utf8).
:-op(500, yfx, delta).
run:-
	open('proof.txt', write, Out),
	(with_output_to(Out, test_assoc);true),
	close(Out).
test_assoc:-
	A = set('A'),
	B = set('B'),
	C = set('C'),
	Exp1 = A delta (B delta C),
	Exp2 = (A delta B) delta C,
	format('"Left side" newline\n'),
	simplify_exp(Exp1, NewExp1),
	format('\nnewline newline "Right side" newline\n'),
	simplify_exp(Exp2, NewExp2),
	nl, nl,
	!, NewExp1 = NewExp2,
	format('\nnewline newline\n"Summery:" newline\n "Right side: " ~p newline\n', [main_set(NewExp1, 'Sort the order')]),
	format('"Right side:" ~p newline', [main_set(NewExp2, 'Sort the order')]),
	format('"Left side" = "Right side"').

simplify_exp(InExp, OutExp):-
	read_exp(InExp, TempExp, main_set(_, _)),!,
	normalize_ops(TempExp, OutExp).

read_exp(set(A), set(A), _).
read_exp(\set(A), \set(A), _).
read_exp(\ \ A, Anew, Template):-
	bind_temp(Template, [\ \ A, 'Reduce negation of negation'], T1),
	print(T1), nl,
	read_exp(A, Anew, Template).
read_exp(\(A /\ B), Exp, Template):-
	bind_temp(Template, [\(A /\ B), 'Reduce negation of AND'], T1),
	print(T1), nl,
	read_exp((\A) \/ (\B), Exp, Template).
read_exp(\(A \/ B), Exp, Template):-
	bind_temp(Template, [\(A \/ B), 'Reduce negaion of OR'], T1),
	print(T1), nl,
       	read_exp((\A) /\ (\B), Exp, Template).
read_exp(A \/ B, Exp, Template):-
	bind_temp(Template, [(_ /\ B), _], T1),
	read_exp(A, Anew, T1),
	bind_temp(Template, [(A /\ _), _], T2),
	read_exp(B, Bnew, T2),
	simplify(Anew \/ Bnew, Exp, Template).
read_exp(A /\ B, Exp, Template):-
	bind_temp(Template, [(_ /\ B), _], T1),
	read_exp(A, Anew, T1),
	bind_temp(Template, [(A /\ _), _], T2),
	read_exp(B, Bnew, T2),
	simplify(Anew /\ Bnew, Exp, Template).
read_exp(A delta B, C, Template):-
	bind_temp(Template, [(_ delta B), _], T1),
	read_exp(A, Anew, T1),
	bind_temp(Template, [(A delta _), _], T2),
	read_exp(B, Bnew, T2),
	read_exp((Anew /\ \Bnew) \/ (Bnew /\ \Anew), C, Template).

bind_temp(Template, Vars, T):-
	copy_term(Template, T),
	term_variables(T, Vars).

simplify(set(A), set(A), _).
simplify(\set(A), \set(A), _).

simplify(A /\ \A, false, Template):-
	bind_temp(Template, [A /\ \A, ''], T1),
	print(T1), nl,
	bind_temp(Template, [false, 'Something and its negation is always false'], T2),
	print(T2), nl.
simplify(\A /\ A, false, Template):-
	bind_temp(Template, [\A /\ A, ''], T1),
	print(T1), nl,
	bind_temp(Template, [false, 'Something and its negation is always false'], T2),
	print(T2), nl.
simplify(A /\ false, false, Template):-
	bind_temp(Template, [A /\ false, ''], T1),
	print(T1), nl,
	bind_temp(Template, [false, 'Something and false is always false'], T2),
	print(T2), nl.
simplify(false /\ A , false, Template):-
	bind_temp(Template, [false /\ A, ''], T1),
	print(T1), nl,
	bind_temp(Template, [false, 'Something and false is always false'], T2),
	print(T2), nl.
simplify(A \/ false, Anew, Template):-
	bind_temp(Template, [A \/ false, 'Reduce something or false'], T1),
	print(T1), nl,
	read_exp(A, Anew, Template).
simplify(false \/ A, Anew, Template):-
	bind_temp(Template, [false \/ A, 'Reduce something or false'], T1),
	print(T1), nl,
	read_exp(A, Anew, Template).
simplify(A /\ (B \/ C), Exp, Template):-
	bind_temp(Template, [A /\ (B \/ C), 'Distributivity'], T1),
	print(T1), nl,
	read_exp((A /\ B) \/ (A /\ C), Exp, Template).
simplify((B \/ C) /\ A , Exp, Template):-
	bind_temp(Template, [(B \/ C) /\ A, 'Distributivity'], T1),
	print(T1), nl,
	read_exp((A /\ B) \/ (A /\ C), Exp, Template).
simplify(A,A, _).



normalize_ops(Ops, NewOps):-
	op_tree_to_list(Op, Ops, List),
	sort(List, Sorted),
	%reverse(Sorted, RevList),
	list_to_ops(Op, Sorted, NewOps).
op_tree_to_list(_, set(A), [set(A)]).
op_tree_to_list(_, \set(A), [\set(A)]).
op_tree_to_list(Op, Exp, List):-
	Exp =.. [Op, A, B],
	op_tree_to_list(Op, A, L1),
	op_tree_to_list(Op, B, L2),
	append(L1, L2, List).
op_tree_to_list(Op, Exp, [NewExp]):-
	Exp =.. [NewOp, _,_],
	Op \= NewOp,
	normalize_ops(Exp, NewExp).
list_to_ops(NewOp, [A,B], Exp):-
	Exp =.. [NewOp, A, B].
list_to_ops(NewOp, [A|Rest], NewExp):-
	list_to_ops(NewOp, Rest, Exp),
	NewExp =.. [NewOp, Exp, A].

sort_pair(Pair, NewPair):-
	Pair =.. [Op, A, B],
	(compare(<, A, B) ->
	   NewPair =.. [Op, A, B]
	 ; NewPair =.. [Op, B, A]).

portray(main_set(A)):-
	format('{}= lbrace x mline ~p rbrace newline\n', [A]).
portray(main_set(A, Proof)):-
	format('{}= lbrace x mline ~p rbrace newline "~w:" newline\n', [A, Proof]).
portray(A delta B):-
	format('(~p %DELTA ~p)', [A,B]).
portray(\set(A)):-
	format('(x notin ~p)', [A]).
portray(set(A)):-
	format('(x in ~p)', [A]).
portray(A /\ B):-
	format('(~p and ~p)', [A, B]).
portray(A \/ B):-
	format('(~p or ~p)', [A, B]).
portray(\A):-
	format('neg (~p)', [A]).