如有巧合，纯属故意
本篇的出现确实纯属意外，本来我开开心心地在玩sodukuvania2，结果调整显示屏放大倍数注销账户，再登录上来就发现我的sodukupad记录全没了。当时我大概是1500分钟（连带boss），进度推进了2/3的样子（已经解锁到天文台那里了），全！没！了！再打一遍实在是重复劳动，突然想到推理过程中大量不严谨的推理过程（比如漏掉了一个候选数，虽然这个候选数到最后也不成立），干脆就重新写一个推理链记录吧
其实本计划还有一个lean4的尝试，但我也是学了没多久外加写基础设施的设计太纠结，已经推翻改了好几版结构（可以看commit记录），仓库地址在https://github.com/timesharingos/sodukuvania2，但不保证推进进度。（才发现自己拼错了，就这样不改名字了）
关于sudokuvania2
这其实是一个数独恶魔城。数独恶魔城标准采用战争迷雾规则，并随着推进不断解锁新的规则。即使你可能猜到了某些规则的内容，但在没有明确解锁前，不能以此为推理证据。与此同时，可能还会有一些boss关和精英怪，它们指向了另一个外部数独，通关后会解锁对应格子的数字。数独恶魔城一般不需要填满所有数字来解锁结局，但填满数字才会被视为全收集。
战争迷雾：部分格子为迷雾，其上的信息不可见，满足特定条件后解锁部分迷雾。
boss关：必须通过的关卡，会给出必不可缺的数字提示。
精英怪：可选关卡，即使不选择击败也不影响进度推进，其对应数字可通过主盘面推理得到。
推理链记录
这个推理链记录我选的是半形式化形态（也就是纸笔证明套了个形式化DSL的壳），因为严格形式化的话时间都投入在前期准备上了，而且半形式化的可验证性也相对不算损失太多。我大致会用的记号如下（这里并不全，只是最常用的，因为半形式化嘛有些地方满足无歧义就足够了）：
（推理条目）<name> : <ant> => <cons> [(with name [[by] (<param>=<value>)*])*] 基本格式，其中ant是条件，cons是结论。其实=>就是|-的翻版，但那个符号不好打出来（离小拇指太远了......）。若没有写=>则代表(empty)=><cons>，也就是无条件成立，这样省事一些。
（变量记号）$<name>与_<name>_：代表条目中的变量，调用时使用with标注替换值（即param=name的部分），且替换时对于一个变量必须全部替换（可以保留其他变量）。$和_仅仅是记号不同，因此它们之间对于不同的值同样需要不同的名字。变量的作用域为所在推理条目。
（假设引入）intro <name>:.....和end intro <name> 其实就是推理条目前加了一个intro关键字，用于假设引入。假设引入区块内的所有推理条目在区块外引入时自动带上<name>.的前缀和对应的前件前提。
（坐标）(u)g_gn_b_bn_/r_rn_/c_cn_ 正好也展示一下_<name>_的用法。其中g代表grid编号，b代表grid内block编号，r/c代表所属g/b/u内部的编号（取决于前方最近的是g、b还是c），u代表全局坐标。其中坐标约定以左上角为原点，向右向下延伸。若只写了一部分，则视为满足该条件的全部坐标的集合。
（候选数与确定数）候选数记作=?，确定填入则记为=，使用!标记否定。这里不区分集合和元素，或者也可以说直接元素默认视为单元素集合，反正就是按需取用，这个不影响其他推理过程。
（公理省略）对于可以无歧义且可以直接写出对应函数形式化形式或知名的函数，以及mp/iff/常见等价关系有可能不再写出，视为默认成立。
（注释，如果你真的想要的话......）依照祖训，自然是//这个啦！
从水下的第一个生命萌芽开始......Hello world!
在进入正式记录之前，先拿一个简单的killer数独熟悉一下记录吧！
killer数独：标准数独规则（也就是行列宫1-n不重复），每个虚线框出来的区域其中的数字不能重复且总和等于左上角数字。
首先，这里有一堆三缺一的杀手框，先来解决这些：
vr2c5_6 : r1c5=1, r1c6=3, r2c6=5, r1c5+r1c6+r2c5+r2c6=15 => r2c5=6 (with given) // 这里given代表条件由题目本身给出
vr2c3_4 : r2c1=3, r2c2=1, c2c4=2, (sum r2c1-4)=10 (with given) => r2c3=4 (with given) // with 可以用在单个条件之后，但仅能作为对应单条件的证据，其他证据仍然需要补齐证明。这里的sum和r2c1-4就分别是所谓“知名函数”和“明确表达的自然语言”。
r3c13_251 : r3c1-3 <- [2,5,1] (with given) // 这里纯粹的题目给定，因此无条件成立，<-[]可以理解为按顺序解构
vr3c4_6 : r3c13_251, (sum r3c1-4)=14 (with given) => r3c4=6 // 这里就没有结尾的with，因为单纯的算术不需要说明。引用其他的结论不需要证据。
vr5c1_1 : r4c1=4,r4c2=3,r5c2=2, (sum r4-5c1-2)=10 => r5c1=1 (with given)
vr6c2_4 : r6c1=6, r6c3=5, (sum r6c1-3)=15 => r6c2=4 (with given)
接下来，就出现了好多一个区域内仅有1个空格的，接下来清理这些：
vr1c1_5 : r2-6c1 <- [3,2,4,1,6] (with given), c1r_x_ 1..=6 (with given), nodup c1(with given), c1.length=6(with given) => r1c1=5 (with given, only_exist) // 这里only_exist指的是不重复+每个格子都是1-n+长度为n才个条件才能推出来1-n各自恰好1个，但这个自证不难doge
再往后应该就是这两种类型的组合了，剩下的就不再写了，作为课后习题（大雾？）
我有一个兔子，你有一个兔子......
1+1=2，这就是算数的基本原理 现在，请你解开NS方程吧！
当然我们不会这么夸张了，但从单grid到多grid，还有puzzle的全局规则，推理链的复杂程度会显著上升，但基本记号就这么多。下一节开始，才是真正的sudokuvania2（当然纯看我记号的熟练程度了，本身这部分的题目我已经做过三遍了......）
