function - 幂的 Agda 定理

Question

我正在尝试证明以下内容:

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)

Answer 1

当您在 n 上进行模式匹配时在1-pow发现它是zero ，Agda来看看_pow_的定义并检查函数子句之一是否匹配。第一个是这样的，所以它将应用该定义和 1 pow zero变成1 。 1显然等于1 ，所以refl将为证明工作。

n时的情况怎么样？是suc x ？问题是:Agda 无法提交第二个子句(因为 x 可能是 zero )，也不能提交第三个子句(因为 x 对于某些 suc y 可能是 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再次。最后一个有点棘手，我们应该生成 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})

尝试找出为什么会这样!如果您有任何问题，请在评论中告诉我，我会帮助您。