Decreases for functions in datatypes

[gancherj]

Hi all! Apologies if this is an oft-requested issue. Is there a way to make the following go through?

datatype Tree = | Node(n : int) | Branch(f : bool -> Tree)

function Size(t : Tree) : int
	decreases t
{
	match t
		case Node(_) => 0
		case Branch(f) => 1 + Size(f(false)) + Size(f(true)) // Error : decreases clause might not decrease
}

The above is a pattern common to other proof assistants (e.g., Coq, F*), so I would hope that there's some way to encode it here as well.

[MikaelMayer]

I think the following works for you. Dafny does not compare functions and trees, so you need to provide the comparison explicitely.

datatype Tree_ = | Node(n : int) | Branch(f : bool -> Tree_) {
  predicate WellFormed() {
    match this {
      case Node(i) => true
      case Branch(f) => forall b: bool :: f(b) < this && f(b).WellFormed()
    }
  }
}

type Tree = t : Tree_ | t.WellFormed() witness Node(0)

function Size(t : Tree) : int
	decreases t
{
	match t
		case Node(_) => 0
		case Branch(f) => 1 + Size(f(false)) + Size(f(true)) // Error : decreases clause might not decrease
}