# Proof that two lines intersect each other at precisely one point in Idris

I recently attempted to prove that given two lines, they intersect at one and only one point in Idris. Here is what I came up with:

interface (Eq line, Eq point) => Plane line point where
-- Abstract notion for saying three points lie on the same line.
colinear : point -> point -> point -> Bool
coplanar : point -> point -> point -> Bool
contains : line -> point -> Bool

-- Intersection between two lines
intersects_at : line -> line -> point -> Bool

-- If two lines l and m contain a point a, they intersect at that point.
intersection_criterion : (l : line) ->
(m : line) ->
(a : point) ->
(contains l a = True) ->
(contains m a = True) ->
(intersects_at l m a = True)

-- If l and m intersect at a point a, then they both contain a.
intersection_result : (l : line) ->
(m : line) ->
(a : point) ->
(intersects_at l m a = True) ->
(contains l a = True, contains m a = True)

-- For any two distinct points there is a line that contains them.
line_contains_two_points : (a :point) ->
(b : point) ->
(a /= b) = True ->
(l : line ** (contains l a = True, contains l b = True ))

-- If two points are contained by l and m then l = m
two_pts_define_line : (l : line) ->
(m : line) ->
(a : point) ->
(b : point) ->
((a /= b) = True) ->
contains l a = True ->
contains l b = True ->
contains m a = True ->
contains m b = True ->
((l == m) = True)

same_line_same_pts : (l : line) ->
(m : line) ->
(a : point) ->
(b : point) ->
((l /= m) = True) ->
contains l a = True ->
contains l b = True ->
contains m a = True ->
contains m b = True ->
((a == b) = True)

-- There exists 3 non-colinear points.
three_non_colinear_pts : (a : point ** b : point ** c : point **
(colinear a b c = False,
(a /= b) = True,
(b /= c) = True,
(a /= c) = True))

-- Any line contains at least two points.
contain_two_pts : (l : line) ->
(a : point ** b : point **
(contains l a = True, contains l b = True))

-- If two lines intersect at a point and they are not identical, that is the o-
-- nly point they intersect at.
intersect_at_most_one_point : Plane line point =>
(l : line) -> (m : line) -> (a : point) -> (b : point) ->
((l /= m) = True) ->
(intersects_at l m a = True) ->
(intersects_at l m b = True) ->
((a == b) = True)

intersect_at_most_one_point l m a b l_not_m int_at_a int_at_b =
same_line_same_pts
l
m
a
b
l_not_m
(fst (intersection_result l m a int_at_a))
(fst (intersection_result l m b int_at_b))
(snd (intersection_result l m a int_at_a))
(snd (intersection_result l m b int_at_b))


My main concerns is that I have an "inefficient" (possibly incorrect?) formulation of the axioms. The code runs and compiles, but it feels like for instance, somehow, intersection_criterion and intersection_result could be somehow made into one axiom. Nevertheless, any advice is appreciated.

(This is also on Github here in the file hilbert.idr)

It still may be far from perfect, but I asked a question on Stackoverflow related to this, and received an excellent answer from xash.

I have attempted to cure my Boolean blindness. If I understand correctly, the operator == asks the question "Is the left hand side equal to the right hand side?" Instead, I want to say: "I have a proof that this holds."

To fix this, I changed a lot of my functions like colinear to more closely match the (=) signature:

colinear : point -> point -> point -> Bool


becomes:

Colinear : point -> point -> point -> Type


Also, I removed a /= b and instead replaced it with Not (a = b).

Here was the resulting code:

interface Plane line point where
-- Abstract notion for saying three points lie on the same line.
Colinear : point -> point -> point -> Type
Coplanar : point -> point -> point -> Type
Contains : line -> point -> Type

-- Intersection between two lines
IntersectsAt : line -> line -> point -> Type

-- If two lines l and m contain a point a, they intersect at that point.
intersection_criterion : (l : line) ->
(m : line) ->
(a : point) ->
Contains l a ->
Contains m a ->
IntersectsAt l m a

-- If l and m intersect at a point a, then they both contain a.
intersection_result : (l : line) ->
(m : line) ->
(a : point) ->
IntersectsAt l m a ->
(Contains l a, Contains m a)

-- For any two distinct points there is a line that contains them.
line_contains_two_points : (a : point) ->
(b : point) ->
Not (a = b) ->
(l : line ** (Contains l a, Contains l b))

-- If two points are contained by l and m then l = m
two_pts_define_line : (l : line) ->
(m : line) ->
(a : point) ->
(b : point) ->
Not (a = b) ->
Contains l a ->
Contains l b ->
Contains m a ->
Contains m b ->
(l = m)

same_line_same_pts : (l : line) ->
(m : line) ->
(a : point) ->
(b : point) ->
Not (l = m) ->
Contains l a ->
Contains l b ->
Contains m a ->
Contains m b ->
(a = b)

-- There exists 3 non-colinear points.
three_non_colinear_pts : (a : point ** b : point ** c : point **
(colinear a b c = False,
Not (a = b),
Not (b = c),
Not (a = c)))

-- Any line contains at least two points.
contain_two_pts : (l : line) ->
(a : point ** b : point **
(Contains l a, Contains l b))

-- If two lines intersect at a point and they are not identical, that is the o-
-- nly point they intersect at.
intersect_at_most_one_point : Plane line point =>
(l : line) -> (m : line) -> (a : point) -> (b : point) ->
Not (l = m) ->
IntersectsAt l m a ->
IntersectsAt l m b ->
(a = b)

intersect_at_most_one_point l m a b l_not_m int_at_a int_at_b =
same_line_same_pts
l
m
a
b
l_not_m
(fst (intersection_result l m a int_at_a))
(fst (intersection_result l m b int_at_b))
(snd (intersection_result l m a int_at_a))
(snd (intersection_result l m b int_at_b))