用简单的定理证明重写

Question

我在 Idris 中写了group 的定义：

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

Finita la commedia！

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

Answer 2

您的组定义的结构方式如果它是一个接口就可以理解。我已将其重写如下，尽可能保留您原来的变量和函数名称：

%default total

interface Group t where
  Unit: t
  (*): t -> t -> t
  Inv: t -> t

  assoc: (a : t) -> (b : t) -> (c : t) -> ((a*b)*c = a*(b*c))
  neutralL: (x: t) -> (a : t) -> a * Unit = a
  neutralR: (x: t) -> (a : t) -> Unit * a = a
  invUnitL: (x: t) -> (a : t) -> a * (Inv a) = Unit
  invUnitR: (x: t) -> (a : t) -> (Inv a) * a = Unit

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

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

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

is_left_unit : Group t => (x : t) -> Type
is_left_unit x = (y : t) -> x * y = y

only_one_left_unit : Group t => (x : t) -> is_left_unit x -> x = Unit
only_one_left_unit x is_left_unit_x = 
  let x_times_unit_is_unit = is_left_unit_x Unit in
  let x_times_unit_is_x = neutralL Unit x in
    trans (sym x_times_unit_is_x) x_times_unit_is_unit

is_right_unit : Group t => (x : t) -> Type
is_right_unit x = (y : t) -> y * x = y

only_one_right_unit : Group t => (x : t) -> is_right_unit x -> x = Unit
only_one_right_unit x is_right_unit_x = 
  let unit_times_x_is_unit = is_right_unit_x Unit in
  let unit_times_x_is_x = neutralR Unit x in
    trans (sym unit_times_x_is_x) unit_times_x_is_unit

您会注意到t 类型实际上是组类型，而Unit 是一个值而不是具有一个参数的函数。我已经定义了单独的函数 is_left_unit 和 is_right_unit 分别代表左单元或右单元的概念。

为了确保所有这些都有意义，我们希望定义一些实际的具体组，为Unit、* 和Inv 提供实现，另外还为assoc、neutralL、@987654331 提供实现@、invUnitL 和 invUnitR 代表证明义务。