% original version at http://www.ii.uib.no/~bezem/GL/p2p1.in
% Pappus2 => Pappus1 in projective planes

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(ep/2).
:- dynamic(el/2).
:- dynamic(pl/2).
:- dynamic(col/4).
:- dynamic(dom/1).
:- dynamic(answer/1).

flag(keywords).
flag(quiet).
flag(quick).

%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
[assump1] := true => col(a,b,c,l),col(d,e,f,m). %a,b,c on l, etc.
[assump2] := true => col(b,f,g,n),col(c,e,g,o).
[assump3] := true => col(b,d,h,p),col(a,e,h,q).
[assump4] := true => col(c,d,i,r),col(a,f,i,s).

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

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

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

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

%congruence
[pcon,P,Q,L] := ep(P,Q),pl(Q,L) => pl(P,L).
[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 ...
[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
[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
[line,P,Q] := ep(P,P),ep(Q,Q) => dom(L),pl(P,L),pl(Q,L).

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