% original version at http://www.ii.uib.no/~bezem/GL/pd_hes.in

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

:- dynamic(p/2).
:- dynamic(l/2).
:- dynamic(i/2).
:- dynamic(answer/1).

flag(keywords).
flag(quick).

[goal_normal,U] := i(bc,U),i(ac,U),i(ab,U) => answer((i(bc,U),i(ac,U),i(ab,U))).
[hessenberg_gap1] := i(a1,b2c2) => answer(i(a1,b2c2)).
[hessenberg_gap2] := i(b2,a1c1) => answer(i(b2,a1c1)).
[] := answer(_) => goal.

%Desargues assumptions: points, lines and incidences
%triangles a1b1c1 and a2b2c2
[ia1b1] := true => i(a1,a1b1).
[ib1a1] := true => i(b1,a1b1).
[ia2b2] := true => i(a2,a2b2).
[ib2a2] := true => i(b2,a2b2).
[ia1c1] := true => i(a1,a1c1).
[ic1a1] := true => i(c1,a1c1).
[ia2c2] := true => i(a2,a2c2).
[ic2a2] := true => i(c2,a2c2).
[ic1b1] := true => i(c1,b1c1).
[ib1c1] := true => i(b1,b1c1).
[ic2b2] := true => i(c2,b2c2).
[ib2c2] := true => i(b2,b2c2).

% lines through perspectivity point o and corresponding vertices
[iooa]  := true => i(o,oa).
[ioob]  := true => i(o,ob).
[iooc]  := true => i(o,oc).
[ia1oa] := true => i(a1,oa).
[ia2oa] := true => i(a2,oa).
[ib1ob] := true => i(b1,ob).
[ib2ob] := true => i(b2,ob).
[ic1oc] := true => i(c1,oc).
[ic2oc] := true => i(c2,oc).

% cross b1c1,b2c2 in point bc
[ibc1] := true => i(bc,b1c1).
[ibc2] := true => i(bc,b2c2).

% cross a1c1, a2c2 in point ac
[iac1] := true => i(ac,a1c1).
[iac2] := true => i(ac,a2c2).

% cross a1b1,a2b2 in point ab
[iab1] := true => i(ab,a1b1).
[iab2] := true => i(ab,a2b2).
%to prove: points ab,bc,ac on (perspectivity) line 

%triangle1 non-degenerate
[triangle1,L] := i(a1,L),i(b1,L),i(c1,L) => false.

%triangle2 non-degenerate
[triangle2,L] := i(a2,L),i(b2,L),i(c2,L) => false.

%no corresponding vertices in common
[notaa] := p(a2,a1) => false. 
[notbb] := p(b2,b1) => false. 
[notcc] := p(c2,c1) => false.

%no corresponding edges in common
[notbc] := l(b1c1,b2c2) => false. 
[notac] := l(a1c1,a2c2) => false. 
[notab] := l(a1b1,a2b2) => false.

%pequality for points
[pref,P,L]   := i(P,L) => p(P,P).     %sorted incidence
[psym,P,Q]   := p(P,Q) => p(Q,P).
[ptra,P,Q,R] := p(P,Q),p(Q,R) => p(P,R).

%pequality for lines
[lref,P,L]   := i(P,L) => l(L,L).     %sorted incidence
[lsym,L,M]   := l(L,M) => l(M,L).
[ltra,L,M,N] := l(L,M),l(M,N) => l(L,N).

%congruence
[pcon,P,Q,L] := p(P,Q),i(Q,L) => i(P,L).
[lcon,P,L,M] := i(P,L),l(L,M) => i(P,M).

%projective uniqueness
[unique,P,Q,L,M] := i(P,L),i(P,M),i(Q,L),i(Q,M) => p(P,Q);l(L,M).

%projective geometry
[line,P,Q] := p(P,P),p(Q,Q) => i(P,L),i(Q,L).
[point,L,M] := l(L,L),l(M,M) => i(P,L),i(P,M).

%Pappus: A,B,C on L, D,E,F on M, then ... or N=O;P=Q;R=S
[papp,A,B,C,D,E,F,G,H,I,L,M,N,O,P,Q,R,S] :=
i(A,L),i(B,L),i(C,L),i(D,M),i(E,M),i(F,M),          % ABC on L, DEF on M
i(B,N),i(F,N),i(G,N),i(C,O),i(E,O),i(G,O),          % cross BF,CE in G
i(B,P),i(D,P),i(H,P),i(A,Q),i(E,Q),i(H,Q),          % cross BD,AE in H
i(C,R),i(D,R),i(I,R),i(A,S),i(F,S),i(I,S)           % cross CD,AF in I
=> l(N,O);l(P,Q);l(R,S);                            % degenerations         
   l(T,T),i(G,T),i(H,T),i(I,T).                     % G,H,I on line T

                       
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%proof script%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

'e:tactic'(('log:implies'((p(a1,a1), p(b2,b2)),(i(a1,_L0), i(b2,_L0)))),[[],[
	('log:implies'((l(_L0,_L0), l(oc,oc)),(i(_P1,_L0), i(_P1,oc)))),
	('log:implies'((p(_P1,_P1), p(ac,ac)),(i(_P1,_L2), i(ac,_L2)))),
	('log:implies'((l(_L2,_L2), l(a2b2,a2b2)),(i(_P3,_L2), i(_P3,a2b2)))),
	('log:implies'((p(_P3,_P3), p(o,o)),(i(_P3,_L4), i(o,_L4)))),
	('log:implies'((l(_L4,_L4), l(a1c1,a1c1)),(i(_P5,_L4), i(_P5,a1c1)))),
	('log:implies'((i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(b2,_), i(_,_), i(_,_), i(b2,_), i(_,_), i(_,_), i(c2,_), i(_,_), i(_,_), i(c2,_), i(_,_), i(_,_), i(_P5,_), i(_,_), i(_,_), i(_P5,_)),(l(_,_); l(_,_); l(_,_); l(_,_), i(b2,_), i(c2,_), i(_P5,_)))),
	('log:implies'((l(_L4,_L4), l(a1b1,a1b1)),(i(_P6,_L4), i(_P6,a1b1)))),
	('log:implies'((i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_P1,_), i(_,_), i(_,_), i(_P1,_), i(_,_), i(_,_), i(_P6,_), i(_,_), i(_,_), i(_P6,_), i(_,_), i(_,_), i(bc,_), i(_,_), i(_,_), i(bc,_)),(l(_,_); l(_,_); l(_,_); l(_,_), i(_P1,_), i(_P6,_), i(bc,_)))),
	('log:implies'((i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(ab,_), i(_,_), i(_,_), i(ab,_), i(_,_), i(_,_), i(bc,_), i(_,_), i(_,_), i(bc,_), i(_,_), i(_,_), i(ac,_), i(_,_), i(_,_), i(ac,_)),(l(_,_); l(_,_); l(_,_); l(_,_), i(ab,_), i(bc,_), i(ac,_))))]]).
'e:tactic'(('log:implies'((p(_P,_P), p(_Q,_Q)),(i(_P,_L), i(_Q,_L)))),
	[[('log:implies'((p(_P,_P), p(_Q,_Q)),(i(_P,_L), i(_Q,_L))))|_T],_T]).
'e:tactic'(('log:implies'((l(_L,_L), l(_M,_M)),(i(_P,_L), i(_P,_M)))),
	[[('log:implies'((l(_L,_L), l(_M,_M)),(i(_P,_L), i(_P,_M))))|_T],_T]).
'e:tactic'(('log:implies'((i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_G,_), i(_,_), i(_,_), i(_G,_), i(_,_), i(_,_), i(_H,_), i(_,_), i(_,_), i(_H,_), i(_,_), i(_,_), i(_I,_), i(_,_), i(_,_), i(_I,_)),(l(_,_); l(_,_); l(_,_); l(_,_), i(_G,_), i(_H,_), i(_I,_)))),
	[[('log:implies'((i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_,_), i(_G,_), i(_,_), i(_,_), i(_G,_), i(_,_), i(_,_), i(_H,_), i(_,_), i(_,_), i(_H,_), i(_,_), i(_,_), i(_I,_), i(_,_), i(_,_), i(_I,_)),(l(_,_); l(_,_); l(_,_); l(_,_), i(_G,_), i(_H,_), i(_I,_))))|_T],_T]).