在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

一般来说，在建立证据时，什么是“首选的交互模式”？

Answer 1

总体问题

你的职位从以下假设开始：

：与agda互动感觉非常尴尬。

可以解释你的感觉的原因是，你似乎认为Agda既可以推断术语，也可以推断出它的类型，换句话说，它既是你想要证明的属性，也是它的证明。Agda经常可以做到其中之一，但要求两者都没有多大意义。相比较而言，想象一下坐在公园的长凳上，一个完全陌生的人来到你身边，坐在你旁边，一言不发。你可以看到他很乐意问你一些事情，但是，尽管你努力让他说话，他仍然保持沉默。几分钟后，陌生人对你大喊大叫，说尽管他渴了，但你并没有把他期望的饮料带来。在这个比喻中，陌生人是你，而你是Agda。你不可能知道他渴了，更不用说把他的饮料拿来了。

具体而言

您给出了以下代码：

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

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

?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可以尝试并提供帮助。

解决方案

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

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

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

您可以调用Agsy为您解决问题(CTRL)，这将导致：

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

您可以直接尝试并改进目标(CTRL)，询问Agda是否存在任何具有正确类型的唯一构造函数，这将导致相同的结果：

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

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

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 ∎