问题标签 [agda]

Agda 2.3.2.1 can't see that the following function terminates:

Agda wiki says that it's OK for the termination checker if the arguments on recursive calls decrease lexicographically. Based on that it seems that this function should also pass. So what am I missing here? Also, is it maybe OK in previous versions of Agda? I've seen similar code on the Internet and no one mentioned termination issues there.

我试图在 agda 中证明 2*3!=5。为此，我将定义一个带有签名 2 * 3 ≡ 5 → ⊥ 的函数。

利用我对乘法的定义

我已经证明

和

但是当我试图证明：

编译器吐出这个关于 x 的错误

对不起，如果这是一个愚蠢的问题。提前致谢。

有几个地方说所有的agda 程序都会终止。但是我可以构造一个这样的函数：

语法高亮似乎不喜欢它，但没有编译错误。

计算stall 0结果的正规形式0。计算结果stall 1会导致 Emacs 挂在看起来很像非终止循环的地方。

这是一个错误吗？或者 Agda 有时可以永远运行吗？还是发生了更微妙的事情？

我从“残酷的 Agda 简介” http://oxij.org/note/BrutalDepTypes/

假设我们想在偶数上定义除以二。我们可以这样做：

N是自然数，偶数是以下“命题”

当你评估表达式 div (succ (succ zero)) 你得到 \p -> succ zero 这就是你所期望的。但是，我不明白的是如何解释 \p. 我也不明白代码 f : \bot -> N f = div (succ zero) 是什么意思。我知道 \bot 对任何 A 都意味着 A ...因此类型是有效的。我想我认为依赖类型将允许我以这样的方式编写 div，即 div (succ zero) 会更明确地失败类型检查。

任何人都可以就如何在 agda 中使用和查看谓词提出建议吗？

我正在学习如何在 Agda 中实现“类型类”。作为一个例子，我正在尝试实现罗马数字，其与 # 的组合将进行类型检查。

1. 我不清楚为什么 Agda 抱怨没有 Join (Roman _ _) (Roman _ _) _ 的实例 - 显然，它无法计算出在那里替换的自然数。

2. 有没有更好的方法来引入没有“构造函数”形式的罗马数字？我有一个构造函数“makeup”，它可能需要是私有的，以确保我只有“可信”的方式来通过 Join 构造其他罗马数字。

   /li>

显然，如果我明确指定隐式，它会起作用 - 所以我相信这不是错误的函数类型。

我最近问了这个问题： 类型中使用的 agda 命题——这是什么意思？ 并收到了关于如何使类型隐式并获得真正的编译时错误的深思熟虑的答案。

但是，我仍然不清楚如何创建具有依赖类型的值。

考虑：

其中N是自然数，偶数是下面的命题。

假设我想写一个函数如下：

我不知道如何以我想要的方式做这样的事情......在我看来，最好的办法是证明（不是（甚至 n））\甚至（成功 n）。我真的不知道如何在 agda 中表达这一点。我能写

由此，我可以做如下事情：

并评估为正常形式......以获得答案。如果我想写 f，我可以这样做

我得到 fn = gn { }1 { }2 其中 ?1 = 偶数 n，而 ?2 = 偶数 (succ n)。然后我可以做 f 5 之类的事情并评估为正常形式。我真的不明白为什么这是有效的......有没有办法告诉agda更多关于f以这种方式定义的信息。我可以确定如果 ?1 失败 ?2 会成功，那么告诉 agda 评估 f 总是有意义的吗？

我将 g 解释为一个函数，它接受一个数字 n，一个 n 是偶数的证明，一个 (succ n) 是偶数的证明，并返回一个数字。（这是阅读本文的正确方法吗？或者有人可以提出更好的阅读方法吗？）我真的很想准确（或更准确地）理解上述类型的检查方式。它是否使用感应 - 它是否将 (evenB n) 与 p 连接：甚至 n？等等。我现在很困惑，因为它知道

不正确。首先我明白为什么 - q 代表 succ n，所以它不匹配。但是第二次失败了，而且原因更加神秘，而且似乎阿格达比我想象的还要强大……

如果我能弄清楚该怎么做（如果有意义的话），这是我非常喜欢的第一步。

其中奇数 p 证明如果偶数 n 是荒谬的，那么 succ n 是偶数。我想，这将要求我能够使用依赖类型的值。

最终，我希望能够写出这样的东西：

或类似的规定。甚至

我真的很想知道如何制作与依赖类型相对应的证明，以便我可以在程序中使用它。有什么建议么？

我想创建一个辅助函数，它将从索引或参数化类型中获取一个术语并返回该类型参数。

这可能吗？（我可以看到showType []可能有问题，但是当 Type 被索引时呢？）

我仍在尝试围绕 agda 进行思考，所以我写了一个小井字游戏类型

这将拥有一个有效的游戏路径。

这里#ofMoves gs将返回空Squares 的数量， n < (#ofMoves gs)将证明n第 th 步是有效的，并makeMove gs x n替换n游戏状态向量中的第 th 个空 Square。

在与自己进行了几场刺激的比赛之后，我决定拍摄更棒的东西。目标是创建一个函数，让 x 玩家和 o 玩家在史诗般的生死战中相互对抗。

这(0 < (#ofMoves gs))是游戏正在进行的证明的“速记”， 将返回您所期望的游戏状态gameCondition gs（之一xWin，，，或oWin）drawongoing

我想证明有有效的动作（s≤s z≤n部分）。这应该是可能的，因为suc nn<= #ofMoves gs。我不知道如何在 agda 中完成这项工作。

I want some clarification on double negations in agda.

even though

I cannot figure out how to prove:

Which is long hand for ¬ (0 ≢ 0). Perhaps I've missed an agda idiom somewhere along the way. Idealy I'd like an explanation with minimal reference the standard library.

我在上一个问题Using the value of a computed function for a proof in agda 中看到了检查函数的示例，但我仍然无法解决这个问题。

这是一个简单的例子：

给定函数crazy，

我想创建一个safe这样的函数safe : {nn : ℕ} -> (id nn) ≢ 0 -> Fin (id nn)。换句话说，它会返回一个数字 mod crazy，如果你给它一个疯狂的证明是 0。（我知道这个例子有点做作，我可能会更好地使用suc函数签名）

我的第一个解决方案是

但这是漫长而混乱的。因此，我尝试在将计算函数的值用于 agda 中的证明中模拟示例，但只能到此为止

我认为，inspect 使用 Hidden 在类型签名中隐藏函数应用程序的记录。然后可以使用reveal来检索它。

这是我认为我理解的：

Reveal_is_似乎持有隐藏的价值f，并且x；以及x应用于的结果f。 [_]将导致该相等性的证明。

⊥-elim接受矛盾证明并返回矛盾。

我要投入什么才能让它???发挥作用？