重写简单的定理证明

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)

喜剧结束！

您真正想要的是 record 或类型类，例如参见contrib/Control/Algebra.idr and contrib/Interfaces/Verified.idr. In addition, Agda versions are syntactically pretty close to Idris (agda-stdlib/src/Algebra.agda and probably the 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 提供实现，并另外为 [= 提供实现18=、neutralL、neutralR、invUnitL和invUnitR代表证明义务。

重写简单的定理证明

Rewriting in simple theorem proof

formal-verification

proof

theorem-proving

dependent-type

idris