2

我试图证明以下几点：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1
1-pow {zero} = refl
1-pow {suc x} = {!!}

我是 Adga 的新手，甚至不知道从哪里开始。有什么建议或指导吗？显然很容易在纸上证明，但我不确定要告诉 Agda 什么。

我将我的 pow 函数定义如下：

_pow_ : ℕ → ℕ → ℕ
x pow zero = 1
x pow (suc zero) = x
x pow (suc y) = x * (x pow y)
4

1 回答 1

6

当您对nin 进行模式匹配1-pow并发现它是zero时，Agda 将查看_pow_并检查其中一个函数子句是否匹配。第一个确实如此，因此它将应用该定义并1 pow zero变为1. 1显然等于1，因此refl将适用于证明。

那案子n是什么时候suc x？这就是问题所在：Agda 不能承诺第二个子句（因为xcould be zero）也不能承诺第三个子句（因为xcould be suc yfor some y）。因此，您必须进一步确保 Agda 应用以下定义_pow_：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1
1-pow {zero}        = refl
1-pow {suc zero}    = {!!}
1-pow {suc (suc x)} = {!!}

让我们看看第一个孔的类型是什么。Agda 告诉我们它是1 ≡ 1，所以我们可以refl再次使用。最后一个有点棘手，我们应该产生一些 type 1 * 1 pow (suc x) ≡ 1。假设您使用的是标准定义_*_（即左侧参数的递归和左侧的重复添加，例如标准库中的那个），这应该减少到1 pow (suc x) + 0 ≡ 1. 归纳假设（即1-pow应用于suc x）告诉我们1 pow (suc x) ≡ 1。

所以我们快到了，但我们不知道n + 0 ≡ n（那是因为加法是通过左参数的递归定义的，所以我们不能简化这个表达式）。一种选择是证明这一事实，我将其留作练习。不过，这里有一个提示：您可能会发现此功能很有用。

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

它已经是Relation.Binary.PropositionalEquality模块的一部分，所以你不需要自己定义它。

所以，回顾一下：我们知道n + 0 ≡ n并且1 pow (suc x) ≡ 1我们需要1 pow (suc x) + 0 ≡ 1. 这两个事实很好地结合在一起——等式是传递的，所以我们应该能够合并1 pow (suc x) + 0 ≡ 1 pow (suc x)并1 pow (suc x) ≡ 1成为一个证明，事实上，情况就是这样：

1-pow {suc (suc x)} = trans (+0 (1 pow suc x)) (1-pow {suc x})

就是这样！

让我提一些其他方法。

整个证明也可以使用 的证明来完成1 * x ≡ x，尽管这与我们之前所做的几乎没有什么不同。

您可以简化_pow_为：

_pow_ : ℕ → ℕ → ℕ
x pow zero    = 1
x pow (suc y) = x * (x pow y)

这使用起来稍微方便一些。证明将相应地改变（即它不会有原始证明的第二个子句）。

最后，你可以这样做：

1-pow : ∀ {n : ℕ} → 1 pow n ≡ 1
1-pow {zero}        = refl
1-pow {suc zero}    = refl
1-pow {suc (suc x)} = cong (λ x → x + 0) (1-pow {suc x})

试着弄清楚为什么会这样！如果您有任何问题，请在评论中告诉我，我会帮助您。

于 2014-02-10T05:04:34.880 回答