在 agda 模式下与 agda 交互？

Question

感觉超级尴尬和agda交互。

考虑证明状态：

_ = begin
  5 ∸ 3
  ≡⟨⟩
   4 ∸ 2 ≡⟨⟩
   3 ∸ 1 ≡⟨⟩
   2 ∸ 0 ≡⟨⟩  { 2 <cursor-goes-here> }0

当我输入 C-c C-l (type-check) 时，它会说

?0 : 2 ∸ 0 ≡ _y_131
_y_131 : ℕ  [ at /home/bollu/work/plfa/src/plfa/part1/Naturals.lagda.md:586,5-10 ]

这似乎不是一个大错误？ refine (C-c C-r) 也没有给我一个好的错误信息：它只告诉我：

cannot refine

1. 如何让 adga 告诉我：

你已经完成了证明，除了缺少\qed

1. 一般来说，构建证明时的“首选交互模式”是什么？

Answer 1

整体问题

您的帖子以以下假设开始：

和agda交互感觉超级尴尬。

可以解释您的感受的原因是您似乎假设 Agda 可以推断出一个术语和它的类型，换句话说，既可以推断出您希望证明的属性，也可以推断出它的证明. Agda 通常可以做到其中之一，但要求两者都没有多大意义。作为比较，想象一下在公园的长椅上，当一个完全陌生的人走过来坐在你旁边，一言不发。你可以看出他很乐意问你一些事情，但是，尽管你努力让他说话，他仍然保持沉默。几分钟后，陌生人对你大喊大叫，尽管他口渴，但你没有带他预期的饮料。在这个比喻中，陌生人是你，你是阿格达。你不可能知道他渴了，更别说给他喝水了。

具体来说

您提供了以下代码：

_ = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩  { 2 <cursor-goes-here> }0

这段代码缺少类型签名，这将允许 Agda 为您提供更多帮助。当您输入 check 时，Agda 通过为您提供推断的目标类型来告诉您：

?0 : 2 ∸ 0 ≡ _y_131
_y_131 : ℕ  [ at /home/bollu/work/plfa/src/plfa/part1/Naturals.lagda.md:586,5-10 ]

在这里，Agda 说您的证明目标是 2 ∸ 0 等于某个未知自然数 y。这个数字是未知的，Agda 几乎不可能帮助您在证明工作中走得更远，因为它甚至不知道您要证明什么。据它所知，您的目标可能是5 ∸ 3 ≡ 3，因为希望不存在证明项。

回到我们的比喻，你缺少“我口渴”这句话。如果陌生人提供这条信息，您可以 - 可能 - 做出反应，这意味着 Agda 可以尝试提供帮助。

解决方案

我假设你想证明你的减法结果是二，在这种情况下，代码如下：

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ {!!}

在这种情况下，您可以通过多种方式与 Agda 进行交互，这都导致 Agda 为您提供了一个隔音术语：

你可以调用Agsy为你解决问题（CTRL-c CTRL-a），导致：

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ refl

您可以尝试直接优化目标（CTRL-c CTRL-r），询问 Agda 是否存在任何具有正确类型的唯一构造函数，结果相同：

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ refl

如果您希望使用 \qed 结束您的证明，您可以尝试将 _∎ 输入到孔中，然后精炼 (CTRL-c CTRL-r) 给出：

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ {!!} ∎

在结果目标中调用 Agsy 自然会给出：

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ 2 ∎