什么是命题不等于？(What is the equivalent of propositional not equals?)

什么是命题不等于？(What is the equivalent of propositional not equals?)

我最近问了一个问题并用rewrite策略的一些应用解决了这个问题。 然后我决定回顾我关于代码审查的其他一个问题 ，要求审查我试图正式化希尔伯特（基于欧几里德）几何。

从第一个问题开始，我了解到命题平等与布尔平等和命题平等之间存在区别。 回顾一下我为希尔伯特飞机写的一些公理，我广泛使用了布尔相等。 虽然我不是100％肯定，但根据我收到的答案，我怀疑我不想使用布尔相等。

例如，采取这个公理：

-- 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))

我尝试重写它不涉及= 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)))

总而言之，我从codereview上的问题中取出了代码，删除了==和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))

这给出了错误：

| 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

所以，似乎/=仅适用于布尔值。 我一直无法找到“命题” /=喜欢：

data (/=) : a -> b -> Type where

命题不等于存在吗？ 或者我错了想要从布尔变为命题平等？

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?

最满意答案

等价于布尔a /= b的命题将是a = b -> Void 。 Void是一种没有构造函数的类型。 因此，每当你有一个contra : Void ，出现问题。 所以a = b -> Void应理解为：如果你有一个a = b ，就会产生矛盾。 通常写为Not (a = b) ，这只是一个简写（ Not a = a -> Void ）。

你改变命题平等是正确的。 您甚至可以更改布尔属性，例如contains : line -> point -> Bool to Contains : line -> point -> Type 。 随后contains lp = True到Contains lp ，并contains lp = False到Not (Contains lp) 。

这是一个布尔盲的情况，即使用prf : contains lp = True ，我们唯一知道的是contains lp是True （并且编译器需要查看contains来猜测它为什么是True ）。 另一方面，使用prf : Contains lp你有一个构造证明prf 为什么命题Contains lp成立。

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.