モデルなしで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)) 

私は線が他の線と多くても1度交差することを示したいと思います。

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値の並べ替えは、入射ジオメトリの考え方を満たしています。私はシステムのモデルが必要なので、これを数学的に解釈します。問題は、大きく異なるこれらの公理を満たす多くの「幾何学」があることです。

明示的にdataを使用する必要なしに、インターフェイスに関する定理を導き出すことは可能ですか？

Answer 1

あなたはintersect_at_most_one_pointのあなたのタイプの署名にPlane制約を追加する必要があります。

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