最近在看《同构：编程中的数学》，觉得可以用lean4来写一下里面的习题，所以记录一下。
foldn
之前在C++中见到fold的时候说是折叠的意思，那时候我还在想为什么叫折叠。有左折叠和右折叠，左折叠就是从左边开始，对第一个和第二个元素应用一个二元函数，然后将得到的结果和第三个元素继续应用这个函数，直到应用完整个容器，右折叠就是从右边开始。最常用的一个例子就是函数是加法，那这个fold实现的功能就是求和，所以我当时的理解是这样的：想象数组就是一张有很多个水平折痕的纸，每个折痕就是一个元素，从左边第一个折痕开始，把它折到第二个折痕上，然后再把第二个折痕折到第三个折痕一直折到头，这样得到的纸条就是所有元素重叠在一起的了，如果把重叠理解为加法的话那就是这一条纸就是所有元素加在一起了。
题外话说完了，书上的说法是
我们称foldn 为自然数上的叠加（fold）操作。
所以其实是叠加的意思，这样折叠起来也确实是叠加了。按照书上的，用lean4实现的foldn如下：1
2
3def foldn {α : Type} (c : α) (f : α → α) : Nat → α
| 0 => c
| n' + 1 => f (foldn c f n')
大概意思是将操作f，在初始值c上叠加n次，其中α是一个类型参数，为了让这个fold更加通用。当n=0时直接返回c，当n=n'+1时，将f应用在foldn c f n'上，这其实就是一个递归了。
计数、累加和累乘
这也是按照书上的描述实现的1
2
3def num := foldn 0 Nat.succ
def sum := Prod.snd ∘ foldn (0,0) fun (a,b) => (a+1,a+1+b)
def fact := Prod.snd ∘ foldn (0,1) fun (a,b) => (a+1,(a+1)*b)
num就是0的n次后缀。sum和fact的话用到了二元组，二元组的第一个数是序号，第二个数是累加和累乘的结果。其中∘是lean4中函数组合的符号，用\o输入。
斐波那契数列和卢卡斯数列
1 | def fib := Prod.fst ∘ foldn (0,1) fun (a,b) => (b,a+b) |
跟前面不一样的地方在于这个二元组的意义不一样，第一个元素表示前一个值，第二个元素表示后一个值。
课后习题
1 | def pow2 := Prod.snd ∘ foldn (0,0) fun (a,b) => (a+1,b+2*a+1) |
pow2是平方，pow是n的m次方。平方那题我觉得出得很巧妙，或者说我觉得我写得很巧妙，我用平方公式来迭代的，也就是$(n+1)^2=n^2+2n+1$，迭代过程中的(a,b)表示的就是$(n,n^2)$，后一项的b可以通过前一项算出来。
pow如果书上把n和m的顺序换一下也是个好题，但是这个顺序太奇怪了，要先给出m，再给n，所以写得有点复杂。
还有一题奇数和之前漏了，所以放在扩展第一种里了
扩展
我在写前面的东西的过程中发现了一些共性的东西，觉得可以把它们提取出来一下，所以也写了一下，因为我不会起名字，所以就直接叫F了1
2
3
4
5def F {α:Type} (c:α) (g:α → α → α) (f:Nat → α) := Prod.snd ∘ foldn (0,c) fun (a,b) => (a+1,g b (f a))
def sumF (f:Nat → Nat) := F 0 Nat.add f
def sum := sumF Nat.succ
def factF (f:Nat → Nat) := F 1 Nat.mul f
def fact := factF Nat.succ
大概说一下F是怎么来的，前面观察累加和累乘我们会发现，其实除了个加号和乘号以外全部都是一样的，所以我们可以把a+1和b之间的符号提取出来，作为参数g。然后我们发现还有个看起来不顺眼的东西，a+1为什么会有个+1呢，这个东西的意义是什么，可以理解为一个对a的操作，总之先把它提取出来就对了，它就叫f了。
接下来我们可以实现一个广义上的数列的求和sumF，前面我们说的f就可以理解为一个数列，表示数列的第a项。接下来就可以实现一个奇数的和了1
def oddsum := sumF fun n => n*2+1
其中fun n => n*2+1就是用于计算第n个奇数。