与agda在agda模式下进行交互？

如何解决与agda在agda模式下进行交互？

与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. 通常，构建证明时“首选的交互方式”是什么？

解决方法

总体问题

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

与agda互动非常尴尬。

之所以可以解释您的感觉，是因为您似乎认为Agda可以同时推断一个术语及其类型，换句话说，就是您想证明的特性和它的证明。 。阿格达（Agda）通常可以执行其中一项操作，但是要求两者都没有多大意义。相比之下，想象一下在公园的长凳上，当一个陌生的陌生人走过来坐在你旁边时，什么也没说。您可以看到他非常乐意向您询问一些内容，但是尽管您努力使他说话，他仍然保持沉默。几分钟后，陌生人对你大喊，尽管他很口渴，但你没有拿到他所期望的饮料。在这个比喻中，陌生人是你，而你是阿格达。您不可能知道他渴了，更不用说把他喝了。

具体

您提供了以下代码：

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

这段代码缺少类型签名，这将使Agda能够为您提供更多帮助。当您输入检查内容时，Agda会通过为您提供目标的推断类型来告诉您：

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

在这里，阿格达说您的证明目标是2 ∸ 0等于某个未知的自然数y。这个数字是未知的，因为Agda甚至不知道您想证明什么，因此Agda几乎不可能帮助您进一步进行证明。据其所知，您的目标可能是5 ∸ 3 ≡ 3，希望没有证据项。

回到我们的隐喻，您缺少“我渴了”的说法。如果陌生人提供了这些信息，您可能会做出反应，这意味着Agda可以尝试并提供帮助。

解决方案

我假设您希望证明减法的结果是2，在这种情况下，代码如下：

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 ∎