How to work around lack of Function Extensionality in Dafny?

I'm trying to write a program in Dafny where I build directed graphs and prove properties about them. Sometimes I'll have shown that two graphs are equivalent, and then I'd like to show that an arbitrary function will give the same result for the two graphs. I think the limiting factor is that functions that produce identical results aren't considered to be equal (Function extensionality in Dafny), so I can't prove that the two Digraphs are equal even if the behavior is identical.

What is a good strategy to approach a problem like this?

Perhaps I should have just used sets for IsNode and IsConnected? I have tried to avoid this because I found it really easy to mess up and get very slow proofs when I was using sets.

   datatype Digraph<!Node> = Digraph(
        IsNode: Node -> bool,
        IsConnected: (Node, Node) -> bool,
        NodeMap: Node -> nat,
        InvNodeMap: nat -> Option<Node>,
        NodeBound: nat
    )

    ghost predicate {:opaque} DigraphValid<Node(!new)>(g: Digraph)
    {
        (forall n: Node :: g.NodeMap(n) >= g.NodeBound ==> !g.IsNode(n)) &&
        (forall n: Node :: !g.IsConnected(n, n)) && // No self-connections
        (forall n: Node, m: Node :: g.IsConnected(n, m) ==> g.IsNode(n) && g.IsNode(m)) &&
        (forall n: Node :: g.InvNodeMap(g.NodeMap(n)) == Some(n)) &&
        Functions.Injective(g.NodeMap) && Functions.Injective(g.InvNodeMap)
    }

  ghost predicate {:opaque} DigraphsEqual<Node(!new)>(g: Digraph, h: Digraph)
    {
        (forall n: Node :: g.IsNode(n) == h.IsNode(n)) &&
        (forall n, m: Node :: g.IsConnected(n, m) == h.IsConnected(n, m)) &&
        (forall n: Node :: g.NodeMap(n) == h.NodeMap(n)) &&
        (forall n: nat :: g.InvNodeMap(n) == h.InvNodeMap(n)) &&
        g.NodeBound == g.NodeBound
    }

    lemma DigraphsEqualAreEqual(g: Digraph, h: Digraph)
        requires DigraphsEqual(g, h)
        ensures g == h
    {
        // I don't think this is possible to prove.
    }

Solution

It looks like your equality is actually an equivalence relation. As you have observed, equality in Dafny is not completely typed for functions so this is why you can't have extensionality.

Using sets definitely would make it possible to prove equality, and if you found some verification slowdowns, I'd be happy to help you speed them up.

Meantime, you could also try to hide the definition of IsNode: set or IsConnected: set<(Node, Node)> using refinement types and axioms, like that:

abstract module DiGraphs {
   type Set<T>

   predicate Contains<T>(s: Set<T>, n: T)

   datatype Digraph<Node> = Digraph(
        IsNode: Set<Node>,
        IsConnected: Set<(Node, Node)>,
        NodeMap: map<Node, nat>,
        InvNodeMap: map<nat, Node>,
        NodeBound: nat
    )
}

module Impl refines DiGraphs {
  type Set<T> = set<T>
}

With this abstraction over set, you have full control over which axioms of set you want to have in your abstract module, which you will prove in your concrete module that you can satisfy them. You can also define bodiless lemmas in DiGraphs that you'll prove in the refined module using the definition of sets.