阿格达权力定理

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,阿格达会看看的定义_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})

试着弄清楚为什么会有效!如果您有任何问题,请在评论中告诉我,我会帮助您.