Trung tâm cá nhân
sách gpt4 ai đã đi

proof - 重写简单定理证明

In lại 作者：行者123 更新时间：2023-12-01 23:22:04 29 4
mua khóa gpt4 Nike

我写了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.

1 Câu trả lời

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

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

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

现在我们可以证明错误:

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

喜剧结束了!

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

关于proof - 重写简单定理证明，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/44929029/

29 4 0
Bài viết được đề xuất: javafx - 如何删除 JavaFX 按钮(选择时)的默认边框发光？
Bài viết được đề xuất: java - 将字符串数组返回给其他类(包括继承)并打印
Bài viết được đề xuất: ruby-on-rails - 未捕获的未知 cloud_name
Bài viết được đề xuất: webrtc - 取消发布后发布失败
行者123
Hồ sơ cá nhân

Tôi là một lập trình viên xuất sắc, rất giỏi!

Nhận phiếu giảm giá Didi Taxi miễn phí
Mã giảm giá Didi Taxi
Các bài viết nóng hổi trên toàn bộ trang web
Giấy chứng nhận ICP Bắc Kinh số 000000
Hợp tác quảng cáo: 1813099741@qq.com 6ren.com