% Pappus2 => Pappus1 in projective planes

name(p2p1_).

:- dynamic ep/2,el/2,pl/2,col/4.
%ep,el = equality for points and lines, resp. 
%pl = point-line incidence (deliberately asymmetric!)
%col = point-point-point-line collinearity

%points 
dom(a). dom(b). dom(c). dom(d). dom(e). dom(f). dom(g). dom(h). dom(i).
%lines 
dom(l). dom(m). dom(n). dom(o). dom(p). dom(q). dom(r). dom(s).

%Pappus1 assumptions, same as in Pappus2
_ axiom assump1 : (true => col(a,b,c,l),col(d,e,f,m)). %a,b,c on l, etc.
_ axiom assump2 : (true => col(b,f,g,n),col(c,e,g,o)).
_ axiom assump3 : (true => col(b,d,h,p),col(a,e,h,q)).
_ axiom assump4 : (true => col(c,d,i,r),col(a,f,i,s)).

%Pappus1 conclusions
_ axiom goalam   : (pl(a,m) => goal).
_ axiom goalbm   : (pl(b,m) => goal).
_ axiom goalcm   : (pl(c,m) => goal).
_ axiom goaldl   : (pl(d,l) => goal).
_ axiom goalel   : (pl(e,l) => goal).
_ axiom goalfl   : (pl(f,l) => goal).
_ axiom goal4(U) : (pl(g,U),pl(h,U),pl(i,U) => goal).
%not using col(g,h,i,U) for efficiency reasons ...

%collinearity, we avoid the symmetries inflicted by col_intro 
_ axiom col_elim1(P,Q,R,L) : (col(P,Q,R,L) => pl(P,L)).
_ axiom col_elim2(P,Q,R,L) : (col(P,Q,R,L) => pl(Q,L)).
_ axiom col_elim3(P,Q,R,L) : (col(P,Q,R,L) => pl(R,L)).
% axiom col_intro(P,Q,R,L) : (pl(P,L),pl(Q,L),pl(R,L) => col(P,Q,R,L)).

%equality for points
_ axiom pref(P,L)   :  (pl(P,L) => ep(P,P)).     %a bit special indeed!
_ axiom psym(P,Q)   :  (ep(P,Q) => ep(Q,P)).
_ axiom ptra(P,Q,R) :  (ep(P,Q),ep(Q,R) => ep(P,R)).

%equality for lines
_ axiom lref(P,L)   :  (pl(P,L) => el(L,L)).     %a bit special indeed!
_ axiom lsym(L,M)   :  (el(L,M) => el(M,L)).
_ axiom ltra(L,M,N) :  (el(L,M),el(M,N) => el(L,N)).

%congruence
_ axiom pcon(P,Q,L) :  (ep(P,Q),pl(Q,L) => pl(P,L)).
_ axiom lcon(P,L,M) :  (pl(P,L),el(L,M) => pl(P,M)).


%Pappus2: A,B,C on L, D,E,F on M, N/=O, P/=Q, R/=S, then ...
_ axiom papp1(A,B,C,D,E,F,G,H,I,L,M,N,O,P,Q,R,S) : (
col(A,B,C,L),col(D,E,F,M),                         % ABC on L, DEF on M
col(B,F,G,N),col(C,E,G,O),                            %cross BF,CE in G 
col(B,D,H,P),col(A,E,H,Q),                            %cross BD,AE in H
col(C,D,I,R),col(A,F,I,S)                             %cross CD,AF in I
=> dom(T),col(G,H,I,T);                               % G,H,I on line T 
   el(N,O);el(P,Q);el(R,S)).  % exceptions

 
%projective uniqueness
_ axiom unique(L,M,P,Q):(pl(P,L),pl(P,M),pl(Q,L),pl(Q,M) => ep(P,Q); el(L,M)).

%last to avoid infinite paths: projective incidence axioms
_ axiom line(P,Q) : (ep(P,P),ep(Q,Q) => dom(L),pl(P,L),pl(Q,L)).

%not used in this proof
_ axiom point(P,L,M) : (el(M,M),el(L,L) => dom(P),pl(P,L),pl(P,M)).


