A strange predicate that cannot prove assertion already defined in body

Suppose we have a datatype called Tree, and a function size to calculate its size

datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)
function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

Now for some reasons, I wanna let this tree be somehow "balanced". Specifically, that is

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= alpha*(size(t) as real)
    && size(t.right) as real <= alpha*(size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

When alpha_weight_balanced holds, the size of each child of tree t is less than alpha*size(t). And naturally, this lemma should hold

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= alpha*(size(t) as real)
{}

However, dafny could not prove this "obvious" lemma. I even tried wrap size like

function f(a: int): int
// there is no implemetion for `f`

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    f(size(t.left)) as real <= alpha*f(size(t)) as real
    && f(size(t.right)) as real <= alpha*f(size(t)) as real
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures     f(size(t.left)) as real <= alpha*f(size(t)) as real
              && f(size(t.right)) as real <= alpha*f(size(t)) as real
{
}

And dafny proves this successfully. But if I modify the function f

function f(a: int): int
ensures f(a) == a

The proof failed again.

I'm so confused about it, anyone knows why?

One way to avoid verification failure is to hide real number multiplication inside function. Reason you don't require this when doing such verification in nat and int is dafny does automatically for you.

datatype Tree = Empty | Node(key: int, left: Tree, right: Tree)

function size(t: Tree): (s: nat)
{
  match t
  case Empty => 0
  case Node(_, l, r) => size(l) + size(r) + 1
}

function multiply(a: real, b: real): real { a * b }

predicate alpha_weight_balanced(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
{
  if t == Empty then true
  else
    size(t.left) as real <= multiply(alpha, size(t) as real)
    && size(t.right) as real <= multiply(alpha, size(t) as real)
    && alpha_weight_balanced(t.left,alpha)
    && alpha_weight_balanced(t.right,alpha)
}

lemma test(t: Tree, alpha: real)
  requires 0.5 <= alpha < 1.0
  requires alpha_weight_balanced(t, alpha)
  requires t != Empty
  ensures size(t.left) as real <= multiply(alpha, size(t) as real)
{}