/* 

A little fragment of set theory to execise reduction with equivalences.

*/

% set theory

% equality on binary relations
eq(set(U),S,T) == 
  all(X,contains(U,S,X) <=> contains(U,T,X)).


% equality in general
% eq(U,S,T) == (S=T).

pair((U,V),X,Y)=pair((U,V),X1,Y1) => (X=X1) and (Y=Y1).

/*
% cartesian product of relations
contains(prod(U,V),product((U,V),S,T),pair((U,V),A,B))
   == (contains(U,S,A) and contains(V,T,B)).

*/

% composition
contains(prod(U,W),comp((U,V,W),S,T),pair((U,W),X,Y)) 
  == exists(Z,contains(prod(U,V),S,pair((U,V),X,Z)) 
          and contains(prod(V,W),T,pair((V,W),Z,Y))).

% Boolean operations
%contains(union(S,T),X) == (contains(S,X) or contains(T,X)).
%contains(intersection(S,T),X) == (contains(S,X) and contains(T,X)).


% binary relation R subseteq D x C
rel(prod(U,V),R,D,C) 
  == all(P,(contains(prod(U,V),R,P) 
               => exists(X,exists(Y,(P=pair((U,V),X,Y)) and contains(U,D,X) and contains(V,C,Y))))).

% the image of a relation F
%contains(U,image(prod(V,U),F),Y) == exists(X,contains(prod(V,U),F,pair((V,U),X,Y))).

% the image of F on S
% contains(image(F,S),Y) == exists(X,contains(S,X) and contains(F,(X,Y))).


% the identity
%contains(prod(U,U),id(U,T),pair((U,U),X,Y)) == ((X=Y) and contains(U,T,X)).

% total relations
total(prod(U,V),F,D)  
  == all(X,contains(U,D,X) => exists(Y,contains(prod(U,V),F,pair((U,V),X,Y)))).

% unique relations
unique(prod(U,V),F)   
  == all(X,all(Y,all(Z,
       contains(prod(U,V),F,pair((U,V),X,Y)) and contains(prod(U,V),F,pair((U,V),X,Z))
        => (Y=Z)))).

% partial functions
pfunc(prod(U,V),F,D,C) ==  (rel(prod(U,V),F,D,C) and unique(prod(U,V),F)).

% injective relations
injective(prod(U,V),F) == 
   all(X,all(Y,all(Z,contains(prod(U,V),F,pair((U,V),X,Z)) and contains(prod(U,V),F,pair((U,V),Y,Z)) => (X=Y)))).

% functions
func(prod(U,V),F,D,C)  == (pfunc(prod(U,V),F,D,C) and total(prod(U,V),F,D)).



% we prove that the 
% composition of relations with injective functions is injective.

goal
~(
    rel(prod(u,v),p,s,t) and rel(prod(u,v),q,s,t) and
    func(prod(v,w),f,t,b) and injective(prod(v,w),f) =>
                 
  (eq(set(prod(u,w)),comp((u,v,w),p,f),comp((u,v,w),q,f)) => eq(set(prod(u,v)),p,q))
 ).