代码之家 › 专栏 › 技术社区 › Schroedinger

在agda中研究peano公理并遇到一点问题

agda axiom haskell

3

Schroedinger · 技术社区 · 15 年前

PA6 : â{m n} -> m â¡ n -> n â¡ m

是我试图解决和支持的公理,我尝试使用cong(来自核心库),但是cong构造函数有问题

PA6 = cong

我不知道,我知道对于聪聪,我必须提供一个平等和类型的refl,但我不知道我应该提供什么类型。思想?

这是大学里的一个小作业,所以我宁愿有人证明我错过了什么,而不是写一个准确的答案,但我会感谢任何程度的支持。

2 回复 | 直到 14 年前

1

6

glguy 14 年前

你的pa6说 对称的。

这可以在relation.binary.positionalquality模块的标准库中找到。

sym : â {a} {A : Set a} {x y : A} â x â¡ y â y â¡ x
sym refl = refl

(这个问题已经很老了,但我发表这篇文章是为了将来偶然发现它的读者的利益。)

2

3

Schroedinger 15 年前

根据我创建的系统的性质,我必须意识到我有两个等价物,因此需要使用等价方法refl

因此,为了满足我的类型签名,AGDA接受: PA6 refl = refl

希望能帮上忙