在验证终止时，如何告诉Dafny使用引理

问题描述

Dafny利用reduces子句来验证递归函数是否终止。当验证失败时，可以以引理的形式给Dafny一个提示。在检查reduces子句实际减少时，如何告诉Dafny使用引理？

datatype List<T> = Nil | Cons(head:T,tail:List<T>) 
datatype Twee = Node(value : int,left : Twee,right : Twee) | Leaf
function rotateLeft(t:Twee) :Twee
{
    match t 
       case Leaf => t 
       case Node(v,Node(vl,ll,rl),r) => Node(vl,Node(v,rl,r))
       case Node(v,Leaf,r) => Node(v,r)
}
  function Leftheight(t:Twee) :(h:nat) decreases t
{
  match t 
    case Leaf => 0 
    case Node(_,l,_) =>  1+Leftheight(l)
}     
lemma {:induction ll,r} decreasesHint(v:int,vl:int,ll:Twee,rl:Twee,r:Twee)
   ensures   Leftheight(Node(v,r)) == 
           1+ Leftheight(Node(vl,r)))  {} 
function rotateAllLeft(t:Twee) :Twee
    decreases t,Leftheight(t)
{
    match t 
       case Leaf => Leaf 
       case Node(v,rotateAllLeft(r))  //decrases t
       case Node(v,r) => //{ decreasesHint(v,vl,r);}
                  rotateAllLeft(rotateLeft(Node(v,r)))     
}

很抱歉，这么长的示例，但这是我第一次想提供检查终止的提示。错误failure to decrease termination measure出现在最后一行rotateAllLeft(rotateLeft(Node(v,r)上。

解决方法

您可以从表达式内部调用引理。只需使用分号将引理调用与表达式的其余部分分开。

      case Node(v,Node(vl,ll,rl),r) =>
        decreasesHint(v,vl,rl,r);
        rotateAllLeft(rotateLeft(Node(v,r)))

请注意，这不能完全解决您的终止问题，因为您的decreases批注是t,Leftheight(t)，这意味着递归调用必须减小t或离开{ {1}}相同并减小左侧高度。但是，此递归调用不会使t保持不变。我尝试将您的注释更改为仅t，它接受​​了此decreases Leftheight(t)，但在先前的case上却给出了错误。也许您可以找到解决方法。