proof - 重写简单定理证明

Question

我写了group的定义在 idris :

data Group: Type -> Type where
    Unit: (x: t) -> Group t
    (*): Group t -> Group t -> Group t
    Inv: Group t -> Group t
postulate
    assoc: (a : Group t) -> (b : Group t) -> (c : Group t) -> ((a*b)*c = a*(b*c))
postulate
    neutralL: (x: t) -> (a : Group t) -> a * Unit x = a
postulate
    neutralR: (x: t) -> (a : Group t) -> Unit x * a = a
postulate
    invUnitL: (x: t) -> (a : Group t) -> a * (Inv a) = Unit x
postulate
    invUnitR: (x: t) -> (a : Group t) -> (Inv a) * a = Unit x

然后我证明了几个简单的命题:

cong : (a : Group t) -> (b : Group t) -> (c: Group t) -> a = b -> a*c = b*c
cong a b c post = rewrite post in Refl

neutralL1: (x: t) -> (a : Group t) -> a = a * Unit x
neutralL1 x a = rewrite neutralL x a in Refl

neutralR1: (x: t) -> (a : Group t) -> a = Unit x * a
neutralR1 x a = rewrite neutralR x a in Refl

但是，我在证明只有一个单位元素时遇到了问题:

singleUnit : (x: t) -> (y: t) -> (Unit x = Unit y)

我使用一般想法尝试了各种表达式，即 Unit x = (by neutralL1 y (Unit x)) = Unit x * Unit y code> = (by neutralR x (Unit y)) = Unit y，但没有成功:

singleUnit x y = rewrite neutralL1 y (Unit x) in neutralR x (Unit y)
singleUnit x y = rewrite neutralL1 y (Unit x) in rewrite neutralR x (Unit y) in Refl
singleUnit x y = rewrite neutralR x (Unit y) in neutralL1 y (Unit x)
singleUnit x y = rewrite neutralR x (Unit y) in rewrite neutralL1 y (Unit x) in Refl

如何证明这一点？我有一种感觉，这里的问题与复杂表达式的替换有关，例如 Unit x * Unit y。

Answer 1

不幸的是，这个组的定义不起作用。一般来说，引入新公理(假设)时必须非常小心。

例如很容易看出neutralL违反了(不同)数据构造函数的不相交原则，即 Constr1 <data> != Constr2 <data> 。

starAndUnitAreDisjoint : (*) a (Unit x) = a -> Void
starAndUnitAreDisjoint Refl impossible

现在我们可以证明错误:

contradiction : Void
contradiction = starAndUnitAreDisjoint $ neutralL Z (Unit Z)

喜剧结束了!

你真正想要的是 record或类型类，请参见例如contrib/Control/Algebra.idr和 contrib/Interfaces/Verified.idr 。此外，Agda 版本在语法上非常接近 Idris(agda-stdlib/src/Algebra.agda，可能还有 Abstract Algebra in Agda 教程)——您可能想看看它们。