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

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

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

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

% domain elements

% points
dom(a1). dom(a2). dom(a3).
dom(b1). dom(b2). dom(b3).
dom(s).
dom(p1). dom(p2). dom(p3).

% lines
dom(a1a2). dom(a2a3). dom(a3a1).
dom(b1b2). dom(b2b3). dom(b3b1).
dom(s1). dom(s2). dom(s3).

% goal
[perpectivity_line,L]  := i(p3,L),i(p1,L),i(p2,L) => answer((i(p3,L),i(p1,L),i(p2,L))).
[triangle_a_in_b] := i(a1,b2b3),i(a2,b3b1),i(a3,b1b2) => answer((i(a1,b2b3),i(a2,b3b1),i(a3,b1b2))).
[triangle_b_in_a] := i(b1,a2a3),i(b2,a3a1),i(b3,a1a2) => answer((i(b1,a2a3),i(b2,a3a1),i(b3,a1a2))).
[] := answer(_) => goal.

% Desargues' assumptions:= points, lines and incidences

% triangle a1a2a3
[ia1a2] := true => i(a1,a1a2).
[ia2a1] := true => i(a2,a1a2).
[ia2a3] := true => i(a2,a2a3).
[ia3a2] := true => i(a3,a2a3).
[ia3a1] := true => i(a3,a3a1).
[ia1a3] := true => i(a1,a3a1).

% triangle b1b2b3
[ib1b2] := true => i(b1,b1b2).
[ib2b1] := true => i(b2,b1b2).
[ib2b3] := true => i(b2,b2b3).
[ib3b2] := true => i(b3,b2b3).
[ib3b1] := true => i(b3,b3b1).
[ib1b3] := true => i(b1,b3b1).

% lines through perspectivity point s and corresponding vertices
[iss1]  := true => i(s,s1).
[iss2]  := true => i(s,s2).
[iss3]  := true => i(s,s3).
[ia1s1] := true => i(a1,s1).
[ia2s2] := true => i(a2,s2).
[ia3s3] := true => i(a3,s3).
[ib1s1] := true => i(b1,s1).
[ib2s2] := true => i(b2,s2).
[ib3s3] := true => i(b3,s3).

% meet a1a2,b1b2 in point p3
[ip3a] := true => i(p3,a1a2).
[ip3b] := true => i(p3,b1b2).

% meet a2a3,b2b3 in point p1
[ip1a] := true => i(p1,a2a3).
[ip1b] := true => i(p1,b2b3).

% meet a3a1,b3b1 in point p2
[ip2a] := true => i(p2,a3a1).
[ip2b] := true => i(p2,b3b1).

% distinct points ai
[diff_a1_a2] := e(a1,a2) => false.
[diff_a2_a3] := e(a2,a3) => false.
[diff_a3_a1] := e(a3,a1) => false.

% distinct points bi
[diff_b1_b2] := e(b1,b2) => false.
[diff_b2_b3] := e(b2,b3) => false.
[diff_b3_b1] := e(b3,b1) => false.

% no corresponding edges in common
[not12] := e(a1a2,b1b2) => false. 
[not23] := e(a2a3,b2b3) => false. 
[not31] := e(a3a1,b3b1) => false.

% equality
[ref,X]     := dom(X) => e(X,X).     
[sym,X,Y]   := e(X,Y) => e(Y,X).
[tra,X,Y,Z] := e(X,Y),e(Y,Z) => e(X,Z).

% congruence
[conp,P,Q,L] := e(P,Q),i(Q,L) => i(P,L).
[conl,P,L,M] := i(P,L),e(L,M) => i(P,M).

% sorted incidence
[sortp,P,L] := i(P,L) => p(P).
[sortl,P,L] := i(P,L) => l(L).

[gap1] := true => i(a1,b2b3);i(b3,a1a2).
[gap2] := true => i(a2,b3b1);i(b1,a2a3).
[gap3] := true => i(a3,b1b2);i(b2,a3a1).

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

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