有没有办法在没有模型的情况下证明 Idris 中的东西？

Question

我一直在尝试在希尔伯特平面的几何中实现入射公理。并提出了以下公理：

interface (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
  intersection_def : (contains l a = True) -> (contains m a = True) -> (intersects_at l m a = True)

  -- For any two distinct points there is a line that contains them.
  line_contains_two_points : (a,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 : contains l a = True -> contains l b = True -> contains m a = True -> contains m b = True -> l = m

  -- 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 lines contains at least two points.
  contain_two_pts : (l : line) -> (a : point ** b : point ** (contains l a = True, contains l b = True))

我想证明一条线最多与另一条线相交一次。所以我想出了以下声明：

intersect_at_most_one_point : (l, m : line) -> (a : point) -> (intersects_at l m a = True) -> (intersects_at l m b = True) -> a = b

上面写着：

Given two lines, if they intersect at two points a and b then it must be that a = b.

但是我收到错误：

When checking type of Main.intersect_at_most_one_point:
When checking argument x to type constructor =:
        Can't find implementation for Plane line point

所以我怀疑这意味着它想要某种 data 值，我可以证明它满足关联几何的想法。我在数学上对此进行解释，因为我需要一个系统模型。问题是有很多 "geometries" 满足这些截然不同的公理。

是否可以在不需要任何显式 data 的情况下推导出关于接口的定理？

Answer 1

您需要将 Plane 约束添加到 intersect_at_most_one_point 的类型签名中：

intersect_at_most_one_point : Plane line point => 
  (l, m : line) -> (a : point) -> 
  (intersects_at l m a = True) -> (intersects_at l m b = True) -> 
  a = b

有没有办法在没有模型的情况下证明 Idris 中的东西？

Is there a way to prove stuff in Idris without a model?

idris