Dafny归纳数据类型的词典序定义与反自反引理证明问题问询

• Dafny 内置了针对归纳数据类型的词典序自动生成能力，无需手动拼接冗长的构造器优先级判断。通过在datatype声明上添加{auto_lex}注解，编译器会严格按照构造器的声明顺序自动生成对应的词典序比较逻辑：对不同构造器，按声明顺序判定大小；对相同构造器，递归按解构子的顺序做词典序比较，逻辑和你手写的规则完全等价，且从根本上避免漏写构造器分支、条件写反的问题。
• 针对带共享解构子名称的同结构构造器组（比如多个单参数的C2/C3、多个双参数的C4/C5），可以将同参数结构的比较逻辑抽为通用谓词，避免重复编写完全相同的子项比较规则。比如把单参数构造器的比较逻辑封装为通用的一元比较函数，双参数的封装为二元比较函数，在词典序谓词中直接复用，大幅减少重复代码。
• 自动生成的词典序会配套提供对应的反自反、传递、全序性质的可自动证明引理，不需要手动编写大量归纳证明代码。

• Dafny的if语句仅基于显式写出的布尔条件做分支判断，不会主动对归纳类型的构造器做穷尽性拆分。当使用零散的if判断来匹配构造器时，Dafny无法自动推导当前条件组合是否覆盖了所有可能的构造器场景，尤其是构造器数量增多、if嵌套加深时，求解器无法穷举所有条件组合的类型不变量，自然无法自动完成证明。
• 相比之下，match语句是显式的穷尽模式匹配，Dafny会强制校验所有分支覆盖所有构造器情况，并且在每个匹配分支自动注入对应的构造器类型不变量：比如匹配到C2(phi)分支时，证明器会直接确认当前值的构造器类型为C2，不需要手动补写!beta.C1? && !beta.C2?这类排除条件，证明器有足够的上下文自动完成子项的归纳证明。
• 空else分支触发后置条件报错，本质是if分支下证明器缺少足够的类型不变量。当你只写if alpha.C1? { ... }这类简单判断时，剩下的else分支里证明器仅能知道alpha不是C1，无法主动从leq_T的谓词定义中拆出额外的约束（比如哪些构造器组合不可能满足双向leq的前提），自然无法证明该分支下的后置条件。
• 原示例中构造器数量较少，零散if判断碰巧能让求解器推导足够的上下文完成证明；当构造器数量增加后，零散if带来的条件组合复杂度会超过求解器的启发式推导能力，就会出现证明失效的问题。

内容的提问来源于stack exchange，提问作者jiplucap