Incomplete termination measure for option of seq

[sonmarcho]

Dafny does not generate a complete termination measure for the example below:

datatype Option<+T> = | Some(value: T) | None

function method SumF<T(!new)>(f: T ~> nat, ts: seq<T>) : nat
  reads f.reads
  requires forall t | t in ts :: f.requires(t)
{
  if ts == [] then 0 else f(ts[0]) + SumF(f, ts[1..])
}

datatype Tree =
  | Leaf(x: nat)
  | Node(children: Option<seq<Tree>>)
{
  // FAILS: Dafny does not know that: this.children.value[i] < this
  function method Sum() : nat
    decreases this
  {
    match this {
      case Leaf(x) => x
      case Node(children) =>
        match children {
          case Some(cs) =>
            SumF(var f := (t: Tree) requires t in children.value => t.Sum(); f, cs)
            //                                                        ^^^
            //                  Error: decreases clause might not decrease
          case None => 0
        }
    }
  }
}

[MikaelMayer]

I can make it work like this, using the parent trick described here:

datatype Option<+T> = | Some(value: T) | None

function method SumF(ghost parent: Tree, f: Tree ~> nat, ts: seq<Tree>) : nat
  reads f.reads
  requires forall i | 0 <= i < |ts| :: ts[i] < parent
  requires forall t | t in ts :: f.requires(t)
{
  if ts == [] then 0 else f(ts[0]) + SumF(parent, f, ts[1..])
}

datatype Tree =
  | Leaf(x: nat)
  | Node(children: Option<seq<Tree>>)
{
  // FAILS: Dafny does not know that: this.children.value[i] < this
  function method Sum() : nat
    decreases this
  {
    match this {
      case Leaf(x) => x
      case Node(children) =>
        assert children < this;
        match children {
          case Some(cs) =>
          
            var f := (t: Tree) requires t in children.value && t < this => t.Sum();
            assert forall i | 0 <= i < |cs| :: cs[i] < children by {
              forall i | 0 <= i < |cs| ensures cs[i] < children {
                Under(children, i);
                assert cs[i] < children;
              }
            }
            SumF(this, f, cs)
            //                                                        ^^^
            //                  Error: decreases clause might not decrease
          case None => 0
        }
    }
  }
}

lemma {:axiom} {:verify false} Under(x: Option<seq<Tree>>, i: int)
  requires x.Some?
  requires 0 <= i < |x.value|
  ensures x.value[i] < x
{

}

The major reason is that the "<" relation is the prefix relation for sequences:
Note that I have to fix the incompleteness of type parameters by expliciting the type of the arguments of Sum

Moving this thread to discussions. If you want to ask for a specific feature.

[sonmarcho]

I actually used the parent trick several times when encountering similar issues, I didn't know it was documented: thanks for the link!

In this specific case however it was cumbersome to do so, because we really don't want to carry the parent expression around: my workaround was to define an OptionTree datatatype, mutually recursive with Tree:

function method SumF<T(!new)>(f: T ~> nat, ts: seq<T>) : nat
  reads f.reads
  requires forall t | t in ts :: f.requires(t)
{
  if ts == [] then 0 else f(ts[0]) + SumF(f, ts[1..])
}

// This type is mutally recursive with ``Tree``
datatype OptionTrees = | Some(value: seq<Tree>) | None

datatype Tree =
  | Leaf(x: nat)
  | Node(children: OptionTrees)
{
  function method Sum() : nat
    decreases this
  {
    match this {
      case Leaf(x) => x
      case Node(children) =>
        match children {
          case Some(cs) =>
            SumF(var f := (t: Tree) requires t in children.value => t.Sum(); f, cs)
          case None => 0
        }
    }
  }
}

Also note that here I am aware that we don't have: this.children < this nor this.children[i] < this.children, as we can't compare datatypes and sequences. However it would be nice if we could have: this.children[i] < this, which is what I need for termination.

[sonmarcho]

Tagging @cpitclaudel

[cpitclaudel]

Can we move this discussion back to the original issue? This is seems like a pretty reasonable enhancement request to me (wrapping children in an option shouldn't change the termination of the original function.

The workaround of using a ghost parent isn't generally suitable, since SumF is a library function (and the problem isn't directly due to the use of a separate function; see below:

This fails:

datatype Option<+T> = Some(value: T) | None

datatype Tree = Tree(x: int, children: Option<seq<Tree>>)
{
  predicate method Positive()
    decreases this
  {
    && this.x >= 0
    && match children
        case Some(cs) => forall t | t in children.value :: t.Positive()
        case None => true
  }
}

This works (no seq):

datatype Tree = Tree(x: int, children: Option<Tree>)
{
  predicate method Positive()
    decreases this
  {
    && this.x >= 0
    && match children
        case Some(t) => t.Positive()
        case None => true
  }
}

This works (no Option):

datatype Tree = Tree(x: int, children: seq<Tree>)
{
  predicate method Positive()
    decreases this
  {
    && this.x >= 0
    && forall t | t in children :: t.Positive()
  }
}

[cpitclaudel]

Update on this: it looks like adding the following axiom might be sufficient in the prelude:

axiom (forall<T> s: Seq T :: { BoxRank($Box(s)) }
  BoxRank($Box(s)) == Seq#Rank(s));

Currently we already have this:

function BoxRank(Box) : int;

axiom (forall d: DatatypeType :: { BoxRank($Box(d)) }
  BoxRank($Box(d)) == DtRank(d));

so it seems like a simple omission.

[cpitclaudel]

Moved to issue #2585