如何解决Dafny中函数外延性缺失导致的有向图证明难题？

你在Dafny中定义了带函数字段的Digraph数据类型，希望证明行为完全一致的两个图实例相等，但因为Dafny不支持函数外延性（即输出完全相同的函数不会被视为相等），导致无法证明g == h。同时你尝试过用set实现相关字段，但遇到了易出错、证明速度慢的问题。

可行解决策略 #

1. 用行为等价谓词替代语法相等判断 #

Dafny中函数是内涵式的：只要不是同一个函数实例，哪怕输出完全一致也不会被判定为相等，所以直接证明g == h本质上不可行。你可以：

• 放弃证明图的语法相等，在所有需要判断图等价的场景（引理前置条件、方法后置条件、性质证明）中，直接使用你定义的DigraphsEqual谓词替代==。
• 基于DigraphsEqual推导所有后续性质，比如证明任意操作在满足DigraphsEqual(g,h)的两个图上返回相同结果，直接通过展开DigraphsEqual的量化条件来完成，不需要依赖g == h。

2. 改用外延性友好的数据结构替换函数字段 #

如果一定要追求语法层面的相等，可以把函数字段换成Dafny支持外延相等的类型，同时优化证明效率：

• IsNode：用set<Node>替代Node -> bool——两个set只要元素完全相同就相等，Dafny原生支持set的外延性。
• IsConnected：用set<(Node, Node)>替代(Node, Node) -> bool，同理依赖set的外延相等性。
• NodeMap/InvNodeMap：结合NodeBound的约束（节点映射的范围有限），用map<Node, nat>和map<nat, Option<Node>>替代函数——Dafny的map是外延相等的，只要所有键值对匹配就判定为相等。

针对set实现导致的证明慢问题，可以尝试这些优化：

• 给涉及set/map的谓词加上{:opaque}属性，避免自动展开过多量化条件；必要时手动展开关键部分。
• 拆分复杂引理，将大的证明目标拆分成多个小引理，逐步推导。
• 利用NodeBound约束限定量化变量的范围，比如证明IsNode等价时，只需要量化g.NodeMap(n) < g.NodeBound的节点，减少SMT求解器的搜索空间。

3. 封装抽象数据类型隐藏内部实现 #

定义一个抽象的Digraph类型，只暴露对外的操作（比如判断节点、判断连通性），隐藏内部的函数或set/map实现。这样外部逻辑只依赖行为等价性，内部实现的差异不会影响外部的等价性判断，也能避免直接处理函数相等的问题。

你的代码修正说明 #

注意到你定义的DigraphsEqual谓词中有笔误：

g.NodeBound == g.NodeBound

应该改为：

g.NodeBound == h.NodeBound

另外，你的DigraphValid谓词已经包含了对函数字段的约束（比如NodeMap的单射性、InvNodeMap与NodeMap的互逆性），这些约束可以辅助你在基于DigraphsEqual推导性质时，简化证明步骤。

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