6
\$\begingroup\$

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)

\$\endgroup\$
0

1 Answer 1

2
\$\begingroup\$

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))
\$\endgroup\$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.