Cannot prove extremely simple equality already stated.

[MikaelMayer]

Dafny version

4.0.0.50303

Code to produce this issue

function HasProperty<T>(InputTest: T -> bool): bool

function
  HasPropertyMap<T>(m: T -> T, test: T -> bool) : bool {
  HasProperty((t: T) => test(m(t)))
}

lemma CannotInstantiate(test: int -> bool, m: int -> int) {
  assert HasPropertyMap(m, test)
      == HasProperty((t: int) => test(m(t)));
}

Command to run and resulting output

Just pâste into VSCode or verify from the command line.

It says the assertion might not hold.

What happened?

I would have expected the assertion to hold out of the box since I'm just copying the definition of HasPropertyMap.

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

Windows

[MikaelMayer]

Debugging the issue in Boogie reveals the following only difference between the two expressions that prevents Boogie from concluding to equality easily

 _module.__default.HasProperty(TInt, 
             Lit(AtLayer((lambda $l#0#ly#0: LayerType :: 
                   Handle1((lambda $l#0#heap#0: Heap, $l#0#t#0: Box :: 
                       $Box($Unbox(Apply1(TInt, 
                             TBool, 
                             $l#0#heap#0, 
                             test#0,
-                            Apply1(TInt, 
+                            $Box($Unbox(Apply1(TInt,
                               TInt, 
                               $l#0#heap#0, 
                               m#0, 
-                              $l#0#t#0
+                              $Box($Unbox($l#0#t#0): int)
-                            ))): bool)),
+                            )): int))): bool)),
                     (lambda $l#0#heap#0: Heap, $l#0#t#0: Box :: 
                       $IsBox($l#0#t#0, TInt)), 
                     (lambda $l#0#heap#0: Heap, $l#0#t#0: Box :: 
                       SetRef_to_SetBox((lambda $l#0#o#0: ref :: false))))), 
                 $LS($LZ))));

[MikaelMayer]

So a solution is to remove all generics, but that's not feasible in my case.

[MikaelMayer]

More investigation: So it seems that the test variable's output is boxed/unboxed in both cases, so the problem comes only from the "m". Indeed, I can make a shorter example:

function HasProperty<T>(InputTest: T -> T): bool

function 
  HasPropertyMap<T>(m: T -> T) : bool {
  HasProperty((t: T) => m(t))
}

lemma CannotInstantiate(m: int -> int) {
  assert HasPropertyMap<int>(m)
      == HasProperty((t: int) => m(t));
}

And a workaround is to define

function 
  HasPropertyMapInt(m: int -> int) : bool {
  HasProperty((t: int) => m(t))
}

This time, the assertion passes:

lemma Works(m: int -> int) {
  assert HasPropertyMapInt(m)
      == HasProperty((t: int) => m(t));
}

[RustanLeino]

Another workaround is to collect the two occurrences of the lambda expressions into one place:

function HasProperty<T>(InputTest: T -> bool): bool

function MyLambdaExpression<T>(m: T -> T, test: T -> bool): T -> bool {
  (t: T) => test(m(t))
}

function HasPropertyMap<T>(m: T -> T, test: T -> bool) : bool {
  HasProperty(MyLambdaExpression(m, test))
}

lemma CanInstantiate(test: int -> bool, m: int -> int) {
  assert HasPropertyMap(m, test)
      == HasProperty(MyLambdaExpression(m, test));
}

or more generically:

function HasProperty<T>(InputTest: T -> bool): bool

function Compose<A, B, C>(f: A -> B, g: B -> C): A -> C {
  a => g(f(a))
}

function HasPropertyMap<T>(m: T -> T, test: T -> bool) : bool {
  HasProperty(Compose(m, test))
}

lemma CanInstantiate(test: int -> bool, m: int -> int) {
  assert HasPropertyMap(m, test)
      == HasProperty(Compose(m, test));
}

[RustanLeino]

To improve this situation in Dafny, perhaps we should always box when translating lambda expressions.

[MikaelMayer]

That workaround works like a charm ! What is boxing and unboxing for, by the way?