Unable to reason about types that extends a non-ref trait

[txiang61]

Dafny version

4.4.0

Code to produce this issue

trait Object {}

type A extends Object {}

type B extends Object {}

lemma test(x: Object)
  ensures (x is A) ==> !(x is B)
{}

Command to run and resulting output

/tmp/tmpvliupB.tmp.dfy(9,0): Error: a postcondition could not be proved on this return path
  |
9 | {}
  | ^

/tmp/tmpvliupB.tmp.dfy(8,23): Related location: this is the postcondition that could not be proved
  |
8 |   ensures (x is A) ==> !(x is B)
  |                        ^^^^^^^^^


Dafny program verifier finished with 0 verified, 1 error

What happened?

It makes sense if both A and B are trait, but for type I think it should be able to reason about it. If A and B are classes, then the lemma can be proven.

What type of operating system are you experiencing the problem on?

Mac

[MikaelMayer]

I think it should be expected.
There is no reason why type A and type B couldn't be the same type.
Of course, if they are different class definitions, they are provably different. But the type declaration here is an abstract type declaration and could be refined from an abstract module to the same type that extends both traits (for example, a class)
The code above should not compile because you use "type" without any right-hand-side, so that means you are defining an abstract type.
If this answer your issue, you can close the issue.

[RustanLeino]

I agree with @MikaelMayer. Here is some code to support that argument. To try this, use --type-system-refresh --general-traits:datatype.

abstract module M {
  trait Object {}

  type A extends Object {}

  type B extends Object {}

  //lemma test(x: Object)
  //  ensures x is A ==> !(x is B)
}

module M0 refines M {
  // Since A and B are opaque types in M, they may refer to the same type
  type A = C
  type B = C
  trait C extends Object { }

  datatype D extends C = D

  lemma CounterExample() returns (x: Object)
    ensures x is A && x is B
  {
    x := D;
    var a: A := D;
    var b: B := D;
    assert a == x == b;
  }
}

module M1 refines M {
  // Here's a different way to show the counterexample. Here, A and B remain
  // distinct types, but they are both extended by another type.

  type A = AA
  type B = BB
  trait AA extends Object { }
  trait BB extends Object { }

  datatype D extends AA, BB = D

  lemma CounterExample() returns (x: Object)
    ensures x is A && x is B
  {
    x := D;
    var a: A := D;
    var b: B := D;
    assert a == x == b;
  }
}

[robin-aws]

Reopening this just because while the counterexamples above are true given the lack of context in the original report, with more context to exclude those counterexamples it may be reasonable to expect Dafny to be able to prove the lemma. @txiang61 can you provide some of that context?

[txiang61]

Thanks for the explanation!

I have some functions that does a subtype check and returns a value based on what the type is. Here is a simplified version of what I was trying to prove.

method convert( v: Object) returns (res: nat)
  ensures v is B ==> res == 1
{
  if v is A {
    return 0;
  } else if v is B {
    return 1;
  }
  return 0;
}

Just noticed that it doesn't seem to work with datatype either? Though datatype isn't what we want since it has constructors.

module M {
  trait Object {}

  datatype A extends Object = A() {}

  datatype B extends Object = B() {}

  lemma test(x: Object)
    ensures x is A ==> !(x is B)
  {}
}

I'm ok with just listing the relationships as axioms. It does gets long as the hierarchy expands and easy to make mistakes. Just wondering if there is a better way.

[MikaelMayer]

That's indeed a must have. For now, you can do the proof like this:

lemma test(x: Object)
    ensures x is A ==> !(x is B)
  {
    if x is A {
      var a: A :| a == x;
      if x is B {
        var b: B :| b == x;
        assert false;
      }
    }
  }

[MikaelMayer]

Feel free to close this issue if your need has been resolved.

[dschoepe]

The proof above no longer works for me using the latest Dafny commit (a88c3e4aad2b202439f26081226e91e63f49aa57). I was able to fix the proof and reduce the boilerplate slightly (no longer needing an explicit proof for each pair of types), but this is still quite cumbersome for a lot of subtypes and does not play well with more than one level of inheritance:

module M {
  trait Object {
   ghost function typeId() : (id: string)
  }

  type A extends Object {
   ghost function typeId() : (id: string)  { "A" }
  }

  type B extends Object {
   ghost function typeId() : (id: string)  { "B" }
  }
  type C extends Object {
   ghost function typeId() : (id: string)  { "C" }
  }

  lemma test(x: Object)
    ensures x is A ==> !(x is B)
    ensures x is A ==> !(x is C)
    ensures x is B ==> !(x is C)
  {
    if x is A {
    }
    if x is B {
      assert x.typeId() == "B";
    }
  }
}

[RustanLeino]

Here's a slightly shorter proof, but the lemma still requires a quadratic number of postconditions:

trait Object {
  ghost function TypeId(): string
}

datatype A extends Object = A() {
  ghost function TypeId(): string { "A" }
}

datatype B extends Object = B() {
  ghost function TypeId(): string { "B" }
}

lemma DisjointAB(x: Object)
  ensures !(x is A && x is B)
{
  var _ := x.TypeId();
}

method convert(v: Object) returns (res: nat)
  ensures v is B ==> res == 1
{
  DisjointAB(v);
  if v is A {
    return 0;
  } else if v is B {
    return 1;
  }
  return 0;
}

[keyboardDrummer]

Could the postcondition on the lemma be something like

ensures multiset{x is A, x is B, x is C}[true] == 1

, so it's linear in the number of types?

@dschoepe is there a feature request remaining in this issue?

[dschoepe]

With the workaround you suggested it's not a big issue, but I would say it'd still be a nicer user experience to have Dafny prove this on its own without these extra lemmas and TypeId.

[keyboardDrummer]

With the workaround you suggested it's not a big issue, but I would say it'd still be a nicer user experience to have Dafny prove this on its own without these extra lemmas and TypeId.

Could you be more explicit about what you want it to prove without help? Sorry if I'm a little slow to understand