I somewhat recently asked a question and resolved the issue with a some applications of the rewrite tactic. I then decided to look back at one of my other questions on code review asking for a review of my attempt to formalize Hilbert's (based on Euclid's) geometry.
From the first question, I learned there is a distinction between propositional equality and boolean equality and propositional equality. Looking back at the some of the axioms I wrote for the Hilbert plane, I utilized boolean equality extensively. Although I am not 100% sure, in light of the answer I received, I suspect that I don't want to use boolean equality.
For instance, take this axiom:
-- 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))
I tried rewriting it to not involve the = True:
-- There exists 3 non-colinear points.
three_non_colinear_pts : (a : point ** b : point ** c : point **
(colinear a b c = False,
(a /= b),
(b /= c),
(a /= c)))
All in all I took the code from my question on codereview removed the == and removed = True:
interface 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) ->
(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) ->
contains l a = True ->
contains l b = True ->
contains m a = True ->
contains m b = True ->
(l = m)
same_line_same_pts : (l : line) ->
(m : line) ->
(a : point) ->
(b : point) ->
(l /= m) ->
contains l a = True ->
contains l b = True ->
contains m a = True ->
contains m b = True ->
(a = b)
-- There exists 3 non-colinear points.
three_non_colinear_pts : (a : point ** b : point ** c : point **
(colinear a b c = False,
(a /= b),
(b /= c),
(a /= c)))
-- 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) ->
(intersects_at l m a = True) ->
(intersects_at l m b = True) ->
(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))
This gives the error:
|
1 | interface Plane line point where
| ~~~~~~~~~~~~~~~~
When checking type of Main.line_contains_two_points:
Type mismatch between
Bool (Type of _ /= _)
and
Type (Expected type)
/home/dair/scratch/hilbert.idr:68:29:
|
68 | intersect_at_most_one_point : Plane line point =>
| ^
When checking type of Main.intersect_at_most_one_point:
No such variable Plane
So, it seems that /= works only for boolean. I have been unable to find a "propositional" /= like:
data (/=) : a -> b -> Type where
Does a propositional not equals exist? Or am I wrong about wanting to change from boolean to propositional equality?
The propositional equivalent to the boolean a /= b would be a = b -> Void. Void is a type with no constructors. So whenever you have a contra : Void, something has gone wrong. So a = b -> Void is to understand as: if you have an a = b, there is a contradiction. Usually written as Not (a = b), which is just a shorthand (Not a = a -> Void).
You're right to change to propositional equality. You might even change your boolean properties like contains : line -> point -> Bool to Contains : line -> point -> Type. Subsequently contains l p = True to Contains l p, and contains l p = False to Not (Contains l p).
That's a case of boolean blindness, i.e. with prf : contains l p = True, the only thing we know is that contains l p is True (and the compiler would need to take a look at contains to guess why it is True). On the other hand, with prf : Contains l p you have a constructed proof prf why the proposition Contains l p holds.